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: TMR · Software Lockstep · Memory Scrubbing · .meta_safe ELF-Sektion
→ Ergänzend: Aerospace Safety · CLI-Referenz · Embedded & RTOS

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.

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

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 (Attributes & Pragmas) erzwingt auf annotierte Funktionen:

@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: Aerospace & Safety

Laufzeit- und Stack-Budgets für sicherheitskritischen Code:

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

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
}

Out-of-Range-Werte sind eine Hauptursache für Flugunfälle (z.B. falscher Einheitenname, falsche Skala). Lyx-Range-Typen (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

DO-178C verlangt für DAL-A, dass single-point failures im Hardware (Bit-Flips durch kosmische Strahlung, Speicherfehler) erkannt oder toleriert werden.

@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: Triple Modular Redundancy

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

→ Software Lockstep — vollständige Dokumentation
→ Memory Scrubbing — vollständige Dokumentation

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.

// 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):

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

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.

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

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.

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 (→ Attribute). Ebenso @stack_limit und @wcet: deren Nachweis führt der Compiler bei jeder Übersetzung, ganz ohne Flag.

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.

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

Vollständige Flag-Referenz: → CLI-Referenz

DO-178C verlangt eine strukturierte Menge von Nachweis-Dokumenten (Evidence). Lyx-Compiler-Outputs decken die technischen Artefakte ab:

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

Die Planung- und Prozess-Dokumente (PSAC, SDP, SVP, SCI) entstehen außerhalb des Compilers — Lyx liefert die technischen Daten, auf die diese Dokumente verweisen.

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

→ Aerospace & Safety — Safety-Attribute, Range-Typen, Bounded Loops, Best-Practices-Tabelle und vollständiges Regelkreis-Beispiel
→ 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).