Software Safety

Programm

Beginn: 9:00

 

Obleute der Fachausschüsse L6.3 und Q3.4 der DGLR

Begrüßung der Teilnehmer

Markus Hochstrasser, Prof. Florian Holzapfel
Institute of Flight System Dynamics
Technische Universität München

Markus Hornauer
samoconsult GmbH

Formal Verification of Flight Control Applications along a Model-Based Development Process: A case study

Dr. Heiko Dörr, Sophia Kohle, Matthias Kirchner
MES Model Engineering Solutions GmbH

Georg Walde
Technische Universität Berlin

Absicherung von Modelltransformationen für sicherheitsrelevante Avionik-Software

Dr. Harald Rueß, Dr. Tewodros Beyene
fortiss GmbH

Wie können formale Verifikationstechniken das Code Review unterstützen und verbessern?

Dr. Rainer Gerlich, Dr. Ralf Gerlich
BSSE System and Software Engineering (BSSE)

Ergebnisse und Empfehlungen aus der Fehleranalyse von Raumfahrtsoftware

Christoph Torens, Florian Adolf, Sebastian Schirmer
Deutsches Luft- und Raumfahrtzentrum (DLR)

Auf dem Weg zur unbemannten Luftfracht durch Laufzeitabsicherung

Fr. Prof. Dr. Saglietti
Lehrstuhl für Software Engineering (Informatik 11)
Universität Erlangen-Nürnberg

Testverfahren zur Fehlererkennung und zur Zuverlässigkeitsbewertung für kooperierende mobile Agenten

Prof. Dr. Stefan Wagner
Universität Stuttgart

Systemtheoretische Analyse und Verifikation von Software-Safety

Richard Seitz
DGLR Q3.4

Schlusswort

Bei Bedarf können die Dokumente zu den jeweiligen Vorträgen bei den Obleuten des Fachausschuss angefordert werden.

Bericht

Am 5. Oktober 2016 fand der gemeinsame Workshop „Software Safety“ der Fachausschüsse L6.3 Flugregelung und Q3.4 Softwareengineering der deutschen Gesellschaft für Luft- und Raumfahrt (DGLR) am Institut für Luft- und Raumfahrt der Technischen Universität München in Garching statt. Zu Beginn begrüßten die Leiter des Fachausschusses Q3.4, Richard Seitz und Frank Dordowsky, die mehr als 50 Workshopteilnehmer aus Forschung und Industrie.

Als erster Redner schilderte Markus Hochstrasser vom Institut für Flugsystemdynamik der TU München in seinem Vortrag „Formal Verification of Flight Control Applications along a Model-Based Development Process: A case study“ die Anwendung von Model Checking und abstrakter Interpretation auf drei unterschiedlich geartete, am Lehrstuhl entwickelte Matlab/Simulink-Modelle und bewertete sie. Markus Hornauer von der samuconsult GmbH ordnete die von Hochstrasser dargestellten methodischen Ansätze in den Zulassungsprozess nach DO-178C und dessen Supplement für formale Methoden, die DO-333, ein.

Danach berichtete Matthias Kirchner von der Model Engineering Solutions GmbH (MES) in seinem Vortrag „Absicherung von Modelltransformationen für sicherheitsrelevante Avionik-Software“ von den Fortschritten des Projekts MCAS, über das Georg Walde im letztjährigen Workshop berichtet hatte. In dem Projekt wird ein existierendes Flugreglermodell von Simulink/Stateflow nach SCADE mithilfe des kommerziell verfügbaren Tools „SCADE Suite Gateway for Simulink“ übersetzt. Dies funktioniert nur dann, wenn mehr als 100 Regeln bei der Erstellung des Matlab/Simulink-Modells eingehalten werden. Die Überprüfung der Regeln in dem Modell soll möglichst automatisch durch das Werkzeug „Model Examiner MXAM“ erfolgen.

Während bei den ersten beiden Vorträgen die Software Safety im Kontext modellbasierter Entwicklungen stand, gingen die folgenden beiden Vorträge mehr auf die Verifikation von Quellcode ein. Dr. Harald Rueß von der Fortiss GmbH beschrieb in seinem Vortrag „Wie können formale Verifikationstechniken das Code Review unterstützen und verbessern?“ eine Kombination von Peer Reviews mit statischer Analyse, die unter dem Namen SCRUB am Jet Propulsion Laboratory der NASA konzipiert und von Fortiss weiter entwickelt wurde. Dabei stellte Dr. Rueß fest, dass ein einzelnes Analysewerkzeug nicht annähernd alle Fehler findet, so dass es ratsam ist, mehrere solcher Werkzeuge gleichzeitig einzusetzen.

