====== Triple Modular Redundancy (TMR) ======

**Triple Modular Redundancy (TMR)** ist ein Hardware-Fehlertoleranzprinzip, das Lyx auf Software-Ebene implementiert: Kritische Werte werden **dreifach im RAM** gespeichert. Jeder Lesezugriff führt einen Mehrheitsentscheid durch — zwei von drei Kopien müssen übereinstimmen. Eine abweichende Kopie wird automatisch repariert (Self-Healing).

Zweck: Schutz gegen **Single Event Upsets (SEU)** — Bit-Flips in SRAM durch kosmische Strahlung. Im Erdorbit tritt ein SEU typischerweise alle 10–100 Stunden pro MBit Speicher auf. In erdnahen Orbits und auf Reiseflughöhen ist die Rate messbar erhöht.

→ Verwandt: [[lyx_-_programmiersprache:do-178c:software-lockstep|Software Lockstep]] · [[lyx_-_programmiersprache:do-178c:memory-scrubbing|Memory Scrubbing]] · [[lyx_-_programmiersprache:do-178c|DO-178C Hauptseite]]

----

===== 1. @redundant — Syntax und Verhalten =====

Das Pragma ''@redundant'' auf einer globalen Variable veranlasst den Compiler, drei physisch getrennte Speicherbereiche anzulegen:

<code lyx>
@redundant
var thrust_setpoint: int64 := 0;

@redundant
var autopilot_engaged: bool := false;

@redundant
var nav_heading: f64 := 0.0;
</code>

==== Was der Compiler generiert ====

Intern legt der Compiler an:

<code lyx>
// Konzeptuelle Darstellung — tatsächlich vom Compiler erzeugt, nicht manuell schreiben
var _thrust_setpoint_copy1: int64 @ section(".tmr_a");
var _thrust_setpoint_copy2: int64 @ section(".tmr_b");
var _thrust_setpoint_copy3: int64 @ section(".tmr_c");
</code>

Die drei Sektionen (''.tmr_a'', ''.tmr_b'', ''.tmr_c'') werden im Linker-Script auf physisch weit entfernte Speicheradressen gelegt — das verhindert, dass ein lokaler Speicherdefekt alle drei Kopien gleichzeitig trifft.

==== Schreiben: alle drei Kopien simultan ====

<code lyx>
// Schreibzugriff im Quellcode:
thrust_setpoint := 850;

// Compiler-generierter Code (konzeptuell):
//   _thrust_setpoint_copy1 := 850;
//   _thrust_setpoint_copy2 := 850;
//   _thrust_setpoint_copy3 := 850;
</code>

==== Lesen: Majority Vote ====

<code lyx>
// Lesezugriff im Quellcode:
var t: int64 := thrust_setpoint;

// Compiler-generierter Code (konzeptuell):
//   if copy1 = copy2 { t := copy1; copy3 := copy1; }
//   else if copy1 = copy3 { t := copy1; copy2 := copy1; }
//   else if copy2 = copy3 { t := copy2; copy1 := copy2; }
//   else { panic("TMR triple-fault — no majority"); }
</code>

Solange maximal **eine** der drei Kopien korrumpiert ist, gibt der Mehrheitsentscheid immer den korrekten Wert zurück und repariert die defekte Kopie. Erst wenn zwei Kopien gleichzeitig korrumpiert sind (sehr unwahrscheinlich), schlägt der Mehrheitsentscheid fehl.

----

===== 2. Vollständiges Beispiel: Flugsteuerung =====

<code lyx>
unit flight_tmr;
import std.io;

type Altitude = int64 range -1000..60000;
type Speed    = int64 range 0..1000;

// Kritische Zustandsvariablen — alle dreifach
@redundant var current_altitude:  Altitude := 0;
@redundant var target_altitude:   Altitude := 0;
@redundant var airspeed:          Speed    := 0;
@redundant var autopilot_active:  bool     := false;
@redundant var flight_phase:      int64    := 0;   // 0=ground, 1=climb, 2=cruise, 3=descent

// Schreiben: sicher — alle drei Kopien aktualisiert
fn UpdateAltitude(measured_m: int64): void {
    current_altitude := measured_m as Altitude;
}

