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 (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: DO-178C — DAL-Stufen, MC/DC, WCET, TMR, Qualifikations-Evidenz

→ Rechnende Units: std.aero (Standardatmosphäre, Flugleistung, Flugführung) · std.astro (Bahnmechanik, Eintritt, Start)

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.

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
}

→ DO-178C — vollständige Coverage-Anforderungen pro DAL, MC/DC-Workflow, Compiler-Flags und Qualifikations-Evidenz

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 ist das zentrale Sicherheits-Attribut (alle Attribute im Überblick: 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

<WRAP alert> 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. </WRAP>

@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-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(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

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);
}

→ TMR — Majority-Vote-Logik, Self-Healing, Grenzen und @redundant auf Arrays

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;
}

→ Software Lockstep — generierter Code, WCET-Interaktion, Recovery-Handler · Memory Scrubbing — Timing-Fenster, ISR-Integration · .meta_safe ELF-Sektion

@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);
}

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
    }
}

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(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
}

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:

// 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);
}

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 (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;
}

Unbegrenzte Schleifen in sicherheitskritischem Code sind ein Problem: Die WCET lässt sich nicht berechnen, wenn eine Schleife theoretisch unbegrenzt laufen kann. limit(N) (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.

Lyx bündelt alle Zertifizierungs-relevanten Werkzeuge direkt im Compiler. Es werden keine separaten Tools benötigt.

# 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 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

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.

<WRAP alert> 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. </WRAP>

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.

→ DO-178C — MC/DC-Testvektortabelle, vollständiger Coverage-Workflow, Qualifikations-Evidenz-Übersicht

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

<WRAP alert> –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. </WRAP>

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

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

Empfehlungen für den produktiven Einsatz:

→ Aerospace Tutorial: Von der Anforderung zum Nachweis
→ DO-178C Compliance — DAL-Stufen, MC/DC, WCET, TMR, Memory Scrubbing, Qualifikations-Evidenz
→ Unterseiten: TMR · Software Lockstep · Memory Scrubbing · .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 (#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.