Kurzfassung

Dr. Heiko Dörr, Sophia Kohle, Matthias Kirchner, MES
Georg Walde, TU Berlin
Absicherung von Modelltransformationen für
sicherheitsrelevante Avionik‐Software
Der Einsatz qualifizierter Code-Generatoren (z.B. für SCADE) und verifizierter Compiler (z.B. CompCert)
sind ein wesentlicher Baustein für die Absicherung von elektronischen Steuerungs‐ und
Regelungssystemen in der Avionik. Diese enthalten komplexe und sicherheitskritische Funktionen, wie
bspw. elektronische Flugsteuerungen. In der frühen Phase der Entwicklung wird der Flugregler spezifisch
für das geplante Fluggerät entworfen. Die für die Flugeigenschaften relevanten Parameter werden dabei
in ein flugmechanisches Modell des Fluggeräts übertragen. Dieses Modell dient dann als Streckenmodell
für die Entwicklung und Auslegung des Flugreglers.
Die Kopplung des flugmechanischen Modells und des eigentlichen Flugreglers erlaubt die schnelle
Anpassung und Validierung von Reglerstrukturen und -parametern auf Veränderungen im Design des
Fluggeräts. Auch die Ergebnisse späterer Erprobungsflüge hinsichtlich der flugmechanischen
Eigenschaften können in das Simulationsmodell des Fluggeräts aufgenommen werden, sodass das
Modell als getreues Abbild des Fluggeräts verwendet werden kann. Entwicklungs- und Erprobungszyklen
für die Flugregelung können so deutlich verkürzt werden, denn diese kann kontinuierlich gegen das
Streckenmodell entwickelt und optimiert werden. Werkzeuge wie Simulink-/Stateflow sind für diese
integrierte Modellierung von Flugmechanik und Regler im breiten Einsatz. Zum Abschluss der Zulassung
erfolgt die Verifikation und Validierung des Flugreglers im Flugversuch.
Für die Übersetzung eines Reglermodells in die eingebettete Regelungssoftware gibt es verschiedene
Verfahren. Neben der herkömmlichen, manuellen Übertragung in C-Code gibt es im Wesentlichen zwei
Ansätze für die automatische Transformation: 1) Code-Generierung aus dem Reglermodell über eine
direkte Übersetzung mit Embedded Coder oder TargetLink in embedded C, oder 2) Transformation von
Simulink-/Stateflow nach SCADE mit anschließender Code-Generierung in der SCADE-Werkzeugkette.
Beide Ansätze haben ihre Berechtigung und müssen entsprechend der strategischen Randbedingungen
eines Projekts bewertet werden.
Im Projekt MCAS haben wir die technischen Voraussetzungen für den Ansatz 2) untersucht. Die
Transformation kann über ein marktgängiges Werkzeug wie das „SCADE Suite Gateway for Simulink“
durchgeführt werden. Auf Grund der semantischen Differenzen zwischen SCADE und Simulink/Stateflow,
aber auch der Vielfalt von Modellierungskonstrukten sind nicht alle Simulink-/Stateflow-Modelle
übersetzbar. In unserer Studie haben wir die bestehende Dokumentation des SCADE Suite Gateway for
Simulink untersucht. Eine große Zahl weiterer Einschränkungen an Simulink-/Stateflow-Modell wurden
durch die Transformationen realer Modelle ergänzt. Insgesamt konnten rund 100 Regeln gefunden
werden, die die Voraussetzungen für eine erfolgreiche Transformation beschreiben. Die Regeln fallen in
verschiedene Klassen:
·
Regeln zur Modellparametrisierung
·
Allgemeine Modellierungsregeln
·
Spezifische Regeln für Simulink
·
Spezifische Regeln für Stateflow
·
Regeln für erfolgreichen Modellvergleich
Etliche dieser Regeln entsprechen best-practices der modell-basierten Entwicklung - sollten also
unabhängig vom Einsatzzweck eingehalten werden. Andere Regeln sind spezifische Anforderungen, die
aus den Anforderungen für eine erfolgreiche Modelltransformation abgeleitet sind. Es ist noch zu prüfen,
ob diese künftig auch als allgemeine best-practices bewertet werden können und so die Qualität von
Modellen in der SW-Entwicklung weiter absichern können.

Download Report