// Lesen: Majority Vote transparent
@dal(A)
@flight_crit
@wcet(50)
fn GetAltitudeError(): int64 {
    return target_altitude - current_altitude;   // Beide reads sind Majority-Votes
}

fn main(): int64 {
    autopilot_active := true;
    target_altitude  := 10000 as Altitude;

    UpdateAltitude(8500);

    var err: int64 := GetAltitudeError();
    PrintStr("Höhenfehler: "); PrintInt(err); PrintStr(" m\n");
    // Ausgabe: Höhenfehler: 1500 m

    return 0;
}
</code>

----

===== 3. TMR auf Arrays =====

''@redundant'' kann auch auf statische Arrays angewendet werden:

<code lyx>
// Waypoint-Liste dreifach im RAM
@redundant
var waypoints: [16]Waypoint := [];

@redundant
var waypoint_count: int64 := 0;

fn AddWaypoint(wp: Waypoint): bool {
    if (waypoint_count >= 16) { return false; }
    waypoints[waypoint_count] := wp;   // Schreibt alle drei Kopien
    waypoint_count := waypoint_count + 1;
    return true;
}
</code>

> **Hinweis:** Bei Array-Elementen wird der Majority-Vote pro **Element** durchgeführt, nicht über das gesamte Array. Das erhöht die Resilienz: Ein SEU in Kopie 2 bei Index 5 wird beim Lesezugriff auf Index 5 repariert, ohne andere Elemente zu beeinflussen.

----

===== 4. TMR-Verifizierung im Build =====

Der Flag ''--verify-tmr'' lässt den Compiler prüfen, ob alle ''@redundant''-Variablen korrekt auf drei physisch getrennte Speicherbereiche abgebildet wurden:

<code lyx>
// lyxc --target=arm64 --verify-tmr src/flight_tmr.lyx
//
// Ausgabe bei Erfolg:
//   [TMR] thrust_setpoint: copy1@0x40010000, copy2@0x40015000, copy3@0x4001A000 ✓
//   [TMR] autopilot_active: copy1@0x40010008, copy2@0x40015008, copy3@0x4001A008 ✓
//   [TMR] All 8 @redundant variables verified.
//
// Ausgabe bei Fehler (Kopien zu nahe beieinander):
//   [TMR] WARNING: nav_heading copies within same 4KB page — SEU risk elevated
//   → Linker-Script anpassen: .tmr_b und .tmr_c auf andere Pages verteilen
</code>

----

===== 5. Kombination: @redundant + @integrity =====

Für maximale DAL-A-Absicherung kombiniert man TMR für Daten (''@redundant'') mit Software Lockstep für Berechnungen (''@integrity''):

<code lyx>
@redundant
var flight_state_hash: int64 := 0;   // Geprüfte Zustandssignatur

@dal(A)
@flight_crit
@integrity(mode: software_lockstep, interval: 50)
@stack_limit(2048)
@wcet(200)
fn VerifyAndUpdateState(new_state: ^FlightState): bool {
    // software_lockstep: Berechnung wird dupliziert und verglichen
    var computed_hash: int64 := HashState(new_state);

    // @redundant: Lesezugriff ist Majority-Vote
    if (computed_hash = flight_state_hash) {
        return true;
    }

    // Zustandsabweichung — Recovery
    return false;
}
</code>

----

===== 6. Grenzen von TMR =====

^ Szenario ^ TMR-Verhalten ^
| 1 von 3 Kopien korrumpiert | ✅ Erkannt und repariert (Majority Vote) |
| 2 von 3 Kopien gleichzeitig korrumpiert | ✗ Mehrheitsentscheid liefert falschen Wert — nicht erkennbar |
| SEU in der Vote-Logik selbst | Schutz durch ''@integrity(software_lockstep)'' auf der Vote-Funktion |
| Systematischer SW-Fehler | TMR schützt nicht — alle drei Kopien haben denselben Fehler |
| Schreibfehler (Kopie wird falsch geschrieben) | ✗ Alle drei Kopien gleichzeitig falsch — TMR erkennt nichts |

> **TMR schützt gegen zufällige Hardware-Fehler (SEUs), nicht gegen systematische Software-Fehler.** Für systematische Fehler ist MC/DC-Coverage der richtige Ansatz.

----

Letzte Aktualisierung: 2026-05-22