====== Aerospace Tutorial: Von der Anforderung zum Nachweis ====== Dieses Tutorial führt Schritt für Schritt durch den vollständigen Entwicklungszyklus eines sicherheitskritischen Lyx-Programms — von der Projektstruktur über das Schreiben von Safety-konformem Code bis hin zur Erzeugung aller Zertifizierungsnachweise nach DO-178C ([[lyx_-_programmiersprache:guides:do-178c|Guide]]). Als durchgehendes Beispiel dient ein **Altitude Monitor**: eine Komponente, die Druckrohdaten in Höhenmeter umrechnet, Grenzwerte überwacht und einen Warnung-Status ausgibt. Einfach genug, um den Fokus auf den Prozess zu legen — komplex genug, um alle relevanten Safety-Features zu zeigen. > **Zielgruppe:** Entwickler, die erstmals ein DO-178C-konformes Programm mit Lyx erstellen oder den gesamten Toolchain-Workflow kennenlernen wollen. ---- ===== 1. Projektstruktur anlegen ===== Eine klare Verzeichnisstruktur ist die Grundlage für nachvollziehbare, auditierbare Builds. DO-178C verlangt, dass Quellcode, Tests und Nachweise klar voneinander getrennt sind. mkdir -p altitude_monitor/{src,tests,build,evidence} cd altitude_monitor ^ Verzeichnis ^ Inhalt ^ | ''src/'' | Produktiver Quellcode (.lyx-Dateien) | | ''tests/'' | Testfälle und Testprogramme | | ''build/'' | Compiler-Ausgaben (Binaries, .lyu-Units) | | ''evidence/'' | Zertifizierungsnachweise (Reports, Logs, Graphs) | Struktur nach dem Tutorial: altitude_monitor/ ├── src/ │ ├── types.lyx # Gemeinsame Typdefinitionen │ └── altitude.lyx # Hauptkomponente ├── tests/ │ └── altitude_test.lyx # Testprogramm ├── build/ │ ├── altitude.elf │ └── altitude_test.elf └── evidence/ ├── call_graph.dot ├── coverage.html ├── static_analysis.log ├── stack_report.log └── provenance.log ---- ===== 2. Typdefinitionen schreiben ===== Alle gemeinsamen Typen kommen in eine eigene Datei. Range-Typen ([[lyx_-_programmiersprache:sprache:typaliase-und-typumwandlung|Typaliase & Typumwandlung]]) sind das erste Sicherheitsnetz — sie machen ungültige Zustände auf Typebene unmöglich. Datei: ''src/types.lyx'' unit AltitudeMonitor.Types; // Physikalische Wertebereiche — Compile-Zeit- und Laufzeit-geprüft type Altitude = int64 range -1000..15000; // Meter über MSL type Pressure = int64 range 10000..115000; // Pascal (10–1150 hPa) type Temperature = int64 range -90..60; // Grad Celsius type Confidence = int64 range 0..100; // Prozent // Warnstatus — geschlossene Menge, kein ungültiger Wert möglich type WarningLevel = enum { NOMINAL, CAUTION, // Annäherung an Grenzwert WARNING, // Grenzwert überschritten CRITICAL // Zweiter Grenzwert überschritten — sofortiger Handlungsbedarf }; // Sensor-Rohdaten vom ADC type SensorFrame = struct { pressure_raw: int64; temperature_raw: int64; valid: bool; sequence_id: int64; }; // Ausgabe der Altitude-Monitor-Komponente type AltitudeResult = struct { altitude: Altitude; warning: WarningLevel; confidence: Confidence; valid: bool; }; ---- ===== 3. Hauptkomponente schreiben ===== Die Hauptkomponente enthält die eigentliche Berechnungslogik. Jede Funktion, die im Regelzyklus aufgerufen wird, bekommt die entsprechenden Safety-Pragmas. Datei: ''src/altitude.lyx'' unit AltitudeMonitor; import AltitudeMonitor.Types; import std.math; // ── Grenzwerte ──────────────────────────────────────────────────────────────── con CAUTION_ALTITUDE: Altitude := 12000; // Meter — Vorsichtsgrenze con WARNING_ALTITUDE: Altitude := 13500; // Meter — Warngrenze con CRITICAL_ALTITUDE: Altitude := 14500; // Meter — Kritische Grenze con SEA_LEVEL_PRESSURE: f64 := 101325.0; // Pascal con SCALE_HEIGHT: f64 := 8434.0; // Meter (barometrische Formel) con MIN_CONFIDENCE: Confidence := 70; // Unter diesem Wert: Ergebnis ungültig // ── Interne Hilfsfunktionen ─────────────────────────────────────────────────── // Berechnet Höhe aus Luftdruck nach barometrischer Höhenformel // Kein @flight_crit — wird nur aus validierten Funktionen aufgerufen @stack_limit(128) fn PressureToAltitude(pressure_pa: f64): f64 { con EXPONENT: f64 := 0.190263; var ratio: f64 := pressure_pa / SEA_LEVEL_PRESSURE; return SCALE_HEIGHT * (1.0 - PowF64(ratio, EXPONENT)); } // Berechnet Konfidenzwert aus Sensorkonsistenz (vereinfacht) @stack_limit(128) fn ComputeConfidence(frame: SensorFrame): Confidence { if (!frame.valid) { return 0; } // Plausibilitätsprüfung Druck vs. Temperatur (vereinfacht) var p_ok: bool := (frame.pressure_raw >= 10000) && (frame.pressure_raw <= 115000); var t_ok: bool := (frame.temperature_raw >= -90) && (frame.temperature_raw <= 60); if (!p_ok || !t_ok) { return 40; } return 95; } // Bestimmt Warnstufe aus berechneter Höhe @stack_limit(128) fn ClassifyAltitude(alt: Altitude): WarningLevel { if (alt >= CRITICAL_ALTITUDE) { return WarningLevel.CRITICAL; } if (alt >= WARNING_ALTITUDE) { return WarningLevel.WARNING; } if (alt >= CAUTION_ALTITUDE) { return WarningLevel.CAUTION; } return WarningLevel.NOMINAL; } // ── Hauptfunktion ───────────────────────────────────────────────────────────── @dal(B) @flight_crit @stack_limit(512) @wcet(800) pub fn ProcessSensorFrame(frame: SensorFrame): AltitudeResult { // Ungültige oder nicht plausible Frames sicher ablehnen if (!frame.valid) { var _r: AltitudeResult; _r.altitude := 0; _r.warning := WarningLevel.NOMINAL; _r.confidence := 0; _r.valid := false; return _r; } // TMR-Schutz für den berechneten Höhenwert @redundant var altitude_raw: f64 := PressureToAltitude(frame.pressure_raw as f64); // Clamping in den gültigen Range-Typ — Range-Typ übernimmt weitere Prüfung var alt_clamped: int64 := altitude_raw as int64; if (alt_clamped < -1000) { alt_clamped := -1000; } if (alt_clamped > 15000) { alt_clamped := 15000; } @redundant var altitude: Altitude := alt_clamped; var conf: Confidence := ComputeConfidence(frame); var warning: WarningLevel := ClassifyAltitude(altitude); // Ergebnis als ungültig markieren, wenn Konfidenz zu niedrig var result_valid: bool := (conf >= MIN_CONFIDENCE); var _r: AltitudeResult; _r.altitude := altitude; _r.warning := warning; _r.confidence := conf; _r.valid := result_valid; return _r; } ---- ===== 4. Tests schreiben ===== Tests in Lyx sind gewöhnliche Programme, die die zu testende Unit importieren. Für MC/DC ([[lyx_-_programmiersprache:guides:do-178c|DO-178C]]) müssen alle atomaren Bedingungen unabhängig voneinander den Gesamtausdruck beeinflussen — die Testfälle müssen diese Kombinationen explizit abdecken. Datei: ''tests/altitude_test.lyx'' Der folgende Block benutzt std.test. **Diese Unit ist noch nicht ausgeliefert** — import std.test; scheitert mit Modul nicht gefunden. Die Testfaelle geben die vorgesehene Form wieder und sind **nicht compilerverifiziert**. unit AltitudeMonitor.Tests; import AltitudeMonitor; import AltitudeMonitor.Types; import std.test; // ── Hilfsfunktion ───────────────────────────────────────────────────────────── fn MakeFrame(pressure: int64, temp: int64, valid: bool): SensorFrame { var _r: SensorFrame; _r.pressure_raw := pressure; _r.temperature_raw := temp; _r.valid := valid; _r.sequence_id := 1; return _r; } // ── Testfälle für ProcessSensorFrame ───────────────────────────────────────── // TC-01: Ungültiger Frame → result.valid = false, warning = NOMINAL fn TC01_InvalidFrame(): void { var frame := MakeFrame(101325, 15, false); var result: AltitudeResult := ProcessSensorFrame(frame); test.Assert(!result.valid, "TC-01: result.valid soll false sein"); test.Assert(result.warning == WarningLevel.NOMINAL, "TC-01: warning soll NOMINAL sein"); test.Assert(result.confidence == 0, "TC-01: confidence soll 0 sein"); } // TC-02: Normalbetrieb, Meeresspiegel — NOMINAL fn TC02_NominalSealevel(): void { var frame := MakeFrame(101325, 15, true); var result: AltitudeResult := ProcessSensorFrame(frame); test.Assert(result.valid, "TC-02: result.valid soll true sein"); test.Assert(result.warning == WarningLevel.NOMINAL, "TC-02: warning soll NOMINAL sein"); test.Assert(result.confidence >= 70, "TC-02: confidence soll >= 70 sein"); } // TC-03: Reiseflug ~10.000 m — NOMINAL (unterhalb CAUTION-Grenze) fn TC03_CruiseAltitude(): void { var frame := MakeFrame(26436, -45, true); // ~10.000 m var result: AltitudeResult := ProcessSensorFrame(frame); test.Assert(result.valid, "TC-03: result soll valid sein"); test.Assert(result.warning == WarningLevel.NOMINAL, "TC-03: 10.000m soll NOMINAL sein"); } // TC-04: CAUTION-Bereich (~12.500 m) fn TC04_CautionAltitude(): void { var frame := MakeFrame(19000, -55, true); // ~12.500 m var result: AltitudeResult := ProcessSensorFrame(frame); test.Assert(result.valid, "TC-04: result soll valid sein"); test.Assert(result.warning == WarningLevel.CAUTION, "TC-04: soll CAUTION sein"); } // TC-05: WARNING-Bereich (~13.800 m) fn TC05_WarningAltitude(): void { var frame := MakeFrame(16000, -60, true); // ~13.800 m var result: AltitudeResult := ProcessSensorFrame(frame); test.Assert(result.valid, "TC-05: result soll valid sein"); test.Assert(result.warning == WarningLevel.WARNING, "TC-05: soll WARNING sein"); } // TC-06: CRITICAL-Bereich (~14.700 m) fn TC06_CriticalAltitude(): void { var frame := MakeFrame(14000, -62, true); // ~14.700 m var result: AltitudeResult := ProcessSensorFrame(frame); test.Assert(result.valid, "TC-06: result soll valid sein"); test.Assert(result.warning == WarningLevel.CRITICAL, "TC-06: soll CRITICAL sein"); } // TC-07: Druck außerhalb Plausibilitätsbereich → confidence < MIN → result.valid = false fn TC07_ImplausiblePressure(): void { var frame := MakeFrame(5000, 15, true); // Druck zu niedrig (< 10000 Pa) var result: AltitudeResult := ProcessSensorFrame(frame); test.Assert(!result.valid, "TC-07: implausible pressure soll result.valid = false ergeben"); } // TC-08: Temperatur außerhalb Plausibilitätsbereich fn TC08_ImplausibleTemperature(): void { var frame := MakeFrame(101325, 80, true); // Temperatur zu hoch (> 60°C) var result: AltitudeResult := ProcessSensorFrame(frame); test.Assert(!result.valid, "TC-08: implausible temperature soll result.valid = false ergeben"); } // TC-09: Grenzwert genau an CAUTION-Grenze (Boundary Value) fn TC09_BoundaryCAUTION(): void { // Druck der ~12.000 m entspricht (Boundary Value Analysis) var frame := MakeFrame(19330, -56, true); var result: AltitudeResult := ProcessSensorFrame(frame); test.Assert(result.valid, "TC-09: Boundary-Frame soll valid sein"); // Warning ist CAUTION oder NOMINAL je nach exaktem Rundungsverhalten } // TC-10: MC/DC — frame.valid=false dominiert, Pressure/Temp irrelevant fn TC10_MCDC_InvalidOverrides(): void { var frame := MakeFrame(5000, 80, false); // Beide Werte außerhalb + invalid var result: AltitudeResult := ProcessSensorFrame(frame); test.Assert(!result.valid, "TC-10: MCDC: invalid-Flag dominiert"); test.Assert(result.confidence == 0, "TC-10: MCDC: confidence soll 0 sein"); } // ── Einstiegspunkt ──────────────────────────────────────────────────────────── fn main(): int64 { test.Begin("AltitudeMonitor — Testlauf"); TC01_InvalidFrame(); TC02_NominalSealevel(); TC03_CruiseAltitude(); TC04_CautionAltitude(); TC05_WarningAltitude(); TC06_CriticalAltitude(); TC07_ImplausiblePressure(); TC08_ImplausibleTemperature(); TC09_BoundaryCAUTION(); TC10_MCDC_InvalidOverrides(); test.End(); return 0; } ---- ===== 5. Safety-Build durchführen ===== Der erste Build dient der Überprüfung: Sind alle Safety-Regeln eingehalten? Compiliert der Code ohne Warnungen? # Typen kompilieren (vorkompilierte Unit erzeugen) lyxc src/types.lyx \ --compile-unit \ --lint \ -o build/types.lyu # Hauptkomponente kompilieren — vollständige Safety-Prüfung lyxc src/altitude.lyx \ -I build/ \ --lint \ --static-analysis \ --target=arm64 \ -o build/altitude.elf Erwartete Ausgabe bei korrektem Code: [lint] AltitudeMonitor — OK (0 warnings, 0 errors) [stack] ProcessSensorFrame: 312 bytes / 512 limit — OK [stack] PressureToAltitude: 96 bytes / 128 limit — OK [stack] ComputeConfidence: 80 bytes / 128 limit — OK [stack] ClassifyAltitude: 64 bytes / 128 limit — OK [build] build/altitude.elf — OK Häufige Lint-Fehler und ihre Bedeutung: ^ Fehlermeldung ^ Bedeutung ^ Lösung ^ | ''heap allocation in @flight_crit function'' | ''new'' innerhalb einer @flight_crit-Funktion | ''new'' in die Initialisierungsphase verschieben | | ''unbounded loop in @flight_crit context'' | Schleife ohne ''limit(N)'' | ''limit(N)'' hinzufügen | | ''missing @stack_limit on @flight_crit function'' | Kein Stack-Budget definiert | ''@stack_limit(N)'' ergänzen | | ''range violation: value 16000 exceeds Altitude range'' | Konstante verletzt Range-Typ | Konstante oder Typ korrigieren | | ''@wcet annotation missing for DAL-B function'' | DAL-B verlangt WCET-Budget | ''@wcet(N)'' ergänzen | ---- ===== 6. Tests bauen und ausführen ===== # Testprogramm kompilieren lyxc tests/altitude_test.lyx \ -I build/ \ --lint \ -o build/altitude_test.elf # Tests ausführen ./build/altitude_test.elf Erwartete Ausgabe: === AltitudeMonitor — Testlauf === [PASS] TC-01: result.valid soll false sein [PASS] TC-01: warning soll NOMINAL sein [PASS] TC-01: confidence soll 0 sein [PASS] TC-02: result.valid soll true sein [PASS] TC-02: warning soll NOMINAL sein [PASS] TC-02: confidence soll >= 70 sein [PASS] TC-03: result soll valid sein [PASS] TC-03: 10.000m soll NOMINAL sein [PASS] TC-04: result soll valid sein [PASS] TC-04: soll CAUTION sein [PASS] TC-05: result soll valid sein [PASS] TC-05: soll WARNING sein [PASS] TC-06: result soll valid sein [PASS] TC-06: soll CRITICAL sein [PASS] TC-07: implausible pressure soll result.valid = false ergeben [PASS] TC-08: implausible temperature soll result.valid = false ergeben [PASS] TC-09: Boundary-Frame soll valid sein [PASS] TC-10: MCDC: invalid-Flag dominiert [PASS] TC-10: MCDC: confidence soll 0 sein === ALLE TESTS BESTANDEN (19/19) === ---- ===== 7. Statische Analyse und Call-Graph ===== Die statische Analyse sucht nach Problemen, die Compiler und Tests allein nicht finden — unerreichbarer Code, potenzielle Null-Pointer, nicht initialisierte Variablen, Division durch null. lyxc src/altitude.lyx \ -I build/ \ --static-analysis \ 2>&1 | tee evidence/static_analysis.log Beispielausgabe: [analysis] AltitudeMonitor — ProcessSensorFrame [OK] No unreachable code detected [OK] No null-pointer dereferences detected [OK] No uninitialized variables [OK] No division-by-zero paths [OK] All enum cases handled in ClassifyAltitude [analysis] Completed — 0 issues Call-Graph erzeugen (zeigt, welche Funktion welche aufruft — Pflichtnachweis für DO-178C): lyxc src/altitude.lyx \ -I build/ \ --call-graph \ -o evidence/call_graph.dot # Visualisierung als PNG (benötigt Graphviz) dot -Tpng evidence/call_graph.dot -o evidence/call_graph.png Der Call-Graph zeigt u.a., dass ''ProcessSensorFrame'' genau drei interne Funktionen aufruft (''PressureToAltitude'', ''ComputeConfidence'', ''ClassifyAltitude'') und keine externen oder nicht validierten Funktionen — das ist für DAL-B eine Anforderung. ---- ===== 8. Stack-Report erstellen ===== Der Stack-Report dokumentiert den maximalen Stack-Verbrauch jeder Funktion auf dem gesamten Call-Graph. Er ist der Nachweis, dass kein Stack-Overflow auftreten kann. lyxc src/altitude.lyx \ -I build/ \ 2>&1 | tee evidence/stack_report.log Beispielausgabe: [stack] AltitudeMonitor ProcessSensorFrame 312 / 512 bytes OK PressureToAltitude 96 / 128 bytes OK ComputeConfidence 80 / 128 bytes OK ClassifyAltitude 64 / 128 bytes OK Worst-case call depth: ProcessSensorFrame → PressureToAltitude Worst-case stack total: 408 bytes [stack] All limits satisfied — PASS ---- ===== 9. MC/DC-Coverage messen ===== MC/DC (Modified Condition/Decision Coverage) ist für DAL-A und DAL-B vorgeschrieben. Jede atomare Bedingung in einem booleschen Ausdruck muss nachweislich unabhängig voneinander den Gesamtausdruck beeinflussen. **Dieser Ablauf ist mit dem heutigen Compiler nicht durchführbar** (#1524). ''--mcdc'' baut keine Instrumentierung ein — das Programm ist mit und ohne den Schalter byte-identisch. Es entsteht keine ''.coverage''-Datei, und ''--mcdc-report'' erzeugt keinen HTML-Bericht. Auch ''--link'' gibt es nicht. Der folgende Abschnitt beschreibt daher, **was zu tun wäre**, und darunter steht, was der Compiler heute tatsächlich liefert. Schritt 1 — Strukturübersicht der Entscheidungspunkte: lyxc src/altitude.lyx -I build/ --mcdc-report -o /dev/null [MC/DC] Coverage structure analysis [MC/DC] Functions analyzed: 4 [MC/DC] Total decision points: 3 [MC/DC] ProcessSensorFrame: 1 decisions, 1 conditions → min 2 test cases [MC/DC] Decision point details: [MC/DC] point #0 in 'ProcessSensorFrame': if (node 12) Damit sind die Entscheidungspunkte **aufgefunden**. Die Zahl hinter „conditions" ist unbrauchbar — sie lautet immer 1, auch bei ''a && b && c''; Entscheidungen in einem ''return''-Ausdruck fehlen ganz. Schritt 2 — Testvektoren von Hand herleiten. Für eine Entscheidung mit //n// Bedingungen sind //n+1// Testfälle nötig; die Tabelle im [[lyx_-_programmiersprache:guides:do-178c|DO-178C-Guide]] zeigt das Verfahren für drei Bedingungen. Schritt 3 — Überdeckung außerhalb des Compilers belegen: ein Testrahmen, der jede Bedingungskombination und deren Ergebnis mitschreibt, liefert den Nachweis. Der Compiler kann ihn nicht erbringen. Ein Bericht wie der folgende ist **derzeit nicht erzeugbar** und steht hier nur, um das Ziel zu zeigen: Coverage Report — AltitudeMonitor ══════════════════════════════════════════════════════════════ Function Line Branch MC/DC ────────────────────────────────────────────────────────────── ProcessSensorFrame 100% 100% 100% ✓ PressureToAltitude 100% 100% 100% ✓ ComputeConfidence 100% 100% 88% ✗ ← DAL-B: OK, DAL-A: nicht ausreichend ClassifyAltitude 100% 100% 100% ✓ ────────────────────────────────────────────────────────────── GESAMT 100% 100% 97% ══════════════════════════════════════════════════════════════ DAL-B Anforderung: 100% MC/DC für alle @dal(B)-Funktionen — PASS Was das Ergebnis bedeutet: ''ComputeConfidence'' hat 88 % MC/DC. Für DAL-B ist das kein Problem — die Funktion ist nicht mit ''@dal(B)'' annotiert. Wäre das Projekt DAL-A, müsste ein weiterer Testfall ergänzt werden, der die fehlende Kombination abdeckt. ==== MC/DC-Lücke schließen (DAL-A Beispiel) ==== Der Report zeigt, welche Bedingung fehlt: [mcdc-gap] ComputeConfidence — Bedingung 'frame.valid' hat keinen Test, bei dem 'p_ok && t_ok = true' aber 'frame.valid' allein das Ergebnis bestimmt. Fehlende Kombination: valid=true, p_ok=true, t_ok=true → nur valid=false dreht Ergebnis. Zusätzlichen Testfall ergänzen: // TC-11: MC/DC — valid=false bei sonst gültigen Werten fn TC11_MCDC_ValidAlone(): void { var frame_valid := MakeFrame(101325, 15, true); var frame_invalid := MakeFrame(101325, 15, false); var r_valid: AltitudeResult := ProcessSensorFrame(frame_valid); var r_invalid: AltitudeResult := ProcessSensorFrame(frame_invalid); // Nur 'valid' unterscheidet sich — MC/DC-Nachweis für diese Bedingung test.Assert( r_valid.valid, "TC-11: valid=true → result.valid = true"); test.Assert(!r_invalid.valid, "TC-11: valid=false → result.valid = false"); } ---- ===== 10. Provenance und Audit-Log ===== Für die Zertifizierung muss nachweisbar sein, dass der gelieferte Maschinencode aus dem geprüften Quellcode entstanden ist — bit-identisch, reproduzierbar. # Reproduzierbaren Final-Build mit vollständigem Audit-Log erzeugen lyxc src/altitude.lyx \ -I build/ \ --lint \ --static-analysis \ --provenance \ --trace-passes \ --target=arm64 \ -o build/altitude_final.elf \ 2>&1 | tee evidence/provenance.log ''--provenance'' schreibt für jede IR-Transformation einen signierten Eintrag ins Log: [provenance] Source: src/altitude.lyx SHA256: a3f8...c291 [provenance] Unit: build/types.lyu SHA256: 7b21...e04a [provenance] Pass 01: parse → AST [provenance] Pass 02: type-check → typed AST [provenance] Pass 03: range-check → annotated AST [provenance] Pass 04: lower → IR [provenance] Pass 05: mcdc → instrumented IR [provenance] Pass 06: codegen arm64 → ELF [provenance] Output: build/altitude_final.elf SHA256: 19d4...f7a2 [provenance] Compiler: lyxc 1.0.16F [provenance] Flags: --lint --static-analysis --provenance --trace-passes --target=arm64 [provenance] Timestamp: 2026-05-22T14:30:00Z ''--build-info'' zeigt die Compiler-Version und Build-Konfiguration, die im Abnahmedokument festgehalten wird: lyxc --build-info Compiler Build Information: Name: lyxc Version: 1.0.19E Build: bootstrap Target: x86_64-linux-elf Mehr als diese vier Angaben liefert der Schalter nicht — Baudatum, Reproduzierbarkeit und FIPS-Status, die frühere Fassungen dieses Tutorials zeigten, gibt es nicht. Für ein Abnahmedokument sind Datum und Zielplattform daher gesondert festzuhalten. ''%%--%%config'' (TOR-003) ergänzt die Angaben um die verfügbaren Zielplattformen, Architekturen und Ausgabeformate. Der Schalter arbeitet seit der Behebung von [[https://github.com/SEOLizer/LyX-Compiler/issues/1527|#1527]] korrekt und endet mit Exit 0 — ältere Fassungen dieses Tutorials rieten davon ab. ---- ===== 11. Nachweis-Checkliste nach DAL-Level ===== Die folgende Tabelle zeigt, welche Schritte aus diesem Tutorial für welches DAL-Level verpflichtend sind. ^ Nachweis ^ DAL-A ^ DAL-B ^ DAL-C ^ DAL-D ^ | ''--lint'' (DO-178C-Konformitätsprüfung) | ✓ | ✓ | ✓ | ✓ | | ''--static-analysis'' | ✓ | ✓ | ✓ | — | | ''@stack_limit'' (bei jeder Übersetzung geprüft) | ✓ | ✓ | — | — | | ''--call-graph'' (Call-Graph-Dokumentation) | ✓ | ✓ | ✓ | — | | 100 % MC/DC — **ausserhalb des Compilers** (#1524) | ✓ | ✓ | — | — | | Statement Coverage 100 % | ✓ | ✓ | ✓ | ✓ | | Branch Coverage 100 % | ✓ | ✓ | ✓ | — | | Traceability über ''--provenance'' (seit 1.0.20F nutzbar, #1523) | ✓ | ✓ | — | — | | ''--trace-passes'' (Audit-Log) | ✓ | — | — | — | | ''@redundant'' (TMR) für Zustandsvariablen | ✓ (empfohlen) | — | — | — | | ''@integrity(mode: software_lockstep)'' | ✓ (empfohlen) | — | — | — | | Boundary Value Analysis in Tests | ✓ | ✓ | ✓ | — | | ''@dal''-Annotation im Quellcode | ✓ | ✓ | ✓ | ✓ | ---- ===== 12. Vollständiger Build-Ablauf (Skript) ===== Das folgende Skript führt alle Schritte in der richtigen Reihenfolge aus und legt alle Nachweise im ''evidence/''-Verzeichnis ab. Es kann als Basis für eine CI/CD-Pipeline oder einen manuellen Abnahme-Build dienen. #!/bin/bash set -e # Abbruch bei jedem Fehler echo "=== AltitudeMonitor — Safety Build ===" # 1. Typen-Unit kompilieren lyxc src/types.lyx \ --compile-unit \ --lint \ -o build/types.lyu # 2. Hauptkomponente — Lint + Statische Analyse lyxc src/altitude.lyx \ -I build/ \ --lint \ --static-analysis \ --call-graph -o evidence/call_graph.dot \ --target=arm64 \ -o build/altitude.elf \ 2>&1 | tee evidence/static_analysis.log # 3. Tests bauen und ausführen lyxc tests/altitude_test.lyx \ -I build/ \ --lint \ -o build/altitude_test.elf ./build/altitude_test.elf # 4. MC/DC-Instrumentierung und Coverage lyxc src/altitude.lyx \ -I build/ \ --mcdc-report \ --target=arm64 \ -o /dev/null > evidence/mcdc_struktur.log 2>&1 # Testprogramm getrennt uebersetzen — ein --link gibt es nicht, # die Unit wird ueber -I eingebunden lyxc tests/altitude_test.lyx \ -I build/ \ -o build/altitude_test.elf ./build/altitude_test.elf # Eine Coverage-Datei entsteht dabei nicht (#1524) — der Nachweis # ist ausserhalb des Compilers zu fuehren. # 5. Final-Build mit Provenance lyxc src/altitude.lyx \ -I build/ \ --lint \ --static-analysis \ --provenance \ --trace-passes \ --target=arm64 \ -o build/altitude_final.elf \ 2>&1 | tee evidence/provenance.log # 6. Call-Graph als PNG (optional, benötigt Graphviz) if command -v dot &> /dev/null; then dot -Tpng evidence/call_graph.dot -o evidence/call_graph.png fi echo "" echo "=== Build erfolgreich ===" echo "Nachweise in evidence/:" ls -lh evidence/ ---- ===== Zusammenfassung ===== ^ Schritt ^ Kommando ^ Artefakt ^ | Typen-Unit | ''lyxc --compile-unit --lint'' | ''build/types.lyu'' | | Safety-Build | ''--lint --static-analysis --runtime-checks'' | ''build/altitude.elf'' | | Tests ausführen | ''./build/altitude_test.elf'' | Konsolenausgabe | | Statische Analyse | ''--static-analysis'' | ''evidence/static_analysis.log'' | | Call-Graph | ''--call-graph'' | ''evidence/call_graph.dot'' | | Stack-Prüfung | ''@stack_limit'' im Quelltext — kein Flag | Compiler-Fehler bei Überschreitung | | MC/DC-Coverage | ''--mcdc'' + ''--mcdc-report'' | Bericht auf stdout | | Provenance | ''--provenance --trace-passes'' | ''evidence/provenance.log'' | → [[lyx_-_programmiersprache:guides:aerospace-safety|Zurück: Aerospace & Safety – Sprachreferenz]] 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)'' in der Attributtabelle auf ''mode: software_lockstep'' berichtigt — ''lockstep'' ist kein gültiger Modus.