Zu einem ähnlichen Ergebnis hinsichtlich der Sensitivität verfügbarer Analysewerkzeuge kam auch Dr. Ralf Gerlich von BSSE System and Software Engineering. In seinem Vortrag „Ergebnisse und Empfehlungen aus der Fehleranalyse von Raumfahrtsoftware“ illustrierte er anhand von Codebeispielen die Wirksamkeit der unterschiedlichen Werkzeuge und riet den Teilnehmern in seiner Zusammenfassung dazu, frühzeitig im Projekt Regeln zur Verifikation und zur Fehlerbehandlung aufzustellen sowie erkannte Schwachstellen zu dokumentieren und zu vermeiden.

Einen etwas anderen Weg ging Christoph Torens vom Deutschen Zentrum für Luft- und Raumfahrt (DLR). In seinem Vortrag „Auf dem Weg zur unbemannten Luftfracht durch Laufzeitabsicherung“ stellte er einen Monitoring-Ansatz vor, der auf das Konzept der EASA (European Aviation Safety Agency) für eine spezielle Risikokategorie von Luftfrachtdrohnen abgestimmt ist. Dabei werden formal spezifizierte Regeln zur Laufzeit überwacht und bei Verletzung der Regeln autonom Gegenmaßnahmen bis hin zur Terminierung des Flugs ergriffen.

Die beiden letzten Vorträge des Workshops stellten die Software Safety in den größeren Kontext der Systemsicherheit. Prof. Dr. Francesca Saglietti vom Lehrstuhl für Software Engineering der Universität Erlangen-Nürnberg stellte in ihrem Vortrag „Testverfahren zur Fehlererkennung und zur Zuverlässigkeitsbewertung für kooperierende mobile Agenten“ Verfahren zur Fehlererkennung den probabilistischen Verfahren zur Zuverlässigkeitsbewertung von Software gegenüber. Allerdings erfordern Aussagen zur Zuverlässigkeit eine sehr hohe Anzahl unabhängiger Testfälle, die nur automatisch generiert oder aus der Datenaufzeichnung zur Laufzeit gewonnen werden können. Zur Illustration einer Zuverlässigkeitsbewertung präsentierte Saglietti die modellbasierte Testfallgenerierung mit Hilfe farbiger Petri-Netze in den Projekten R3-COP und R5-COP des Verbands ARTEMIS (Advanced Research & Technology for Embedded Intelligent Systems).

Zum Abschluss des Workshops stellte Prof. Dr. Stefan Wagner von der Universität Stuttgart in seinem Vortrag „Systemtheoretische Analyse und Verifikation von Software-Safety“ den systemtheoretischen Ansatz STAMP und STPA von Nancy Leveson vom Massachusetts Institute of Technology (MIT) vor. An der Universität Stuttgart wird dieser Ansatz mit dem Open-Source-Werkzeug XSTAMPP implementiert und zusammen mit Industriepartnern evaluiert.

Richard Seitz vom DGLR Fachausschuss Q3.4 beschloss die Veranstaltung.

Die Vorträge wurden von umfangreichen Fragen und engagierten Diskussionen begleitet, die in den beiden Kaffeepausen und während des Mittagessens fortgesetzt wurden. Die Teilnehmer nutzten auch intensiv die Gelegenheit zu einem allgemeinen Informations- und Gedankenaustausch.

Ein herzliches Dankeschön geht an die Vortragenden für ihre hervorragenden Präsentationen. Ein ganz besonderer Dank geht an die Mitarbeiter des Lehrstuhls für Flugsystemdynamik von Prof. Dr. Holzapfel, Markus Hochstrasser und Kajetan Nürnberger, für ihre tatkräftige und sehr engagierte Unterstützung bei der Vorbereitung und Durchführung des Workshops. Wir möchten uns auch bei den Firmen Airbus Defence and Space und ESG Elektroniksystem- und Logistik-GmbH für die Übernahme der Kosten für die Verpflegung in den Pausen bedanken sowie bei der Technischen Universität München für die Überlassung des Hörsaals. Schließlich möchten wir uns bei allen Teilnehmern des Workshops bedanken, die durch ihre rege Beteiligung die Veranstaltung erst zu einem Workshop gemacht haben.

Danksagungen

Wir danken für die freundliche Unterstützung bei der Vorbereitung und Durchführung des Workshops: