Zur Übersicht →
Modul 01 / 04
Vier Laufzeitfragen.
Stufe 2 beginnt erst, nachdem das Softwaremodell gegen die mathematische Spezifikation verifiziert wurde.
Was der Regler berechnen muss.Abschnitt öffnen
Mathematische Spezifikation
Vier Laufzeitfragen.
01 / ZUSTAND
Was hat sich geändert?
Den erweiterten Zustand Z(t) schätzen: Streckenzustand, physische Ressourcen, Modellgültigkeit und aktive Konfiguration.
02 / LEISTUNGSFÄHIGKEIT
Was ist noch möglich?
Verbleibende Ressourcen auf Funktionen und Missionswert jeder verifizierten Konfiguration abbilden.
03 / ZULÄSSIGKEIT
Welche Übergänge sind erlaubt?
Kandidaten verwerfen, die Machbarkeit, Stabilität, Safety oder den verifizierten Konfigurationsgraphen verletzen.
04 / ZEIT
Wann darf geschaltet werden?
Reaktionslatenz, Umschaltzeit und Mindestverweilzeit vor dem nächsten Trajektorienschritt einhalten.
Evidenz aus dem praktischen Simulationspaper
Berichtete Ergebnisse der Referenzsoftware.
WCET der Regelschleife\(42\,\mu\mathrm{s}\)
Indikatorberechnung\(8\,\mu\mathrm{s}\)
Notfallreaktion\(4.2\,\mathrm{ms}\)
Code + Daten\(48\,\mathrm{KB}\)
Diese Werte stammen aus der Referenzimplementierung des Papers. Sie belegen Machbarkeit, sind jedoch keine plattformunabhängigen Garantien.