🛡️ Ada – Safety-Critical Avionics (Ada 83/95/2005/2012, Ravenscar, SPARK)

1.1 Évolution : Ada 83 / 95 / 2005 / 2012 (vue avionique)

Timeline simplifiée

Version	Apports	Pourquoi ça compte en safety-critical
Ada 83	base structurée, packages, typage fort	interfaces claires, modularité, réduction d’erreurs
Ada 95	OOP, tâches/RT enrichi, hiérarchies	concurrence plus robuste, systèmes RT complexes
Ada 2005	améliorations RT, containers, patterns	outillage et expressivité (avec discipline)
Ada 2012	contracts (pre/post), expressions, safety	spécification plus précise, meilleure vérification

Lecture avionique : Ada a été conçu pour des projets longs, multi-équipes, où la maintenabilité et la preuve de sûreté sont aussi importantes que la performance.

1.2 Concepts fondamentaux Ada (packages, types, visibilité)

Package spec/body (modularité “contract-first”)

--  file: altitude.ads (spec)
package Altitude is
   subtype Feet is Integer range 0 .. 60_000;

   function Get return Feet;
   procedure Set (Value : Feet);
end Altitude;

--  file: altitude.adb (body)
package body Altitude is
   Current : Feet := 0;

   function Get return Feet is
   begin
      return Current;
   end Get;

   procedure Set (Value : Feet) is
   begin
      Current := Value; -- range-checked by subtype
   end Set;
end Altitude;

Ce que ça “achète” en safety

Subtypes + ranges : l’erreur “out of range” devient explicite.
Interface claire : la spec est un contrat (lisible/auditable).
Encapsulation : état interne caché, accès maîtrisé.
Lisibilité : moins de “pointeurs” et de surprises implicites.

L’idée n’est pas d’éviter tous les bugs “par magie”, mais de rendre les classes d’erreurs rares, visibles, et testables.

1.3 Pourquoi Ada est “safety-friendly” (safe by design)

Table : Ada vs classes d’erreurs fréquentes en C

Classe de problème	Approche Ada	Impact safety
Plages invalides	subtypes + ranges + checks	réduction erreurs silencieuses
Interfaces floues	spec explicite (package) + types	auditabilité accrue
Conversions	conversions explicites, typage strict	moins de “narrowing” invisible
Concurrence	primitives langage (tasks/protected)	modèle plus contrôlable
Undefined behavior	moins de zones UB “historiques”	exécution plus prédictible

Important : en safety-critical, on choisit souvent des sous-ensembles/profils (et des règles internes) même en Ada, pour renforcer le déterminisme et la vérifiabilité.

2.1 Concurrence Ada : tasks & protected objects (temps réel)

Protected object : partage de données maîtrisé

protected type Sensor_Buffer is
   procedure Put (V : Integer);
   function  Get return Integer;
private
   Last : Integer := 0;
end Sensor_Buffer;

protected body Sensor_Buffer is
   procedure Put (V : Integer) is
   begin
      Last := V;
   end Put;

   function Get return Integer is
   begin
      return Last;
   end Get;
end Sensor_Buffer;

Lecture safety / deterministic

Encapsulation + exclusion mutuelle gérée par le langage.
Réduit le risque de races “accidentelles”.
Facilite l’analyse de contention / latence.

Dans les profils “stricts”, on limite encore certaines constructions de concurrence pour rendre le scheduling prouvable.

Diagramme (concept) : tasks périodiques

sequenceDiagram
  participant T10 as Task@10ms
  participant T50 as Task@50ms
  participant Buf as Protected Buffer

  T10->>Buf: Put(sensor_sample)
  T10->>T10: Validate/Compute/Output
  T50->>Buf: Get()
  T50->>T50: Health monitoring / BIT

2.2 Ravenscar Profile : Ada temps réel déterministe (sous-ensemble)

Ravenscar est un profil (ensemble de restrictions) visant à rendre la concurrence Ada prévisible et plus facile à analyser (schedulability / WCET / contention).

Pourquoi un profil ?

But	Ce qu’on restreint	Bénéfice
Scheduling prouvable	constructions de tâche trop dynamiques	analyse plus simple
Latence bornée	rendezvous complexes / comportements imprévisibles	jitter réduit
Auditabilité	patterns “magiques” ou implicites	comportements plus lisibles

En avionique, la question n’est pas “peut-on le coder ?” mais “peut-on le prouver et le maintenir sur 20 ans ?”.

