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

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

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

→ 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 := 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
    }
}

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 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) 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 aller Funktionen prüfen und gegen @stack_limit validieren
lyxc flight_ctrl.lyx --stack-check

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%)

→ 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: 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

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

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

→ 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