DO-178C Compliance in Lyx

Die DO-178C ist der primäre Standard der Luftfahrtbehörden (EASA, FAA) zur Zertifizierung von Software in fliegenden Systemen. Lyx wurde entwickelt, um die Einhaltung dieses Standards durch native Sprachfeatures und Compiler-Garantien zu unterstützen.

1. Design Assurance Levels (DAL)

Der Standard teilt Software nach der Kritikalität der Auswirkungen eines Fehlers in Stufen ein. Lyx ermöglicht die Annotation dieser Stufen direkt im Quellcode über das Pragma @dal(Level).

Level	Kritikalität	Beschreibung in Lyx
A	Katastrophal	Höchstes Sicherheitslevel. Erfordert zwingend `@critical` und meist `@integrity`.
B	Gefährlich	Hohe Anforderungen an Testabdeckung und Determination.
C	Major	Moderate Sicherheitsanforderungen.
D	Minor	Niedrigste zertifizierungsrelevante Stufe.

2. Deterministische Ausführung

Ein Kernaspekt von DO-178C ist die Vorhersehbarkeit (Determinisitik). Lyx erzwingt dies durch:

Bounded Loops (@limit)

Schleifen in sicherheitskritischen Sektionen müssen ein festes Iterationslimit haben, um die Berechnung der WCET (Worst-Case Execution Time) zu ermöglichen.

while (sensor_data == null) limit(100) { 
    poll_sensor(); 
}

Floating-Point Determinisitik (@flight_crit)

Das Attribut @flight_crit garantiert ein konsistentes Rundungsverhalten der FPU (Floating Point Unit) und deaktiviert unsichere Optimierungen wie Constant Folding für Fließkommazahlen.

3. Safety-Pragmas & Überprüfung

Lyx-Funktionen können mit spezifischen Metadaten annotiert werden, die der Compiler gegen die Zielarchitektur validiert:

@wcet(N): Definiert das Zeitbudget in Mikrosekunden.
@stack_limit(N): Begrenzt die maximale Stack-Nutzung in Bytes, um Stack-Overflows (ein häufiger Verstoß gegen Safety-Guidelines) zu verhindern.
@critical: Markiert Funktionen, die für den Flugbetrieb essenziell sind; diese dürfen keine extern fn aufrufen.

4. Datensicherheit & Range-Types

Um ungültige Zustände (Out-of-Bounds) zu vermeiden, nutzt Lyx Range-Typen. Diese erlauben die Definition von aeronautischen Wertebereichen mit strikter Prüfung:

type Altitude = int64 range -1000..60000; // Meter über MSL
type Speed    = int64 range 0..300;       // Knoten

Compile-Time: Literale außerhalb des Bereichs führen zu Fehlern.
Runtime: Dynamische Werte werden per IR-Check geprüft; bei Verletzung erfolgt ein kontrollierter panic.

5. Hardware-Fehlertoleranz (Integrity)

DO-178C fordert Mechanismen gegen Hardware-Ausfälle. Lyx implementiert hierfür:

TMR (Triple Modular Redundancy) für Variablen über @redundant.
Software Lockstep für die redundante Ausführung kritischer Pfade.
Memory Scrubbing zur Erkennung von Bit-Flips im Programmcode.