2.3 SPARK : Ada + preuves formelles (contrats, absence d’erreurs runtime)

Ce que SPARK apporte

Contrats (pré/post-conditions, invariants) : spécification proche du code.
Analyse formelle : prouver absence de certaines erreurs (selon niveau d’usage).
Moins d’ambiguïté : le code devient “evidence-friendly”.

SPARK n’est pas “magique” : on choisit des sous-ensembles, on structure, on prouve ce qui est critique, et on garde des tests/coverage en complément.

Exemple (style contrats Ada 2012 / SPARK-like)

subtype Feet is Integer range 0 .. 60_000;

function Clamp_Feet (V : Integer) return Feet
  with
    Pre  => True,
    Post => (Clamp_Feet'Result in Feet);

function Clamp_Feet (V : Integer) return Feet is
begin
   if V < Feet'First then
      return Feet'First;
   elsif V > Feet'Last then
      return Feet'Last;
   else
      return Feet(V); -- explicit conversion
   end if;
end Clamp_Feet;

Lecture deterministic : bornage explicite + types/ranges + conversion contrôlée = comportement stable et auditable.

Comment SPARK s’intègre au process (vue avionique)

flowchart LR
  Req[Requirements] --> Spec[Ada spec + contracts]
  Spec --> Impl[Ada/SPARK Implementation]
  Impl --> Proof[Formal analysis / proofs]
  Impl --> Tests[Unit + Integration tests]
  Impl --> Cov[Coverage (if required)]
  Proof --> Pkg[Evidence package]
  Tests --> Pkg
  Cov --> Pkg

En pratique : proofs + tests + coverage + traceability. On cumule les preuves, on ne remplace pas tout par du “formel”.

3.1 Domaines avioniques : où Ada est pertinent

Zones typiques safety-critical

Domaine	Pourquoi Ada	Contraintes
Flight Control	typage + modularité + concurrence maîtrisée	latence, dégradations, modes
Navigation / Mission	maintenabilité long terme	interfaces strictes, intégration
Calculateurs RT	modèle de tâches robuste	schedulability, contention
Safety monitors	contrats + invariants (SPARK)	preuves, tests, audit

Pattern (concept) : boucle de contrôle + monitoring séparé

flowchart LR
  CL[Control loop task] --> OUT[Actuators]
  IN[Sensors] --> CL
  CL --> DIAG[Diagnostics flags]
  DIAG --> MON[Monitoring task]
  MON --> LOG[Bounded logging]

3.2 Ada vs Deterministic C (lecture engineering)

Table comparatif (haut niveau)

Critère	Ada	Deterministic C
Safety by design	fort (typage, packages, checks)	faible → dépend des règles (MISRA/CERT)
Concurrence	primitives langage (tasks/protected)	via RTOS + discipline + patterns
UB / surprises	moins de zones “dangereuses”	fort risque si non profilé
Auditabilité	très bonne (spec/bodies)	bonne si code strict + outillage
Écosystème avionique	historique & niche	massif & dominant
Proof (SPARK)	excellent (selon périmètre)	possible mais plus “artisanal”

Conclusion pratique : Ada peut réduire le coût de sûreté via le design du langage, tandis que le C impose une discipline stricte (règles + tooling + V&V). Les deux peuvent être certifiés, l’optimisation dépend du contexte.

3.3 Tooling : GNAT, build, analyses, coverage, CI

Pipeline concept (Ada safety-critical)

1) Build (warnings strict)
2) Static checks (style + rules internes)
3) Unit tests + reports
4) Integration tests (target/HIL)
5) Coverage (selon criticité)
6) Traceability & evidence package (process DO-178C)

Table : livrables “audit-friendly”

Objet	Pourquoi
spec Ada	contrat d’interface clair et stable
rapports tests	preuve de vérification
coverage	preuve structurelle (selon exigence)
analyses	détection classes d’erreurs + justifications

Même avec Ada, en certification : ce qui compte est le process + preuves. Ada rend souvent les preuves plus “propres”.

4.1 Checklist Ada safety-critical (revue de code & conception)

[Ada Safety-Critical Checklist]

A) Types & Ranges
- [ ] Use subtypes with ranges for domain values (Feet, Degrees, etc.)
- [ ] Avoid "raw Integer" in interfaces; prefer strong domain types
- [ ] Explicit conversions only; document rationale

