Gerichtete und parallele Validierung von abstrakten Spezifikationen
Final Report Abstract
Formale Methoden haben das Ziel, basierend auf mathematischen Analysen, fehlerfreie Software zu produzieren. Die B-Methode ist solch eine formale Methode, die erfolgreich in der Industriepraxis eingesetzt wird. Zum Beispiel benutzten in 2014 weltweit 25 % der fahrerlosen U-Bahnzüge Software die auf Basis der B-Methode erstellt wurde. Die B-Methode garantiert, dass die entwickelte Software einer formalen Spezifikation entspricht. Mit steigender Komplexität der Anforderungen an Softwaresysteme, wird aber auch das Erstellen korrekter Spezifikationen schwieriger; daher stellt die Korrektheit der Anfangspezifikation einen kritischen Punkt dar. Das Hauptziel dieses Forschungsprojektes war es, Methoden und Werkzeuge zu entwickeln, mit denen aus Industrieprojekten stammende, komplexe, formale B-Spezifikationen validiert werden können. Eine besondere Herausforderung war dabei die hohe Ausdruckskraft der B Spezifikationssprache. Alle Gepavas Techniken sind praktisch in unserem Werkzeug ProB umgesetzt worden und stehen der Öffentlichkeit zur Verfügung (http://www.stups.hhu.de/ProB). Die größten Fortschritte des Projekts waren dabei: - optimiertes, paralleles und beweisgerichtete Modellprüfung für industrielle Anwendungen mit sehr großen Zustandsräumen, - eine Technik um B Modelle und Systeme, trotz eines hohen Anteils an Nebenläufigkeit, effizient zu validieren, - die Möglichkeit, dank gerichteter Modellprüfung, Fehler auch in unendlichen Zustandsräumen zu finden, - eine Technik zur Konsistenzprüfung der Benutzung physikalischer Einheiten in industriellen formalen Modellen und Systemen. Ein besonderer Erfolg des Projekts ist die neue Methode zur parallelen Modellprüfung. Der Rechenaufwand wird dabei automatisch auf verschiedene Rechner verteilt und skaliert selbst bei einer großen Anzahl an Rechnern. Die Laufzeit wurde dabei um bis zu zwei Größenordnungen verbessert und es können nun formale Modelle mit Milliarden von Zuständen auch verteilt in der “Cloud” validiert werden. Das DFG Projekt hat in wichtigem Maße zur Verbesserung des Standes der Technik und Forschung auf dem Gebiet der formalen B Methode beigetragen. Dank des Projekts wurde auch das Werkzeug ProB weiterentwickelt und die Neuentwicklungen der Wissenschaftsgemeinde zur Verfügung gestellt (mittlerweile gibt es mehr als 580 Zitationen für die zwei Hauptartikel über ProB, und etliche akademische und industrielle Werkzeuge wie DTVT, SafeCap, iUML-B, HRemo, B4MSecure, oder VTG bauen auf ProB auf). ProB wird zur Validierung von sicherheitskritischen Bahnsystemen verwendet, und wurde weltweit zur Prüfung mehrere fahrerloser U-Bahnlinien eingesetzt. ProB wird in diesem Rahmen bei Firmen wie Siemens, Alstom, und General Electric in der täglichen Praxis eingesetzt. Im Rahmen des Projekts Gepavas haben wir auch eine Brücke zu anderen Forschungsgebieten geschlagen, unter anderem zur Sprache TLA+, welche auch durch den Turing Preis von Leslie Lamport in 2013 vermehrt im Ramplenlicht steht (siehe http://amturing.acm.org/award_ winners/lamport_1205376.cfm).
Publications
- Automatic Flow Analysis for Event-B. In Proceedings of Fundamental Approaches to Software Engineering (FASE) 2011, volume 6603 of Lecture Notes in Computer Science, Springer, 2011
Jens Bendisposto, Michael Leuschel
- Inferring Physical Units in B Models. In Proceedings SEFM’2013, LNCS 8137, Springer, 2013
Sebastian Krings, Michael Leuschel
- Parallel Model Checking of B Specifications. In Proceedings of the 4th Rodin User and Developer Workshop, TUCS Lecture Notes, TUCS, 2013
Jens Bendisposto, Philipp Körner, Michael Leuschel
- Optimising the ProB Model Checker for B using Partial Order Reduction. In SEFM 2014, LNCS 8702, 2014
Ivaylo Dobrikov, Michael Leuschel
(See online at https://doi.org/10.1007/s00165-015-0351-1) - Translating B to TLA+ for Validation with TLC. In Proceedings ABZ’14, LNCS 8477, 2014
Dominik Hansen, Michael Leuschel
(See online at https://doi.org/10.1007/978-3-662-43652-3_4) - Directed and Distributed Model Checking of B-Specifications. PhD Thesis, University of Düsseldorf. January 2015
Jens Bendisposto
- Optimising the ProB Model Checker for B using Partial Order Reduction. Formal Aspects of Computing, April 2016, Volume 28, Issue 2, pp 295–323
Ivaylo Dobrikov, Michael Leuschel
(See online at https://doi.org/10.1007/978-3-319-10431-7_16) - Translating B to TLA + for Validation with TLC. Elsevier
Science of Computer Programming
Volume 131, 1 December 2016, Pages 109-125
Dominik Hansen, Michael Leuschel
(See online at https://doi.org/10.1007/978-3-662-43652-3_4) - Inferring Physical Units in Formal Models. Software & Systems Modeling, February 2017, Volume 16, Issue 1, pp 25–47
Sebastian Krings, Michael Leuschel
(See online at https://doi.org/10.1007/s10270-015-0458-0)
