Dokument: Towards Infinite-State Symbolic Model Checking for B and Event-B

Titel:	Towards Infinite-State Symbolic Model Checking for B and Event-B
URL für Lesezeichen:	https://docserv.uni-duesseldorf.de/servlets/DocumentServlet?id=43261
URN (NBN):	urn:nbn:de:hbz:061-20170831-103844-3
Kollektion:	Dissertationen
Sprache:	Englisch
Dokumententyp:	Wissenschaftliche Abschlussarbeiten » Dissertation
Medientyp:	Text
Autor:	Krings, Sebastian [Autor] [im Online-Personal- und -Vorlesungsverzeichnis LSF anzeigen]
Dateien:	[Dateien anzeigen] Adobe PDF [Details] 16,60 MB in einer Datei [ZIP-Datei erzeugen] Dateien vom 28.08.2017 / geändert 28.08.2017
Beitragende:	Prof. Dr. Leuschel, Michael [Betreuer/Doktorvater] Dr. Merz, Stephan [Gutachter]
Dewey Dezimal-Klassifikation:	000 Informatik, Informationswissenschaft, allgemeine Werke » 004 Datenverarbeitung; Informatik
Beschreibungen:	The idea of verifying the correctness of software has been brought up in the early days of computing, for example by Alan Turing in 1949 or Robert W. Floyd in 1967. James C. King extended upon the idea of manual verification by suggesting and working towards an implementation of a ”verifying compiler“. King’s idea has later been stated as a ”Grand Challenge for Computing Research“ by Tony Hoare in 2005. Idealism however is not the only reason for software verification. According to a study performed in 2002 by the U.S. National Institute of Standards & Technology, the U.S. economy suffers a loss of close to $60 billion per year due to software errors. Furthermore, errors have directly led to deaths or serious injuries, as well as failure or loss of equipment. Within typical software engineering approaches, testing and static analysis tools are used to limit the possibility of software errors. Several holistic approaches to software development have been designed in order to keep bug counts low throughout the whole development cycle. This thesis focuses on a more rigorous approach to the development of software: the usage of formal methods. In particular, it is concerned with improving the ProB model checker by augmenting its original explicit state model checker with a symbolic counterpart. In this way we broaden the scope of problems to which ProB can be applied. As symbolic model checking makes heavy use of constraint solving, one aspect of this thesis is to implement methods to increase the performance of ProB’s constraint solving kernel. This will be achieved by two means. First, by improving the constraint solver itself, mainly by lifting it from finite to infinite-state problems. Second, we developed an integration of ProB with the SMT solvers CVC4 and Z3, combining them into a single procedure. Following, this thesis will present different symbolic model checking algorithms and evaluate them regarding their applicability to B and Event-B. Some suitable algorithms, namely Bounded Model Checking, k-Induction and IC3 were implemented inside ProB. Both the improved constraint solver alone and the symbolic model checking algorithms will be evaluated on different examples ranging from solving B predicates, proving, disproving and SMT solving to model checking of academic and industrial specifications. Die Idee die Korrektheit von Software zu beweisen kam bereits zu Beginn des Computerzeitalters auf. Sie findet sich beispielsweise 1949 bei Alan Turing oder 1967 bei Robert W. Floyd. James C. King erweiterte die Idee durch seinen Vorschlag statt manueller Verifikation einen so genannten ”verifying compiler“, also eine automatische Software, zur Verifikation zu verwenden. Seine Idee der automatischen Verifikation wurde 2005 von Tony Hoare in seine Liste der ”Grand Challenges for Computing Research“ aufgenommen. Idealismus ist aber nicht der einzige Grund für die Verifikation von Software. Laut einer Studie die 2002 vom U.S. National Institute of Standards & Technology durchgeführt wurde erleidet allein die Wirtschaft der USA einen Verlust von fast 60 Milliarden Dollar pro Jahr auf Grund von Softwarefehlern. Softwarefehler haben bereits zu Todesfällen oder Verletzungen geführt, zu Versagen oder Verlust von Equipment beigetragen oder diese direkt verursacht. Häufig werden Tests oder statische Analysen verwendet um Fehler zu entdecken oder ihr Auftreten unwahrscheinlich zu machen. Ausserdem werden Entwicklungsmodelle verwendet, die die Anzahl von Softwarefehlern gering halten sollen. In dieser Arbeit geht es um einen strikteren Ansatz zur Entwicklung von korrekter Software: Formale Methoden. Insbesondere beschäftigt sich diese Arbeit mit der Verbesserung des Model-Checkers ProB. Ein Ziel ist es, den bestehenden Model-Checking-Algorithmus durch einen symbolischen Algorithmus zu ergänzen. So kann ProB auf eine größere Klasse von Problemen angewendet werden. Da die Effizienz von symbolischen Model-Checking-Algorithmen direkt von der Effizienz des verwendeten Solvers abhängt ist die Verbesserung des Kernels von ProB ein weiterer wichtiger Aspekt dieser Arbeit. Hier wurden zwei wesentliche Dinge umgesetzt. Zum einen wurde ProB’s interner Constraint Solver erweitert, so dass er mit Problemen auf unbegrenzten Mengen umgehen kann. Weiterhin wurde eine Integration zwischen ProB und SMT Solvern entwickelt. Anschließend werden verschiedene symbolische Model-Checking-Algorithmen vorgestellt und dann auf ihre Anwendbarkeit auf B und Event-B hin untersucht. Mehrere geeignete Algorithmen, wie Bounded Model Checking, k-Induction und IC3 wurden in ProB implementiert. Sowohl der Kernel als auch der symbolische Model-Checker werden auf verschiedene Arten evaluiert. Dazu gehört das Auswerten von Prädikaten, das Finden von Gegenbeispielen und das Beweisen von Theoremen. Darüber hinaus wird ProB auf SMT Probleme angewendet. Zuletzt wird die Performance der Model- Checking-Algorithmen auf Basis verschiedener akademischer und industrieller Beispiele ausgewertet.
Lizenz:	Urheberrechtsschutz
Fachbereich / Einrichtung:	Mathematisch- Naturwissenschaftliche Fakultät » WE Informatik » Softwaretechnik und Programmiersprachen
Dokument erstellt am:	31.08.2017
Dateien geändert am:	31.08.2017
Promotionsantrag am:	07.04.2017
Datum der Promotion:	29.07.2017