B) Exceptions & Error Handling
- [ ] Define a strategy: avoid exceptions in control loop (or strictly bound them)
- [ ] Return status codes or use controlled error channels
- [ ] No hidden exception propagation across safety boundaries

C) Concurrency (RT)
- [ ] Prefer protected objects for shared data
- [ ] Keep critical sections short and bounded
- [ ] Consider Ravenscar restrictions (if applicable) for analyzability

D) Determinism / Timing
- [ ] Bounded loops; no unbounded waiting
- [ ] Separate control loop tasks from monitoring/logging
- [ ] Ensure any IO is bounded and budgeted

E) Verification
- [ ] Unit tests cover edge cases (ranges, conversions, boundary values)
- [ ] Traceability Req -> Spec -> Code -> Tests -> Reports
- [ ] Coverage evidence as required

4.2 Mini-projet : capteur → normalisation → clamp (Ada package complet)

Spec : types domaine + API

package Sensor_Norm is
   subtype Raw is Integer range 0 .. 4095;

   subtype Q15 is Integer range -32768 .. 32767;

   type Diag is record
      Invalid_Count : Natural := 0;
      Invalid_Range : Boolean := False;
   end record;

   function Normalize_Q15 (R : Raw; Min : Raw; Max : Raw; D : in out Diag) return Q15;
end Sensor_Norm;

Body : normalisation bornée, “safe default”

package body Sensor_Norm is

   function Clamp_Q15 (V : Integer) return Q15 is
   begin
      if V < Q15'First then
         return Q15'First;
      elsif V > Q15'Last then
         return Q15'Last;
      else
         return Q15(V);
      end if;
   end Clamp_Q15;

   function Normalize_Q15 (R : Raw; Min : Raw; Max : Raw; D : in out Diag) return Q15 is
      Num : Integer;
      Den : Integer;
      V   : Integer;
   begin
      if Min >= Max then
         D.Invalid_Count := D.Invalid_Count + 1;
         D.Invalid_Range := True;
         return 0; -- safe default
      end if;

      if (R < Min) or else (R > Max) then
         D.Invalid_Count := D.Invalid_Count + 1;
         D.Invalid_Range := True;
         return 0; -- safe default
      end if;

      Num := Integer(R - Min);
      Den := Integer(Max - Min);

      -- map to [0..65535] then shift to [-32768..32767]
      V := (Num * 65535) / Den;
      V := V - 32768;

      return Clamp_Q15(V);
   end Normalize_Q15;

end Sensor_Norm;

Version “contracts” (style Ada 2012 / SPARK-like)

-- Example contract idea:
-- Normalize_Q15 returns a value always in Q15 range (guaranteed by subtype)
-- and sets diagnostics deterministically.

-- In real SPARK usage, you would add precise contracts, invariants,
-- and forbid or control certain features for proof.

En safety-critical, l’intérêt : la spec est déjà “proche requirement”, et les types imposent des invariants.

4.3 Références & ressources (Ada / SPARK / Real-time)

Points d’entrée (liens à ajuster selon ta politique de sources IDEO-Lab).

Si tu veux un bloc “références officielles normatives” plus strict (DO-178C/DO-330/DO-331), je te le structure aussi.

⚙️ Quickstart Ada (style avionique)

1) Model your domains with subtypes + ranges (Feet, Degrees, Q15...)
2) Put stable interfaces in package specs; keep bodies small & testable
3) Prefer explicit conversions; avoid "Integer everywhere"
4) Decide your exception strategy early (often: avoid in control loop)
5) Use protected objects for shared data; tasks for periodic work
6) Consider Ravenscar (or similar restrictions) for analyzability
7) Bound loops and waiting; keep real-time path deterministic
8) Separate control loop and monitoring/logging tasks
9) Add contracts (Ada 2012) where it clarifies intent
10) Evidence-driven: tests, coverage, traceability, reports

🛡️ Ada – Safety-Critical Avionics

Ada : le langage “engineered for correctness”.

Évolution : Ada 83 → 95 → 2005 → 2012

Concepts fondamentaux

Pourquoi Ada est “safety-friendly”

Concurrence & temps réel (tasks, protected)

Ravenscar Profile

SPARK : preuves formelles

Domaines avioniques

Ada vs Deterministic C

GNAT / Toolchain & certification

Checklist Ada safety-critical

Mini-projet : capteur → normalisation → clamp

Références & ressources