ProMoSA - Probabilistic Models for Safety Analysis
Final Report Abstract
Das Forschungsprojekt "Probabilistic Models for Safety Analysis" (ProMoSA) hatte das Ziel, eine exakte modellbasierte Analyse der Sicherheit technischer Systeme zu ermöglichen. Bisher waren solche Analysen sehr zeitaufwändig und kompliziert. Grundlage für die Analyse sind dabei formale Methoden. Als Verfahren zur Modellverifikation wird symbolisches und probabilistisches Model-Checking verwendet. Die wesentlichen drei Herausforderungen waren dabei: (1) Die effiziente Erstellung formaler Modelle, die sowohl für (temporal-)logische als auch probabilistische Verifikation verwendet werden können. (2) Die automatisierte Analyse der Sicherheit und Zuverlassigkeit auf Grundlage dieser Modelle. (3) Die einfache Möglichkeit der Optimierung solcher Modelle unter Berücksichtigung gegenläufiger Ziele. Die in ProMoSA entwickelten Techniken und Algorithmen bieten die Möglichkeit diese Herausforderungen zu stemmen. Kernelement ist dabei die Modellierungssprache SAML (System Analysis and Modelling Language). Sie ermöglicht sehr einfach formale Modelle als Abstraktion technischer Systeme zu entwerfen. SAML erlaubt dabei die Spezifikation deterministischen und indeterministischen Verhaltens genauso wie die Modellierung probabilistischen Verhaltens. Ein weiteres Kernelement ist die Möglichkeit Modellfamilien zu definieren und je nach Bedarf einzelne Modelle daraus zu instanziieren. Dies erlaubt eine sehr flexible Modellierung. Auf Basis dieser so entworfenen Modelle können Systementwickler das qualitative bzw. quantitative Verhalten analysieren. Andere Modellierungssprachen waren hier bisher auf eine einzige Verifikationsart beschränkt. Zudem sind innerhalb des Projektes für SAML-Modelle Transformationsalgorithmen geschaffen worden, die es ermöglichen, ein SAML-Modell mit verschiedenen Verifikationswerkzeugen zu analysieren. Im Speziellen sind SAML-Modelle in die Eingabesprachen von ModelCheckern wie PRISM und NuSMV übersetzbar. Die angewendeten Transformationen sind formal bewiesen, sodass die Rückführung der Ergebnisse der Verifikationen auf das SAML-Modell valide ist. Dies erlaubt Systementwicklern schon im Modellierungsprozess valide Sicherheitsaussagen über ihr zu entwickelndes System zu erhalten und die Modellierung entsprechend anzupassen. Für diese Arbeiten wurde eine innerhalb des Projektes abgeschlossene Promotion mit dem Ernst-Denert-Preis ausgezeichnet. Des Weiteren wurde in ProMoSA ein Optimierungsframework geschaffen, das es erlaubt Modelle zu parametrisieren und auf Basis gegenläufiger Zielfunktionen optimale Parameterkonstellationen zu finden. Insbesondere ist es möglich, dass Sicherheitsanforderungen selbst Zielfunktionen sein können. Da multikriterielle Optimierungen (d.h. Optimierungen mit mehreren Zielfunktionen) möglich sind, konnen Systementwickler selbst für gegenläufige Zielfunktionen bspw. Sicherheit gegen Systemkosten bestmögliche Modelle finden. Zur Beschleunigung dieser Optimierung werden u.a. Näherungs- und Schätzverfahren wie Krige-Schätzer oder künstliche neuronale Netze angewendet. An diversen Fallstudien zeigte sich, dass die in ProMoSA entwickelten praktikabel einsetzbar sind. Darunter sind u.a. das Modell eines Fahrzeugairbags, eines Überholspursystems für Eisenbahnen, eines Notstromgenerators, die Landeklappensteuerung eines Flugzeuges oder der punktförmigen Zugbeeinflussung, die heute noch Anwendung in deutschen Zügen findet. Für die Umsetzung der Fallstudie wurden alle entwickelten Techniken und Algorithmen innerhalb einer integrierten Entwicklungsumgebung für SAML namens VECS (Verification Environment for Critical Systems) implementiert. VECS bietet dabei die Möglichkeit ein SAML Modell effizient zu erstellen. Basis sind dabei technische Möglichkeiten, wie die automatische Modellvalidierung oder das schrittweises Testen von Modellen (Debugging). Des Weiteren liefert VECS die entwickelten Transformationsalgorithmen mit, sodass Systementwickler ohne großes Expertenwissen Verifikationen mit externen ModelCheckern durchführen können. Dabei bietet VECS die Möglichkeit die Ergebnisse der Verifikation für den Nutzer im Modell zu visualisieren. Zusammenfassend kann man feststellen, dass durch ProMoSA neue Methoden geschaffen wurden um sicherheitskritische Systeme besser analysieren zu können. Dies betrifft sowohl die Effizienz beim Erstellen von formalen Spezifikationen als auch die, bisher nicht vorhandene, Möglichkeit formale Modelle hinsichtlich gewünschter Zielfunktionen wie Produktionskosten oder Zuverlässigkeit zu optimieren.
Publications
- "Practical Experiences in Model-Based Safety Analysis“. In: Proceedings: International Workshop on Digital Engineering. ACM Proceedings, 2011
Frank Ortmeier, Michael Lipaczewski und Matthias Güdemann
- "Qualitative and Quantitative Formal Model-Based Safety Analysis“. Diss. Otto-von-Guericke-Universität Magdeburg, 2011
Matthias Gödemann
- "Multi-Objective Optimization of Formal Specifications“. In: IEEE 14th International Symposium on High-Assurance Systems Engineering (HASE 2012). 2012
Simon Struck, Matthias G¨demann, Michael Lipaczewski und Frank Ortmeier
- "Using model-based analysis in certification of critical software-intensive systems“. In: GI-Edition-Lecture Notes in Informatics (LNI) 199 (2012)
Frank Ortmeier, Simon Struck und Michael Lipaczewski
- "Efficient Optimization of Large Probabilistic Models“. In: Journal of Systems and Software 86 (2013), S. 2488–2501
Simon Struck, Matthias Güdemann und Frank Ortmeier
- "A Graphical Notation for Probabilistic Specifications“. In: Verification and Assurance VeriSure 2014. Position Paper
Sebastian Nielebock, Tim Gonschorek und Frank Ortmeier
