====== DO-178C Compliance in Lyx ====== **DO-178C** ("Software Considerations in Airborne Systems and Equipment Certification") ist der Industriestandard der Luftfahrtbehörden EASA (Europa) und FAA (USA) für Software in zugelassenen Luftfahrzeugen. Ohne Compliance keine Musterzulassung (Type Certificate). Lyx ist die erste eigenständige Systemsprache, die DO-178C-Konformität als integralen Bestandteil der Sprache — nicht als nachgelagertes Werkzeug — implementiert. → Unterseiten: [[lyx_-_programmiersprache:do-178c:triple_modular_redundancy|TMR]] · [[lyx_-_programmiersprache:do-178c:software-lockstep|Software Lockstep]] · [[lyx_-_programmiersprache:do-178c:memory-scrubbing|Memory Scrubbing]] · [[lyx_-_programmiersprache:do-178c:meta_safe|.meta_safe ELF-Sektion]]\\ → Ergänzend: [[lyx_-_programmiersprache:aerospace-safety|Aerospace Safety]] · [[lyx_-_programmiersprache:compiler-parameter|CLI-Referenz]] · [[lyx_-_programmiersprache:rtos-embedded-concurrency|Embedded & RTOS]] ---- ===== 1. Design Assurance Levels (DAL) ===== DO-178C teilt Software nach der **Auswirkung eines Ausfalls** auf das Flugzeug und seine Insassen ein. Je schwerwiegender der mögliche Schaden, desto strenger die Anforderungen. ^ DAL ^ Auswirkung ^ Coverage-Anforderung ^ Lyx-Anforderung ^ | **A** | Katastrophal — Totalverlust | Statement + Branch + MC/DC + Objektcode-Struktur | ''@dal(A)'', ''@flight_crit'', ''@integrity'', ''@redundant'' | | **B** | Gefährlich — schwere Verletzungen | Statement + Branch + MC/DC | ''@dal(B)'', ''@flight_crit'', ''@wcet'' | | **C** | Major — reduzierte Sicherheitsmarge | Statement + Branch | ''@dal(C)'', ''@stack_limit'' | | **D** | Minor — keine Sicherheitsrelevanz | Statement | ''@dal(D)'' | | **E** | No Safety Effect | Keine Coverage-Pflicht | Keine Lyx-Annotationen erforderlich | > **Wichtig:** DAL gilt immer für die **Funktion**, die den kritischsten Pfad im Fehlerbaum besetzt — nicht für das Gesamtsystem. Ein Telemetrie-Subsystem kann DAL-D sein, während der Autopilotkern DAL-A ist. ==== DAL in Lyx annotieren ==== // DAL-A: automatischer Pilot — katastrophaler Ausfall @dal(A) @flight_crit @integrity(mode: software_lockstep, interval: 50) @stack_limit(4096) @wcet(500) fn ComputeFlightPath(state: ^FlightState): FlightCommands { // ... } // DAL-C: Bordunterhaltung @dal(C) fn UpdateDisplayBrightness(lux: int64): void { // ... } Der Compiler verweigert den Build, wenn ''@dal(A)'' oder ''@dal(B)'' gesetzt ist, aber fehlende Safety-Pragmas die geforderte Absicherung nicht erfüllen. ---- ===== 2. @flight_crit — Floating-Point Determinismus ===== Fließkommaberechnungen sind auf verschiedenen Prozessoren, Compiler-Versionen und Optimierungsstufen **nicht garantiert reproduzierbar**. Selbst dasselbe Programm kann auf einem x86_64 mit AVX und auf ARM64 ohne FMA leicht abweichende Ergebnisse liefern — ein gravierendes Problem für Flugregelungssysteme. ''@flight_crit'' erzwingt auf annotierte Funktionen: ^ Maßnahme ^ Effekt ^ | FPU-Modus IEEE 754 round-to-nearest | Konsistentes Rundungsverhalten auf allen Targets | | Kein FMA (Fused Multiply-Add) | Kein Unterschied zwischen Plattformen mit/ohne FMA | | Kein Constant-Folding für FP | Berechnung zur Laufzeit, nicht zur Compile-Zeit | | Kein FP-CSE (Common Subexpression Elimination) | Kein Zusammenlegen von FP-Operationen | | ''--no-fp-fold'' implizit aktiv | Äquivalent zum Compiler-Flag für diese Funktion | @dal(B) @flight_crit @wcet(200) fn ComputeHeading(lat1: f64, lon1: f64, lat2: f64, lon2: f64): f64 { // Alle FP-Operationen hier sind IEEE-754-strikt und plattformidentisch. // Der Compiler darf KEINE FP-Optimierungen anwenden. let dlat: f64 := lat2 - lat1; let dlon: f64 := lon2 - lon1; return Atan2(dlat, dlon) * (180.0 / Pi); } > Ohne ''@flight_crit'' kann Lyx FP-Ausdrücke zusammenfalten, was auf manchen Plattformen zu Abweichungen in der letzten Dezimalstelle führt. Bei Flugregelungssystemen reicht das aus, um nach 1000 Iteration eine Abweichung von mehreren Metern zu erzeugen. → Praxisbeispiele mit ''@flight_crit'', ''@redundant'' und ''@integrity'' in einer vollständigen Flugsteuerungsfunktion: [[lyx_-_programmiersprache:aerospace-safety|Aerospace & Safety]] ---- ===== 3. WCET & Stack-Limit ===== ==== @wcet(N) — Worst-Case Execution Time ==== ''@wcet(N)'' deklariert das **maximale Zeitbudget** einer Funktion in Mikrosekunden. Der Compiler analysiert Kontrollfluss und Schleifengrenzen und verweigert den Build, wenn die statisch ermittelte WCET das Budget überschreitet. @dal(A) @flight_crit @wcet(100) // max. 100 µs auf der Zielplattform @stack_limit(512) fn ReadIMU(imu: ^IMUState): SensorReading { // Der Compiler prüft: Kann diese Funktion in 100 µs abgeschlossen werden? // Scheitern → Compile-Error mit Pfad-Angabe der teuersten Instruktionssequenz return SensorReading { ax: imu.raw_ax, ay: imu.raw_ay, az: imu.raw_az }; } Ausgabe bei Überschreitung (Beispiel): error[E0412]: WCET budget exceeded in ReadIMU --> imu_driver.lyx:12:1 | 12 | fn ReadIMU(imu: ^IMUState): SensorReading { | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ | Estimated WCET: 143 µs (budget: 100 µs) | Critical path: ReadIMU → FilterKalman → MatMul3x3 | ^~~~~~~~~~~~~~~~~~~~~~~~~~~~ 98 µs hint: Split FilterKalman into a separate @wcet-annotated function or raise the budget. ==== @stack_limit(N) — Maximaler Stack-Verbrauch ==== Stack-Overflows gehören zu den häufigsten Ausfallursachen in eingebetteten Systemen. ''@stack_limit(N)'' lässt den Compiler den maximalen Stack-Verbrauch der Funktion und aller von ihr direkt aufgerufenen (nicht-externen) Funktionen berechnen: @dal(A) @flight_crit @stack_limit(2048) // max. 2048 Byte Stack (inkl. Callees) fn AutopilotCycle(state: ^FlightState): FlightCommands { // Compiler addiert: eigener Frame + alle Callees-Frames // Bei Überschreitung: Compile-Error } > Auf DO-178C DAL-A ist ''@stack_limit'' **zwingend** für alle Funktionen, die im Avionik-Partitionsspeicher laufen. Der Nachweis, dass kein Stack-Overflow auftreten kann, ist Bestandteil der Structural Coverage Analysis. ---- ===== 4. Bounded Loops — WCET-Voraussetzung ===== WCET-Analyse ist nur möglich, wenn alle Schleifen eine nachweisbare Obergrenze haben. Lyx erzwingt das mit dem ''limit''-Schlüsselwort. Schleifen ohne ''limit'' in ''@dal(A/B)''-Funktionen sind Compile-Errors. @dal(A) @flight_crit @wcet(50) fn FindNearestWaypoint(wps: [16]Waypoint, n: int64, pos: GeoPoint): int64 { var best: int64 := 0; var best_dist: f64 := 1.0e18; for i := 0 to n - 1 do { var d: f64 := GeoDistance(pos, wps[i].pos); if (d < best_dist) { best_dist := d; best := i; } } // for...to impliziert limit(n) — aber n muss zur Compile-Zeit bounded sein // Statische Arrays [16] sind bounded: Der Compiler kennt n <= 16 return best; } Für ''while''-Schleifen ist ''limit'' explizit erforderlich: // Sensor-Polling mit explizitem Limit while (ReadSensorReady() = false) limit(1000) { // Maximal 1000 Iterationen — WCET berechenbar } ---- ===== 5. Range-Typen ===== Out-of-Range-Werte sind eine Hauptursache für Flugunfälle (z.B. falscher Einheitenname, falsche Skala). Lyx-Range-Typen machen solche Fehler zur Compile-Zeit oder kontrollierten Laufzeit-Exceptions. // Physikalisch sinnvolle Bereiche type Altitude = int64 range -1000..60000; // Meter über MSL (Mariana-Graben bis Max.-Strat.) type Speed = int64 range 0..1000; // Knoten type Heading = f64 range 0.0..360.0; // Grad (echt: wrap-around — separate Logik) type BankAngle = f64 range -90.0..90.0; // Grad type ThrottlePct = int64 range 0..100; // Prozent fn ClimbTo(target: Altitude): void { // Compile-Fehler: Literal außerhalb des Bereichs // var bad: Altitude := 70000; // Error: 70000 > 60000 } fn ProcessSensor(raw_meters: int64): void { var alt: Altitude := raw_meters as Altitude; // Runtime-Prüfung: Falls raw_meters außerhalb [-1000, 60000] → panic // In DAL-A: panic löst kontrollierten Recovery-Pfad aus statt Absturz } Range-Typen sind kompatibel mit dem Basis-Ganzzahltyp — Arithmetik funktioniert transparent, das Ergebnis wird erneut geprüft: var current_alt: Altitude := 1000; var delta: int64 := 500; var new_alt: Altitude := (current_alt + delta) as Altitude; // Prüfung bei Zuweisung ---- ===== 6. Hardware-Fehlertoleranz ===== DO-178C verlangt für DAL-A, dass single-point failures im Hardware (Bit-Flips durch kosmische Strahlung, Speicherfehler) erkannt oder toleriert werden. ==== @redundant — TMR für Variablen ==== ''@redundant'' legt eine Variable dreifach im RAM an. Jeder Lesezugriff führt einen Mehrheitsentscheid durch: @redundant var thrust_setpoint: int64 := 0; // Intern: 3 physisch getrennte Kopien // Schreiben: alle drei Kopien werden simultan aktualisiert thrust_setpoint := 850; // Lesen: Compiler fügt Majority-Vote-Code ein var t: int64 := thrust_setpoint; // → vote(copy1, copy2, copy3) Eine abweichende Kopie wird zur Laufzeit automatisch repariert (Self-Healing). → Vollständige Dokumentation: [[lyx_-_programmiersprache:do-178c:triple_modular_redundancy|Triple Modular Redundancy]] ==== @integrity — Code- und Berechnungsintegrität ==== ''@integrity'' schützt entweder die **Rechenlogik** (software_lockstep) oder das **Code-Segment im RAM** (scrubbed): // Schutz der Berechnung: Jede ALU/FPU-Operation wird dupliziert und verglichen @dal(A) @flight_crit @integrity(mode: software_lockstep, interval: 50) fn ComputeFlightPath(state: ^FlightState): FlightCommands { // Compiler generiert: Primar- und Redundanz-Berechnung, Vergleich vor return } // Schutz des Code-Segments: periodischer CRC32-Sweep alle 100 ms @integrity(mode: scrubbed, interval: 100) unit nav.core; Modi im Überblick: ^ Modus ^ Schützt ^ Overhead ^ Wann einsetzen ^ | ''software_lockstep'' | ALU/FPU-Berechnungen | ~2× WCET | DAL-A Kernberechnungen | | ''scrubbed'' | Code-Segment im RAM (Bit-Flips) | Gering (Hintergrund) | DAL-A/B Units auf Embedded | | ''hardware_ecc'' | RAM (durch ECC-Hardware) | Keiner (Hardware) | DAL-A mit ECC-RAM | → [[lyx_-_programmiersprache:do-178c:software-lockstep|Software Lockstep — vollständige Dokumentation]]\\ → [[lyx_-_programmiersprache:do-178c:memory-scrubbing|Memory Scrubbing — vollständige Dokumentation]] ---- ===== 7. MC/DC Coverage ===== **Modified Condition/Decision Coverage (MC/DC)** ist die härteste Software-Coverage-Anforderung im kommerziellen Bereich. DO-178C verlangt MC/DC für DAL-A und DAL-B. MC/DC bedeutet: Für jede boolesche Bedingung in jeder Entscheidung muss ein Testfall existieren, der zeigt, dass diese **eine** Bedingung allein das Ergebnis der Entscheidung ändern kann — unabhängig von allen anderen Bedingungen. ==== Beispiel: MC/DC-Analyse ==== // Entscheidung mit drei Bedingungen fn IsLandingAllowed(gear_down: bool, speed_ok: bool, runway_clear: bool): bool { return gear_down & speed_ok & runway_clear; } Für MC/DC dieser Funktion braucht man **4 Testfälle** (nicht 8 wie für volle Branch Coverage): ^ Test ^ gear_down ^ speed_ok ^ runway_clear ^ Ergebnis ^ Zeigt MC/DC für ^ | T1 | true | true | true | true | Basis | | T2 | false | true | true | false | gear_down unabhängig | | T3 | true | false | true | false | speed_ok unabhängig | | T4 | true | true | false | false | runway_clear unabhängig | ==== MC/DC mit Lyx-Compiler ==== // MC/DC-Instrumentierung einschalten: // lyxc --mcdc-instrument --coverage-report=coverage.json src/flight_control.lyx // Nach dem Testlauf: // lyxc --coverage-report-html=report/ coverage.json // → Zeigt für jede Bedingung: welche Test-Vektoren sie abdecken Der ''--mcdc-instrument''-Flag fügt Instrumentierungs-Code ein, der zur Laufzeit für jeden ausgeführten Zweig einen Eintrag in eine Coverage-Datenbank schreibt. ''--coverage-report'' liest diese Datenbank und erzeugt den Nachweis für die Zertifizierungsbehörde. ---- ===== 8. Compiler-Flags für DO-178C ===== Ein vollständiger DO-178C-konformer Build setzt mehrere Flags zusammen: ==== DAL-A Build (Produktion) ==== // lyxc \ // --target=arm64 \ // --opt=2 \ // --flight-crit \ # Alle FP-Operationen IEEE-754-strikt // --stack-check \ # Stack-Limit aller @stack_limit-Funktionen prüfen // --wcet \ # WCET aller @wcet-Funktionen analysieren // --call-graph \ # Call-Graph erzeugen (für WCET-Pfad-Nachweis) // --mcdc-instrument \ # MC/DC-Instrumentierung einbetten // --no-fp-fold \ # FP-Constant-Folding global deaktivieren // --provenance \ # Quellzuordnung für jede Instruktion (Traceability) // --verify-tmr \ # @redundant-Variablen auf korrekte TMR-Implementierung prüfen // --emit-asm \ # Assembler-Output für DO-178C Objective Review // src/flight_control.lyx ==== DAL-C Build (Testsystem) ==== // lyxc \ // --target=x86_64 \ // --opt=0 \ # Keine Optimierungen — Coverage bleibt sauber // --stack-check \ // --mcdc-instrument \ // --coverage-report=cov.json \ // src/flight_control.lyx ==== Coverage-Nachweis erzeugen ==== // 1. Testlauf: ./flight_control_test // Erzeugt: coverage_raw.bin // 2. Report bauen: // lyxc --coverage-report=cov.json coverage_raw.bin // lyxc --coverage-report-html=report/ cov.json // 3. Ergebnis: report/index.html // Enthält: Statement-, Branch- und MC/DC-Abdeckung pro Funktion // Vollständige Quellzuordnung via --provenance Vollständige Flag-Referenz: → [[lyx_-_programmiersprache:compiler-parameter|CLI-Referenz]] ---- ===== 9. Qualifikations-Evidenz — Was Lyx erzeugt ===== DO-178C verlangt eine strukturierte Menge von Nachweis-Dokumenten (Evidence). Lyx-Compiler-Outputs decken die technischen Artefakte ab: ^ DO-178C Artefakt ^ Lyx-Quelle ^ Flag ^ | Source Code Traceability | Quellcode + ''@dal''-Annotationen | ''--provenance'' | | WCET Analysis | Compiler-WCET-Report | ''--wcet'' + ''--call-graph'' | | Stack Usage Analysis | Stack-Check-Report | ''--stack-check'' | | MC/DC Coverage Report | Coverage-Datenbank → HTML | ''--mcdc-instrument'' + ''--coverage-report'' | | Assembly Listing (Object Review) | Assembler-Output | ''--emit-asm'' | | Symbol Sizes | Symbol-Tabelle | ''--symbol-sizes'' | | TMR Verification | TMR-Prüf-Report | ''--verify-tmr'' | | Call Graph | Aufruf-Graph (für Pfadanalyse) | ''--call-graph'' | Die Planung- und Prozess-Dokumente (PSAC, SDP, SVP, SCI) entstehen außerhalb des Compilers — Lyx liefert die technischen Daten, auf die diese Dokumente verweisen. ---- ===== 10. DO-178C in Lyx — Gesamtbild ===== unit flight_control; import std.io; // Unit-Level: Code-Segment-Integrität @integrity(mode: scrubbed, interval: 100) // Typen mit physikalischen Grenzen type Altitude = int64 range -1000..60000; type Speed = int64 range 0..1000; // Kritische Zustandsvariable — dreifach im RAM @redundant var autopilot_active: bool := false; // DAL-A Kernfunktion — alle Safety-Pragmas gesetzt @dal(A) @flight_crit @integrity(mode: software_lockstep, interval: 50) @stack_limit(4096) @wcet(500) fn AutopilotCycle(state: ^FlightState, cmd: ^FlightCommands): void { if (autopilot_active = false) { return; } var target_alt: Altitude := state.target_altitude as Altitude; var cur_alt: Altitude := state.altitude as Altitude; var delta: int64 := target_alt - cur_alt; // Berechnung — dupliziert und verglichen (software_lockstep) cmd.elevator := Clamp(delta / 100, -30, 30) as int64; cmd.throttle := Clamp(500 + delta / 10, 0, 1000) as int64; } // DAL-B Navigationsfunktion @dal(B) @flight_crit @wcet(200) @stack_limit(2048) fn FindNearestWaypoint(wps: [32]Waypoint, n: int64, pos: GeoPoint): int64 { var best: int64 := 0; var best_d: f64 := 1.0e18; for i := 0 to n - 1 do { var d: f64 := GeoDistance(pos, wps[i].pos); if (d < best_d) { best_d := d; best := i; } } return best; } fn main(): int64 { // Integritätsprüfung beim Start if (VerifyIntegrity() = false) { panic("Code corruption detected — switching to backup computer"); } // ... Hauptschleife ... return 0; } ---- → [[lyx_-_programmiersprache:aerospace-safety|Aerospace & Safety — Safety-Attribute, Range-Typen, Bounded Loops, Best-Practices-Tabelle und vollständiges Regelkreis-Beispiel]]\\ → [[lyx_-_programmiersprache:aerospace-tutorial|Aerospace Tutorial: Von der Anforderung zum Nachweis]] Letzte Aktualisierung: 2026-05-22