====== Aerospace & Safety ====== Lyx wurde von Grund auf für den Einsatz in sicherheitskritischen Systemen entworfen. Die Sprache und ihre Toolchain richten sich nach **DO-178C** — dem primären Standard der Luftfahrtbehörden EASA und FAA für die Zertifizierung von Avionik-Software. Viele der Sprachentscheidungen, die auf den ersten Blick wie bloße Stilwahl wirken — explizite Typisierung, kein Garbage Collector, vier Speicherklassen ([[lyx_-_programmiersprache:sprache:variablen|Variablen]]), Range-Typen — sind direkte Konsequenzen dieser Zieldomäne. Diese Seite erklärt, welche Werkzeuge Lyx für sicherheitskritische Entwicklung bereitstellt, warum sie so konzipiert sind und wie sie in der Praxis eingesetzt werden. → Technische Compliance-Referenz: [[lyx_-_programmiersprache:guides:do-178c|DO-178C — DAL-Stufen, MC/DC, WCET, TMR, Qualifikations-Evidenz]] → Rechnende Units: [[lyx_-_programmiersprache:units:aero|std.aero]] (Standardatmosphäre, Flugleistung, Flugführung) · [[lyx_-_programmiersprache:units:astro|std.astro]] (Bahnmechanik, Eintritt, Start) ---- ===== DO-178C und Design Assurance Levels ===== DO-178C teilt Software nach der Kritikalität eines möglichen Fehlers in fünf Stufen ein — die **Design Assurance Levels (DAL)**. Je höher die Stufe, desto strenger die Anforderungen an Testabdeckung, Dokumentation und Nachweisbarkeit. ^ DAL ^ Kritikalität ^ Konsequenz eines Fehlers ^ Typische Systeme ^ | **A** | Katastrophal | Verlust des Luftfahrzeugs oder Todesfolge | Primäre Flugsteuerung, TCAS | | **B** | Gefährlich | Ernsthafter Schaden, stark eingeschränkte Kontrolle | Autopilot, Triebwerkssteuerung | | **C** | Major | Signifikante Verschlechterung der Sicherheit | Navigation, Warnsysteme | | **D** | Minor | Geringe Auswirkung auf Sicherheit | Kabinenbeleuchtung, IFE | | **E** | No Safety Effect | Kein Einfluss auf Sicherheit | Entertainmentsysteme | In Lyx lässt sich das DAL direkt im Quellcode annotieren. Der Compiler und Linter passen ihre Prüfstrenge entsprechend an — bei DAL-A werden alle Safety-Regeln maximal strikt durchgesetzt: @dal(A) fn ComputeFlightPath(input: SensorData): FlightCommand { // Der Compiler erzwingt hier alle DAL-A-Constraints } → [[lyx_-_programmiersprache:guides:do-178c|DO-178C — vollständige Coverage-Anforderungen pro DAL, MC/DC-Workflow, Compiler-Flags und Qualifikations-Evidenz]] ---- ===== Safety-Attribute (@-Pragmas) ===== Lyx steuert sicherheitskritisches Verhalten über Attribute, die direkt an Funktionen, Units oder Variablen angehängt werden. Sie beginnen immer mit ''@'' und sind für den Compiler und Linter verbindlich — keine Kommentare, sondern geprüfte Constraints. ==== @flight_crit — Luftfahrt-Modus ==== ''@flight_crit'' ist das zentrale Sicherheits-Attribut (alle Attribute im Überblick: [[lyx_-_programmiersprache:sprache:attributes-pragmas|Attributes & Pragmas]]). Es soll ein Set an Compiler-Einschränkungen aktivieren, die für Avionik-Code zwingend notwendig sind: * **Fließkomma-Ausnahmen:** Der Prolog schaltet die SSE-Ausnahmen für //invalid// (NaN) und //divide-by-zero// frei; eine entstehende NaN oder Inf löst SIGFPE aus, statt still weiterzurechnen. Fließkomma-Optimierungen (Constant Folding, Reordering) unterbleiben. * **Heap-Verbot:** als Vorsatz gedacht — **wird nicht durchgesetzt**, siehe Kasten. * **Kein FFI ohne Wrapper:** direkte ''@extern''-Aufrufe sollen verboten sein. Nachweislich wirksam ist der Fließkomma-Teil: @flight_crit fn D(a: f64, b: f64): f64 { return a / b; } $ ./fc4 panic: FPU-Ausnahme (NaN/Inf oder Division durch 0) unter @flight_crit in `D` $ echo $? 134 **Das Heap-Verbot besteht nicht** (#1529). ''new'', ''alloc()'' und lokale Felder werden innerhalb einer ''@flight_crit''-Funktion klaglos übersetzt — ohne Fehler und ohne Warnung. Hinzu kommt ein Umstand, der leicht übersehen wird: **ein lokales Feld liegt nicht auf dem Stapel.** ''var puffer: int64[100000]'' erzeugt bei jedem Aufruf ein ''mmap'' über 800 016 Byte: $ strace -e trace=mmap ./fc mmap(NULL, 800016, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = ... In einem Regelzyklus mit harter Frist ist das genau die Speicheranforderung, die ''@flight_crit'' verhindern soll. Wer Puffer im Zyklus braucht, legt sie **außerhalb** an und reicht sie herein — der Compiler erinnert nicht daran. @flight_crit fn ComputeAltitude(rawPressure: f64): f64 { // Alle Fließkomma-Operationen haben deterministisches Verhalten, // NaN und Division durch null loesen SIGFPE aus con SEA_LEVEL_PRESSURE: f64 := 101325.0; con SCALE_HEIGHT: f64 := 8500.0; return SCALE_HEIGHT * (1.0 - (rawPressure / SEA_LEVEL_PRESSURE)); } ==== @stack_limit — Stack-Overflow-Prävention ==== Stack-Overflows sind in eingebetteten Echtzeitsystemen eine häufige Fehlerquelle, die im Normalbetrieb nicht auftritt, aber unter Last katastrophal werden kann. ''@stack_limit(N)'' definiert das maximale Stack-Budget einer Funktion in Bytes. ''lyxc'' analysiert den Aufrufgraphen und stellt statisch sicher, dass dieses Limit eingehalten wird — **ohne jedes Flag, bei jeder Übersetzung**. Ein ''--stack-check'' gibt es nicht und braucht es nicht. > ''@stack_limit'' bilanziert den **Stapelrahmen**. Lokale Felder liegen nicht dort, sondern in einem ''mmap'' (siehe ''@flight_crit'' oben) und zählen deshalb nicht mit: ''@stack_limit(1)'' mit einem ''int64[100000]'' meldet „der Rahmen belegt 16 Byte" und geht durch. Das ist für den Stapel korrekt, ist aber allein kein Nachweis über den Speicherbedarf einer Funktion. @stack_limit(512) // max. 512 Byte Stack für diese Funktion inkl. aller Aufrufe fn ProcessSensorFrame(frame: SensorFrame): void { var filtered: f64 := KalmanFilter(frame.raw); var altitude: Altitude := ComputeAltitude(filtered) as int64; UpdateFlightLog(altitude); } Aufruf — die Prüfung läuft ohne Zutun mit: lyxc flight_ctrl.lyx -o flight_ctrl error: Fresser: @stack_limit(16) verletzt — der Rahmen belegt 32 Byte Rekursion lehnt der Compiler grundsätzlich ab, weil die Aufruftiefe dann nicht beschränkt ist: error: Rek: @stack_limit ist mit Rekursion nicht nachweisbar — die Aufruftiefe ist unbeschraenkt ==== @redundant — Triple Modular Redundancy (TMR) ==== Kosmische Strahlung und elektromagnetische Störfelder können einzelne Bits im RAM kippen (**Soft Errors** / Bit-Flips). In sicherheitskritischen Systemen können solche Ereignisse katastrophale Folgen haben. TMR schützt davor, indem ein Wert dreifach im Speicher abgelegt wird. Bei jedem Lesezugriff findet ein Mehrheitsentscheid statt — zwei von drei Kopien bestimmen den Ergebniswert. ''@redundant'' aktiviert diesen Mechanismus für eine Variable. Der Compiler generiert automatisch die dreifache Speicherung und die Voting-Logik: @flight_crit fn TrackHeading(input: f64): void { @redundant var heading: f64 := input; // 'heading' ist dreifach im RAM. Jeder Lesezugriff führt einen Vote durch. // Ein einzelner Bit-Flip beeinflusst das Ergebnis nicht. if (heading > 359.0) { heading := 0.0; } ApplyHeading(heading); } → [[lyx_-_programmiersprache:guides:do-178c:triple_modular_redundancy|TMR — Majority-Vote-Logik, Self-Healing, Grenzen und @redundant auf Arrays]] ==== @integrity — Systemweite Fehlertoleranz ==== Während ''@redundant'' einzelne Variablen schützt, arbeitet ''@integrity'' auf Funktions- oder Unit-Ebene und aktiviert einen von zwei Mechanismen: * **''scrubbed''**: Ein Hintergrundprozess scannt den Speicher und erkennt Bit-Flips durch Prüfsummen-Vergleiche (Memory Scrubbing). * **''lockstep''**: Zwei Prozessorkerne führen die Funktion identisch aus. Der Vergleich der Ergebnisse erkennt Abweichungen — ein Standard-Mechanismus in Safety-Prozessoren wie dem ARM Cortex-R52. @integrity(mode: software_lockstep) @flight_crit fn ExecuteControlLaw(state: AircraftState): ControlOutput { // Wird auf zwei Kernen parallel ausgeführt und verglichen var pitch_cmd: f64 := PIDController(state.pitch_error); var roll_cmd: f64 := PIDController(state.roll_error); var _r: ControlOutput; _r.pitch := pitch_cmd; _r.roll := roll_cmd; return _r; } → [[lyx_-_programmiersprache:guides:do-178c:software-lockstep|Software Lockstep — generierter Code, WCET-Interaktion, Recovery-Handler]] · [[lyx_-_programmiersprache:guides:do-178c:memory-scrubbing|Memory Scrubbing — Timing-Fenster, ISR-Integration]] · [[lyx_-_programmiersprache:guides:do-178c:meta_safe|.meta_safe ELF-Sektion]] ==== @wcet — Worst-Case Execution Time Budget ==== ''@wcet(N)'' definiert das Zeitbudget einer Funktion in Mikrosekunden. Der Compiler und ein nachgelagertes WCET-Analyse-Tool prüfen, ob die annotierte Funktion dieses Budget auf der Zielarchitektur einhalten kann. Das ist eine zentrale Anforderung für Echtzeitsysteme, bei denen Fristen (Deadlines) harte Sicherheitsgrenzen sind. @wcet(250) // max. 250 Mikrosekunden @flight_crit fn UpdateNavigationState(gps: GPSData, imu: IMUData): NavState { // Alle Pfade durch diese Funktion müssen unter 250 µs bleiben var fused := SensorFusion(gps, imu); return ComputeNavState(fused); } ==== @volatile — Memory Mapped I/O ==== Hardware-Register, die über Memory Mapped I/O adressiert werden, dürfen vom Compiler nicht wegoptimiert werden — auch wenn ein Wert scheinbar unverändert bleibt. ''@volatile'' verhindert diese Optimierung und stellt sicher, dass jeder Lese- und Schreibzugriff tatsächlich zum Hardware-Register durchdringt. @volatile var STATUS_REG: uint32 := 0x40020000; // Adresse eines Hardware-Registers fn WaitForReady(): void { // Ohne @volatile würde der Compiler diese Schleife wegoptimieren while ((STATUS_REG & 0x01) == 0) { // warte auf Hardware-Bereitschaft } } ==== @packed — Exaktes Speicher-Layout ==== Hardware-Protokolle und externe Schnittstellen erwarten oft Datenstrukturen ohne Padding-Bytes. ''@packed'' weist den Compiler an, kein Alignment-Padding einzufügen — die Felder folgen direkt aufeinander, genau wie in der Hardware-Spezifikation definiert. @packed type CANFrame = struct { id: uint32; // 4 Byte — direkt gefolgt von: dlc: uint8; // 1 Byte data: uint8[8]; // 8 Byte checksum: uint16; // 2 Byte // Gesamt: 15 Byte, kein Padding }; ==== @dal — Level-spezifische Linter-Strenge ==== ''@dal(A)'', ''@dal(B)'' usw. informieren den Linter über das erforderliche Sicherheitslevel einer Unit oder Funktion. Bei DAL-A prüft der Linter alle Safety-Regeln maximal strikt: Jede Funktion muss ''@stack_limit'' haben, kein ''new'' im Regelzyklus, alle Branches müssen erreichbar und durch Tests abgedeckt sein. @dal(A) unit FlightControlUnit; @dal(A) @flight_crit @stack_limit(1024) @wcet(500) fn MainControlLoop(state: AircraftState): ControlOutput { // Maximale Compiler- und Linter-Strenge aktiv } ---- ===== Deterministische Speicherverwaltung ===== Garbage Collectors und unkontrollierte Heap-Allokation sind in Echtzeit-Flugsystemen verboten — sie verursachen nicht-deterministische Pausen, die Deadlines verletzen können. Lyx hat keinen GC, aber die Verantwortung für deterministisches Speicherverhalten liegt beim Entwickler. Diese Regeln helfen dabei: ^ Regel ^ Grund ^ | Kein ''new'' im Regelzyklus | Heap-Allokation kann blockieren oder fragmentieren | | Statische Arrays bevorzugen | ''var buf: uint8[256]'' liegt auf dem Stack — Größe compile-time bekannt | | ''new'' nur in der Initialisierungsphase | Einmalige Allokation beim Start ist kontrollierbar | | ''@flight_crit'' erzwingt das Heap-Verbot | Compiler-Fehler statt Laufzeit-Problem | // Initialisierungsphase — Heap-Allokation erlaubt fn SystemInit(): SensorArray { var sensors := new SensorArray(16); sensors.Calibrate(); return sensors; } // Regelzyklus — kein new erlaubt @flight_crit @stack_limit(2048) fn ControlCycle(sensors: SensorArray, state: AircraftState): ControlOutput { // Nur Stack-Variablen — deterministisch, keine Pausen var readings: f64[16]; sensors.ReadAll(readings); var filtered: f64 := KalmanFilter(readings, 16); return ComputeControlOutput(filtered, state); } ---- ===== Range-Typen — Ungültige Zustände verhindern ===== Ein ungültiger Sensorwert, der ungeprüft in die Flugsteuerung gelangt, kann katastrophale Folgen haben. Range-Typen lösen dieses Problem auf Typebene: Der Compiler prüft konstante Zuweisungen zur Compile-Zeit und fügt für dynamische Zuweisungen automatisch Laufzeit-Checks ein. Bei Verletzung wird ein kontrollierter ''panic'' ([[lyx_-_programmiersprache:sprache:exception-handling|Fehlerbehandlung]]) ausgelöst — kein undefiniertes Verhalten. // Typdefinitionen mit aeronautischen Wertegrenzen type Altitude = int64 range -1000..60000; // Meter über MSL type Speed = int64 range 0..900; // km/h type Heading = int64 range 0..359; // Grad type BankAngle = int64 range -60..60; // Grad type Throttle = int64 range 0..100; // Prozent fn SetCruiseParameters(alt: Altitude, spd: Speed, hdg: Heading): void { // Alle Parameter sind durch ihre Typen garantiert gültig. // Diese Funktion kann niemals einen Höhenwert von 100.000 m erhalten — // der Aufrufer hätte bereits einen Fehler bekommen. EngageAutopilot(alt, spd, hdg); } fn main(): int64 { var target_alt: Altitude := 70000; // Compile-Fehler: außerhalb -1000..60000 var cruise_alt: Altitude := 10500; // OK SetCruiseParameters(cruise_alt, 850, 270); return 0; } ---- ===== Bounded Loops — Endlichkeit nachweisen ===== Unbegrenzte Schleifen in sicherheitskritischem Code sind ein Problem: Die WCET lässt sich nicht berechnen, wenn eine Schleife theoretisch unbegrenzt laufen kann. ''limit(N)'' ([[lyx_-_programmiersprache:sprache:schleifen|Schleifen]]) setzt ein hartes Maximum an Iterationen und macht die Endlichkeit im Code explizit und für Analyse-Tools direkt auswertbar. @flight_crit fn WaitForSensorReady(sensor: SensorHandle): bool { var attempts: int64 := 0; while (!sensor.IsReady()) limit(50) { // max. 50 Versuche — danach Abbruch mit false attempts := attempts + 1; SleepMicros(100); } return sensor.IsReady(); } Ohne ''limit'' würde ''--static-analysis'' eine Warnung erzeugen, da die Schleife im Fehlerfall nie terminiert. Mit ''limit(50)'' ist die maximale Ausführungszeit auf 50 × 100 µs = 5 ms begrenzt und für WCET-Kalkulationen verwendbar. ---- ===== Statische Analyse und Zertifizierungs-Toolchain ===== Lyx bündelt alle Zertifizierungs-relevanten Werkzeuge direkt im Compiler. Es werden keine separaten Tools benötigt. ==== Linter und statische Analyse ==== # DO-178C-Konformität prüfen — meldet alle Verstöße gegen Safety-Regeln lyxc flight_ctrl.lyx --lint # Nur Lint, kein Binary erzeugen lyxc flight_ctrl.lyx --lint-only # Tiefe statische Analyse: unerreichbarer Code, Division durch null, Null-Pointer-Risiken lyxc flight_ctrl.lyx --static-analysis ==== Call-Graph und Stack-Analyse ==== # Call-Graph als DOT-Datei erzeugen (visualisierbar mit Graphviz) lyxc flight_ctrl.lyx --call-graph -o call_graph.dot # Stack-Nutzung gegen @stack_limit validieren — laeuft ohne Flag bei jeder Uebersetzung mit lyxc flight_ctrl.lyx -o flight_ctrl ==== MC/DC-Coverage-Instrumentierung ==== **Modified Condition/Decision Coverage (MC/DC)** ist das Testabdeckungs-Kriterium für DAL-A und DAL-B. Es verlangt, dass jede atomare Bedingung in einem booleschen Ausdruck unabhängig voneinander den Gesamtausdruck beeinflussen kann. **Der Compiler kann MC/DC nicht messen** (#1524). ''--mcdc-instrument'' und ''--coverage-report'' gibt es nicht; ''--mcdc'' baut keine Instrumentierung ein, und ''--mcdc-report'' zählt zusammengesetzte Bedingungen als **eine** — also gerade das nicht, was MC/DC ausmacht. Entscheidungen in einem ''return''-Ausdruck werden zudem übersehen. Einen Coverage-Report wie den früher hier abgedruckten gibt es folglich nicht. Der Nachweis für DAL-A/B ist außerhalb des Compilers zu führen. Was der Compiler liefert, ist eine Strukturübersicht der Entscheidungspunkte in ''if''- und ''while''-Köpfen: lyxc flight_ctrl.lyx --mcdc-report -o /dev/null [MC/DC] Coverage structure analysis [MC/DC] Functions analyzed: 3 [MC/DC] Total decision points: 3 [MC/DC] ComputeAltitude: 1 decisions, 1 conditions → min 2 test cases [MC/DC] Decision point details: [MC/DC] point #0 in 'ComputeAltitude': if (node 6) Die Zahl hinter „conditions" ist mit Vorsicht zu lesen — sie lautet bei jeder Entscheidung 1. → [[lyx_-_programmiersprache:guides:do-178c|DO-178C — MC/DC-Testvektortabelle, vollständiger Coverage-Workflow, Qualifikations-Evidenz-Übersicht]] ==== Deterministische Builds und Provenance ==== Reproduzierbare Builds sind eine Zertifizierungsanforderung: Aus identischem Quellcode muss bit-identischer Maschinencode entstehen, unabhängig von Zeitpunkt und Buildmaschine. # Build-Informationen anzeigen (Compiler-Version, Flags, Zeitstempel) lyxc --build-info # Provenance-Tracking: Zuordnung IR -> AST -> Quellzeile lyxc flight_ctrl.lyx --provenance -o /dev/null > evidence/provenance.log # Alle Passes und Transformationen tracen (Audit-Log für Zertifizierung) lyxc flight_ctrl.lyx --trace-passes -o flight_ctrl ''--provenance'' schreibt **kein** eigenes Protokoll auf die Platte — die Ausgabe geht nach stdout und muss umgeleitet werden. Vor allem aber ist das dabei erzeugte Programm **nicht lauffähig** (#1523): es gibt nichts aus und endet mit Exit 42. Daher ''-o /dev/null'' und ein zweiter Aufruf ohne den Schalter für den Auslieferungsstand. Die Zeilennummern der Zuordnung stimmen überdies grösstenteils nicht — bei einem 22-zeiligen Programm verwiesen 77 von 85 Einträgen auf die Importzeile. Als Traceability-Nachweis taugt die Ausgabe derzeit nicht. ==== AST, IR und Symboltabelle inspizieren ==== Für formale Verifikation und manuelle Codereviews können interne Compiler-Repräsentationen exportiert werden: # Abstract Syntax Tree ausgeben lyxc flight_ctrl.lyx --ast-dump # Symboltabelle mit Typen und Adressen lyxc flight_ctrl.lyx --symtab-dump # IR-zu-Quellcode-Mapping — liefert derzeit fast nichts und zerstoert # das erzeugte Programm (#1523); nur mit -o /dev/null verwenden lyxc flight_ctrl.lyx --ir-source-map -o /dev/null # Typ-Inferenz-Protokoll lyxc flight_ctrl.lyx --type-reasoning # Constraint-Solver-Log (Range-Typen, Bound-Checks) lyxc flight_ctrl.lyx --constraint-log ---- ===== Vollständiges Beispiel: Flugsteuerungs-Funktion ===== Das folgende Beispiel zeigt eine realistische Funktion eines primären Flugsteuerungssystems mit allen relevanten Safety-Features kombiniert: unit FlightControlSystem; import std.math; // ── Typen mit aeronautischen Wertegrenzen ────────────────────────────────── type Altitude = int64 range -500..15000; // Meter MSL type Speed = int64 range 0..500; // Knoten type BankAngle = int64 range -45..45; // Grad type Throttle = int64 range 0..100; // Prozent // ── Structs für Sensor- und Steuerdaten ─────────────────────────────────── type SensorInput = struct { altitude_raw: f64; airspeed_raw: f64; bank_angle: f64; pitch_angle: f64; valid: bool; }; type ControlOutput = struct { throttle: Throttle; aileron: BankAngle; elevator: int64; autopilot_on: bool; }; // ── Interne Hilfsfunktion (nicht exportiert) ─────────────────────────────── @stack_limit(256) fn Clamp(value: int64, lo: int64, hi: int64): int64 { if (value < lo) { return lo; } if (value > hi) { return hi; } return value; } // ── Hauptfunktion DAL-A ──────────────────────────────────────────────────── @dal(A) @flight_crit @stack_limit(1024) @wcet(500) @integrity(mode: software_lockstep) pub fn ComputeControlLaw(input: SensorInput): ControlOutput { // Ungültige Sensordaten sicher abfangen if (!input.valid) { var _r: ControlOutput; _r.throttle := 50; _r.aileron := 0; _r.elevator := 0; _r.autopilot_on := false; return _r; } // TMR-geschützte kritische Zustandsvariablen @redundant var altitude: Altitude := input.altitude_raw as int64; @redundant var airspeed: Speed := input.airspeed_raw as int64; // Einfacher Höhenregler (P-Regler) con TARGET_ALTITUDE: Altitude := 10000; var altitude_error: int64 := TARGET_ALTITUDE - altitude; // Elevator-Kommando aus Höhenfehler ableiten (skaliert, geclamped) var elevator_cmd: int64 := Clamp(altitude_error / 50, -30, 30); // Geschwindigkeitsregler: Schubkommando con TARGET_SPEED: Speed := 250; var speed_error: int64 := TARGET_SPEED - airspeed; var throttle_cmd: int64 := Clamp(50 + (speed_error / 5), 0, 100); // Querruder aus Querneigung — Kurskorrektur var aileron_cmd: int64 := Clamp(-(input.bank_angle as int64), -45, 45); var _r: ControlOutput; _r.throttle := throttle_cmd as Throttle; _r.aileron := aileron_cmd as BankAngle; _r.elevator := elevator_cmd; _r.autopilot_on := true; return _r; } Kompilierung mit allen Safety-Checks: lyxc FlightControlSystem.lyx \ --lint \ --static-analysis \ --call-graph \ --verify-tmr \ --runtime-checks \ --target=arm64 \ -o flight_ctrl.elf ---- ===== Best Practices auf einen Blick ===== Empfehlungen für den produktiven Einsatz: ^ Situation ^ Empfehlung ^ | Funktionen im Regelzyklus | Immer ''@flight_crit'' + ''@stack_limit'' + ''@wcet'' | | Zustandsvariablen (Heading, Altitude) | ''@redundant'' für TMR-Schutz | | Wertebereichsbegrenzung | Range-Typen statt manueller Validierung | | Schleifen mit unbekannter Endlichkeit | ''limit(N)'' setzen | | Hardware-Register | ''@volatile'' | | C-Protokoll-Strukturen | ''@packed'' | | Testabdeckung DAL-A/B | 100 % MC/DC nachweisen — **ausserhalb des Compilers** (#1524) | | Audit und Zertifizierung | ''--build-info'' + ''--trace-passes''; ''--provenance'' nur im getrennten Lauf (#1523) | | Dynamische Allokation | Nur in der Initialisierungsphase, nie im Regelzyklus | | Fließkomma-Konsistenz | ''@flight_crit'' deaktiviert unsichere FP-Optimierungen | ---- → [[lyx_-_programmiersprache:guides:aerospace-tutorial|Aerospace Tutorial: Von der Anforderung zum Nachweis]]\\ → [[lyx_-_programmiersprache:guides:do-178c|DO-178C Compliance — DAL-Stufen, MC/DC, WCET, TMR, Memory Scrubbing, Qualifikations-Evidenz]]\\ → 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]] 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). ---- Letzte Aktualisierung: 2026-09-05 ([[https://github.com/SEOLizer/LyX-Compiler/issues/1908|#1908]], gemessen mit lyxc 1.1.18A) — ''@integrity(mode: lockstep)'' an zwei Stellen auf ''mode: software_lockstep'' berichtigt — ''lockstep'' ist kein gültiger Modus und wird abgewiesen.