====== 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, 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:do-178c|DO-178C — DAL-Stufen, MC/DC, WCET, TMR, Qualifikations-Evidenz]] ---- ===== 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: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. Es aktiviert ein Set an Compiler-Einschränkungen, die für Avionik-Code zwingend notwendig sind: * **Heap-Verbot:** ''new'' ist innerhalb der Funktion nicht erlaubt. Alle Daten müssen auf dem Stack oder in vorallokierten Puffern liegen. * **Floating-Point-Determinismus:** Fließkomma-Optimierungen (Constant Folding, Reordering) werden deaktiviert, um konsistentes Rundungsverhalten über alle Compilerdurchläufe und Architekturen zu garantieren. * **Kein FFI ohne Wrapper:** Direkte ''@extern''-Aufrufe sind verboten. Externe Funktionen müssen in einen validierten Wrapper gekapselt werden. @flight_crit fn ComputeAltitude(rawPressure: f64): f64 { // Hier ist kein 'new' erlaubt — Compiler-Fehler wenn versucht // Alle Fließkomma-Operationen haben deterministisches Verhalten 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. Mit dem Compiler-Flag ''--stack-check'' analysiert ''lyxc'' den kompletten Call-Graph und stellt statisch sicher, dass dieses Limit für jeden möglichen Ausführungspfad eingehalten wird. @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: lyxc flight_ctrl.lyx --stack-check -o flight_ctrl # Fehler, wenn Stack-Limit irgendwo überschritten wird: # error: function 'ProcessSensorFrame' exceeds stack limit: 620 bytes used, 512 allowed ==== @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: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: 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); return ControlOutput { pitch: pitch_cmd, roll: roll_cmd }; } → [[lyx_-_programmiersprache:do-178c:software-lockstep|Software Lockstep — generierter Code, WCET-Interaktion, Recovery-Handler]] · [[lyx_-_programmiersprache:do-178c:memory-scrubbing|Memory Scrubbing — Timing-Fenster, ISR-Integration]] · [[lyx_-_programmiersprache: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 := 0x40020000u32; // Adresse eines Hardware-Registers fn WaitForReady(): void { // Ohne @volatile würde der Compiler diese Schleife wegoptimieren while ((STATUS_REG & 0x01u32) == 0u32) { // 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'' 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)'' 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 aller Funktionen prüfen und gegen @stack_limit validieren lyxc flight_ctrl.lyx --stack-check ==== 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 instrumentiert den Code automatisch für MC/DC-Messung: # MC/DC-Instrumentation aktivieren lyxc flight_ctrl.lyx --mcdc-instrument -o flight_ctrl_instrumented # Coverage-Report nach Testlauf erzeugen lyxc --coverage-report flight_ctrl.coverage -o coverage.html # Beispielausgabe eines Coverage-Reports: # Function: ComputeAltitude — Line: 95% Branch: 88% MC/DC: 100% ✓ # Function: ProcessSensorFrame — Line: 100% Branch: 100% MC/DC: 100% ✓ # Function: WaitForSensorReady — Line: 80% Branch: 75% MC/DC: 75% ✗ (DAL-A requires 100%) → [[lyx_-_programmiersprache: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: jede IR-Transformation protokollieren lyxc flight_ctrl.lyx --provenance -o flight_ctrl # Alle Passes und Transformationen tracen (Audit-Log für Zertifizierung) lyxc flight_ctrl.lyx --trace-passes -o flight_ctrl ==== 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 (welche IR-Instruktion stammt aus welcher Zeile) lyxc flight_ctrl.lyx --ir-source-map # 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: lockstep) pub fn ComputeControlLaw(input: SensorInput): ControlOutput { // Ungültige Sensordaten sicher abfangen if (!input.valid) { return ControlOutput { throttle: 50, aileron: 0, elevator: 0, autopilot_on: false }; } // 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); return ControlOutput { throttle: throttle_cmd as Throttle, aileron: aileron_cmd as BankAngle, elevator: elevator_cmd, autopilot_on: true }; } Kompilierung mit allen Safety-Checks: lyxc FlightControlSystem.lyx \ --lint \ --static-analysis \ --stack-check \ --mcdc-instrument \ --target=arm64 \ -o flight_ctrl.elf ---- ===== Best Practices auf einen Blick ===== ^ 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 | ''--mcdc-instrument'' + 100 % MC/DC nachweisen | | Audit und Zertifizierung | ''--provenance'' + ''--trace-passes'' + ''--build-info'' | | Dynamische Allokation | Nur in der Initialisierungsphase, nie im Regelzyklus | | Fließkomma-Konsistenz | ''@flight_crit'' deaktiviert unsichere FP-Optimierungen | ---- → [[lyx_-_programmiersprache:aerospace-tutorial|Aerospace Tutorial: Von der Anforderung zum Nachweis]]\\ → [[lyx_-_programmiersprache:do-178c|DO-178C Compliance — DAL-Stufen, MC/DC, WCET, TMR, Memory Scrubbing, Qualifikations-Evidenz]]\\ → 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]]