Dokument: Directed and Distributed Model Checking of B-Specifications

Titel:	Directed and Distributed Model Checking of B-Specifications
URL für Lesezeichen:	https://docserv.uni-duesseldorf.de/servlets/DocumentServlet?id=34472
URN (NBN):	urn:nbn:de:hbz:061-20150618-111542-6
Kollektion:	Dissertationen
Sprache:	Englisch
Dokumententyp:	Wissenschaftliche Abschlussarbeiten » Dissertation
Medientyp:	Text
Autor:	Bendisposto, Jens Marco [Autor]
Dateien:	[Dateien anzeigen] Adobe PDF [Details] 2,41 MB in einer Datei [ZIP-Datei erzeugen] Dateien vom 17.06.2015 / geändert 17.06.2015
Stichwörter:	Formale Methoden, B-Methode, Model Checking
Dewey Dezimal-Klassifikation:	000 Informatik, Informationswissenschaft, allgemeine Werke » 004 Datenverarbeitung; Informatik
Beschreibungen:	Wir leben im Zeitalter der Software. Es gibt kaum ein technisches Gerät, das heute ohne Komponenten auskommt, die in Software realisiert sind. Software ist kostengünstig zu entwickeln und viel flexibler als Hardware. Die Kehrseite der Medaille ist jedoch: Softwarefehler können töten. Ein Fehler in der Synchronisation der nebenläufigen Software des THERAC-25 Linearbeschleunigers für die Strahlentherapie hat mindestens drei Menschen das Leben gekostet und weitere schwer verletzt. In solchen sicherheitskritischen Systemen kann man nicht die im Umfeld der typischen Anwendungsentwicklung dominante Methode zur Qualitätssicherung - das Testing - einsetzen. Solche Software erfordert striktere, mathematische Methoden, die sogenannten formalen Methoden. In dieser Arbeit beschäftigen wir uns mit der Verifikation von formalen Modellen in B und Event-B mit Hilfe des Model Checkers ProB. Das Ziel ist, den hohen Abstraktionsgrad der Modellierungssprachen auszunutzen, um signifikante Verbesserungen der Laufzeit zu erreichen. Dieses Ziel wurde erreicht. Es lassen sich mit den in dieser Arbeit vorgestellten Verbesserungen Modelle prüfen, deren Verifikation vorher nicht praktikabel war. Insbesondere die verteilte Version von ProB hat eine Verbesserung der Laufzeit von teilweise zwei Grössenordnungen bewirkt. Mit Hilfe des in dieser Arbeit vorgestellten Prototypen können potentiell Modelle mit Milliarden von Zuständen verifiziert werden. Bisher war die praktikable Grenze im Bereich von einigen 10 Millionen Zuständen, abhängig vom Model. Desweiteren haben wir eine Integration von Beweisinformationen ausgenutzt um die Kosten für die Berechnung einzelner Zustände zu reduzieren. Mit Hilfe dieser Methode konnten wir bei einem Teil der Beispiele eine Reduktion auf die halbe Laufzeit erreichen. Ausserdem haben wir eine Methode entwickelt, die zur Extraktion von Programmfluss-Informationen aus Event-B Modellen dienen kann. Diese Methode kann sowohl zur Reduktion des Speicherverbrauchs und der Laufzeit als auch zum Verständnis der algorithmischen Struktur des Modells beitragen. Ausserdem können mit Hilfe der Analyse die Abwesenheit von Deadlocks und andere Aussagen über die Lebendigkeit eines Systems bewiesen werden. Die Evaluierung der in dieser Arbeit entwickelten Implementierungen erfolgte mit Hilfe verschiedener akademischer und industrieller Beispiele. This is the age of software. Almost every modern electronic device has some parts implemented in software. Compared to hardware solutions, software is much cheaper and more flexible. But there is a downside to this: Software errors can kill. A concurrency bug in the software of the THERAC-25 system for radiation therapy killed at least three people. Others were seriously injured. These safety critical systems require a different approach than ordinary business applications. Testing, which is the dominant method in quality management is not sufficient. Development of safety critical systems requires formal methods, i.e., a more rigorous mathematical approach. This thesis deals with the verification of B and Event-B models using the ProB model checker. The goal was to significantly improve the performance exploiting the high abstraction level of B. We achieved this goal. Using the results of this thesis it is possible to verify models that could not previously be checked within reasonable time constraints. In particular the distributed version of ProB improved the model checking run time by orders of magnitude. Using the prototype developed in this thesis, we think it is possible to check state spaces with billions of states. Previously it was not possible to check more than a couple of 10 million states, depending on the model. We also integrated proof information into the model checking process to reduce the costs of checking each individual state. Using our improvement, we could halve the run time for some of the benchmarks. Finally, we developed a method to extract flow information from Event-B models. The results can be used to reduce the memory footprint as well as the run time of model checking. It can also be used to gain better understanding of the algorithmic structure of a model and for proving deadlock freedom and some other liveness properties. We evaluated the implementations using several models from academia and industry.
Lizenz:	Urheberrechtsschutz
Fachbereich / Einrichtung:	Mathematisch- Naturwissenschaftliche Fakultät » WE Informatik » Softwaretechnik und Programmiersprachen
Dokument erstellt am:	18.06.2015
Dateien geändert am:	18.06.2015
Promotionsantrag am:	09.12.2014
Datum der Promotion:	23.01.2015