====== 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:guides:do-178c:triple_modular_redundancy|TMR]] · [[lyx_-_programmiersprache:guides:do-178c:software-lockstep|Software Lockstep]] · [[lyx_-_programmiersprache:guides:do-178c:memory-scrubbing|Memory Scrubbing]] · [[lyx_-_programmiersprache:guides:do-178c:meta_safe|.meta_safe ELF-Sektion]]\\ → Ergänzend: [[lyx_-_programmiersprache:guides:aerospace-safety|Aerospace Safety]] · [[lyx_-_programmiersprache:tools:compiler-parameter|CLI-Referenz]] · [[lyx_-_programmiersprache:guides: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) @stack_limit(4096) @wcet(500) fn ComputeFlightPath(state: int64): 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'' ([[lyx_-_programmiersprache:sprache:attributes-pragmas|Attributes & Pragmas]]) 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 | | Keine FPU-Umordnung | Gilt für diese Funktion; ein globales Flag dafür gibt es nicht | @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:guides:aerospace-safety|Aerospace & Safety]] > **Was ''@flight_crit'' statisch prüft.** Im Rumpf werden ''new'', ''alloc'' und lokale Felder abgewiesen (seit [[https://github.com/SEOLizer/LyX-Compiler/issues/1529|#1529]]). Seit ''lyxc 1.1.4A'' reicht die Prüfung darüber hinaus **transitiv** durch die Aufrufkette ([[https://github.com/SEOLizer/LyX-Compiler/issues/1701|#1701]], nachgemessen mit 1.1.11B): ein Helfer, der alloziert, wird gemeldet, auch zwei Ebenen tief; ein Aufruf über einen Funktionszeiger wird abgewiesen, weil sein Sprungziel erst zur Laufzeit feststeht. > > Für den Nachweis heißt das: Die Grenze der Prüfung ist nicht mehr die Aufrufgrenze. Wer eine Funktion trotzdem ausdrücklich als kritisch führen will, markiert sie zusätzlich selbst mit ''@flight_crit''. ---- ===== 3. WCET & Stack-Limit ===== Laufzeit- und Stack-Budgets für sicherheitskritischen Code: ==== @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: int64): SensorReading { // Der Compiler prüft: Kann diese Funktion in 100 µs abgeschlossen werden? // Scheitern → Compile-Error mit Pfad-Angabe der teuersten Instruktionssequenz var _r: SensorReading; _r.ax := imu.raw_ax; _r.ay := imu.raw_ay; _r.az := imu.raw_az; return _r; } Ausgabe bei Überschreitung (Beispiel): error[E0412]: WCET budget exceeded in ReadIMU --> imu_driver.lyx:12:1 | 12 | fn ReadIMU(imu: int64): 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: int64): 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 := WaypointDistance(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 ([[lyx_-_programmiersprache:sprache:typaliase-und-typumwandlung|Typaliase & Typumwandlung]]) 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:guides: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) fn ComputeFlightPath(state: int64): 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 — **ohne** ''interval'', geprueft wird vor jedem ''return'' | | ''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:guides:do-178c:software-lockstep|Software Lockstep — vollständige Dokumentation]]\\ → [[lyx_-_programmiersprache:guides: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 dem Lyx-Compiler ==== **Seit 1.0.20F zählt ''--mcdc-report'' die Bedingungen richtig** (#1524) — die Rechnung oben deckt sich jetzt mit dem Werkzeug: [MC/DC] Eins: 1 decisions, 1 conditions → min 2 test cases [MC/DC] Zwei: 1 decisions, 2 conditions → min 3 test cases [MC/DC] Drei: 1 decisions, 3 conditions → min 4 test cases **Zwei Einschränkungen bleiben:** * **Entscheidungen in einem ''return''-Ausdruck werden nicht erfasst.** Gesehen werden nur ''if''- und ''while''-Köpfe. Die Funktion ''IsLandingAllowed'' von oben taucht im Bericht in keiner Zeile auf — eine Funktion, die ihre Logik im Rückgabeausdruck trägt, gilt als entscheidungsfrei. Das ist der gefährlichere der beiden Fälle, weil „keine Entscheidungspunkte" wie ein erledigter Nachweis aussieht. * **''--mcdc'' baut keine Instrumentierung ein.** Das Programm ist mit und ohne den Schalter byte-identisch; es gibt also nichts, was zur Laufzeit Überdeckung aufzeichnen könnte, und folglich keine Coverage-Datenbank. Für den Nachweis heißt das: die **Struktur** liefert der Compiler jetzt verlässlich, sofern die Entscheidung in einem ''if'' oder ''while'' steht. Die **Überdeckung** ist weiterhin außerhalb zu belegen. Was der Compiler heute liefert, ist eine **Strukturübersicht** der Entscheidungspunkte in ''if''/''while'': lyxc --mcdc-report src/flight_control.lyx -o /dev/null [MC/DC] Coverage structure analysis [MC/DC] Functions analyzed: 3 [MC/DC] Total decision points: 3 [MC/DC] Fakultaet: 1 decisions, 1 conditions → min 2 test cases [MC/DC] Decision point details: [MC/DC] point #0 in 'Fakultaet': if (node 6) Nützlich, um Entscheidungspunkte aufzufinden. Für den Überdeckungsnachweis nach DO-178C Level A müssen die Bedingungen einer Entscheidung **von Hand** aufgeschlüsselt und die Testvektoren selbst hergeleitet werden — die Tabelle weiter oben zeigt, wie das für drei Bedingungen aussieht. ''--mcdc-instrument'' und ''--coverage-report'' aus früheren Fassungen dieses Guides gibt es nicht; eine HTML-Aufbereitung ebenso wenig. ---- ===== 8. Compiler-Flags für DO-178C ===== Von den Flags, die frühere Fassungen dieses Guides nannten, existiert die Mehrzahl nicht. Es gibt **kein** ''--opt=N'', ''--flight-crit'', ''--stack-check'', ''--wcet'', ''--no-fp-fold'', ''--mcdc-instrument'', ''--coverage-report'' und ''--symbol-sizes'' — jedes davon bricht mit ''unbekannter Schalter'' und Exit 2 ab. Seit **1.0.20F** lässt sich der Nachweislauf dagegen **in einem Aufruf** führen: ''--provenance'' verändert das Erzeugnis nicht mehr (#1523), und ''--map-file'' arbeitet seit 1.0.20A. Allein ''--asm-listing'' bricht weiterhin ab (#1370). ==== DAL-A Build (Produktion) ==== lyxc src/flight_control.lyx \ --target=arm64 \ --call-graph \ --static-analysis \ --verify-tmr \ --runtime-checks \ --lint \ --mcdc-report \ --provenance \ --map-file \ -o evidence/fcc.elf > evidence/analyse.log 2>&1 Analysen, Traceability-Protokoll, Speicherkarte und Auslieferungsstand entstehen damit im **selben Übersetzungslauf** — das schließt die Lücke, die frühere Fassungen dieses Guides vermerken mussten: dass die geprüften Artefakte und das ausgelieferte Programm aus verschiedenen Läufen stammten und ihre Gleichheit nur angenommen war. > Ein Assembly-Listing (DO-178C 6.1) liefert der Compiler nicht (#1370). Ersatz: ''objdump -d evidence/fcc.elf''. Die Speicherkarte steht nach dem Lauf in ''evidence/fcc.elf.map''. Zu ''--flight-crit'' und ''--no-fp-fold'': beides sind **Attribute im Quelltext**, keine Schalter. ''@flight_crit'' an einer Funktion schaltet die SSE-Ausnahmen frei und unterbindet die Fließkomma-Umordnung für diese Funktion (→ [[lyx_-_programmiersprache:sprache:attributes-pragmas|Attribute]]). Ebenso ''@stack_limit'' und ''@wcet'': deren Nachweis führt der Compiler bei **jeder** Übersetzung, ganz ohne Flag. ==== DAL-C Build (Testsystem) ==== lyxc src/flight_control.lyx \ --target=linux \ --runtime-checks \ --lint \ -o test/flight_control_test Ein ''--opt=0'' gibt es nicht; das Gegenstück heißt ''-O0'' oder ''--no-opt'' und schaltet seit 1.0.20A die Vereinfachungen des Codegens ab (Konstantenfaltung, tote Zweige, #1371). Für eine Überdeckungsmessung ist das die richtige Wahl, weil der erzeugte Code dann Zeile für Zeile der Quelle folgt. Die Stufen ''-O1'' bis ''-O3'' unterscheiden sich untereinander nicht. ==== Coverage-Nachweis erzeugen ==== **Den Laufzeitnachweis der Überdeckung liefert der Compiler weiterhin nicht.** ''--mcdc'' baut keine Instrumentierung ein — das Programm ist mit und ohne den Schalter byte-identisch; es gibt also keine Coverage-Datenbank und keine HTML-Aufbereitung. Was ''--mcdc-report'' seit 1.0.20F liefert, ist die **Struktur**: Entscheidungspunkte, Zahl der Bedingungen je Entscheidung und die daraus folgende Mindestzahl an Testfällen (#1524). Das ist die halbe Arbeit — die Testvektoren lassen sich daraus herleiten, ihre tatsächliche Ausführung muss ein Testrahmenwerk belegen, das die Ergebnisse jeder Bedingungskombination mitschreibt. Zu beachten: erfasst werden nur ''if''- und ''while''-Köpfe. Eine Entscheidung in einem ''return''-Ausdruck taucht im Bericht **nicht** auf. Vollständige Flag-Referenz: → [[lyx_-_programmiersprache:tools: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 ^ Weg ^ Stand ^ | Call Graph (Pfadanalyse) | Aufrufgraph | ''--call-graph'' | **verfügbar** | | Stack Usage Analysis | ''@stack_limit'' | kein Flag — wird bei jeder Übersetzung geprüft | **verfügbar** | | WCET Analysis | ''@wcet'' | kein Flag — wird bei jeder Übersetzung geprüft | **verfügbar** | | TMR Verification | ''@redundant'' | ''--verify-tmr'' | **verfügbar** | | Data-Flow / Live-Variablen | Quellcode | ''--static-analysis'' | **verfügbar** | | Laufzeitprüfungen | Quellcode | ''--runtime-checks'' | **verfügbar** | | Source Code Traceability | IR → AST → Quelle | ''--provenance'' | **verfügbar** — das Erzeugnis bleibt seit 1.0.20F unverändert (#1523); die Zuordnungsgenauigkeit vor dem Nachweis stichprobenartig prüfen | | MC/DC-Struktur (Entscheidungen, Bedingungen, Mindest-Testfälle) | ''if''/''while''-Köpfe | ''--mcdc-report'' | **verfügbar** seit 1.0.20F (#1524); Entscheidungen in ''return''-Ausdrücken fehlen | | MC/DC-Überdeckung (Laufzeitnachweis) | — | — | **fehlt** — ''--mcdc'' instrumentiert nicht | | Assembly Listing (Object Review) | — | ''--asm-listing'' bricht ab | **fehlt** (#1370) — Ersatz: ''objdump -d'' auf das Programm | | Memory Map | — | ''--map-file'' bricht ab | **fehlt** (#1370) — Ersatz: ''readelf -lW'' | | Symbol Sizes | — | ''--symbol-sizes'' existiert nicht | **fehlt** — Ersatz: ''nm --size-sort'' | Mit **1.0.20F** liefert der Compiler den größten Teil: Aufrufgraph, Stack- und WCET-Nachweis, TMR-Prüfung, Datenflussanalyse, Laufzeitprüfungen, Traceability und die MC/DC-**Struktur**. ''--map-file'' und ''--dump-relocs'' sind seit 1.0.20A ebenfalls da. Nicht geliefert werden weiterhin: das **Assembly-Listing** (''--asm-listing'', #1370 — Ersatz ''objdump -d'') und der **Laufzeitnachweis der MC/DC-Überdeckung**, weil ''--mcdc'' nicht instrumentiert. Letzterer ist für DAL A verpflichtend und außerhalb des Compilers zu erbringen. Zwei Einschränkungen gehören ins Prüfprotokoll: die MC/DC-Struktur erfasst nur ''if''- und ''while''-Köpfe, nicht Entscheidungen in ''return''-Ausdrücken; und die Zuordnungsgenauigkeit von ''--provenance'' sollte vor dem Nachweis stichprobenartig geprüft werden. Der Stand ist gegen lyxc 1.0.21A gemessen, jeder Schalter einzeln nachgerufen. 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; // Zustand, Stellgroessen und Navigationsdaten pub type FlightState = struct { altitude: int64; target_altitude: int64; }; pub type ControlCmd = struct { elevator: int64; throttle: int64; }; pub type GeoPoint = struct { lat: f64; lon: f64; }; pub type Waypoint = struct { pos: GeoPoint; name: pchar; }; // Platzhalter fuer die Entfernungsrechnung des Musters. Eine echte Anwendung // nimmt std.geo.sphere (Grosskreis) oder std.geodesy (Ellipsoid) — hier steht // eine Naeherung, damit das Beispiel fuer sich uebersetzt. fn WaypointDistance(a: GeoPoint, b: GeoPoint): f64 { var dlat: f64 := a.lat - b.lat; var dlon: f64 := a.lon - b.lon; return dlat * dlat + dlon * dlon; } // 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) @stack_limit(4096) @wcet(500) fn AutopilotCycle(state: FlightState, cmd: ControlCmd): 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 := WaypointDistance(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:guides:aerospace-safety|Aerospace & Safety — Safety-Attribute, Range-Typen, Bounded Loops, Best-Practices-Tabelle und vollständiges Regelkreis-Beispiel]]\\ → [[lyx_-_programmiersprache:guides:aerospace-tutorial|Aerospace Tutorial: Von der Anforderung zum Nachweis]] Letzte Aktualisierung: 2026-05-22 Codebeispiele geprüft: gegen **lyxc 1.2.5C** übersetzt (Prüflauf 2026-09-08 über die gesamte Doku: 574 Vollprogramme, 0 echte Fehler; zusätzlich 5159 Aufrufe gegen die ''pub fn''-Signaturen in ''aurum/std'' gehalten, 0 Abweichungen).