Dokument: Improving Explicit-State Model Checking for B and Event-B

Titel:	Improving Explicit-State Model Checking for B and Event-B
URL für Lesezeichen:	https://docserv.uni-duesseldorf.de/servlets/DocumentServlet?id=45594
URN (NBN):	urn:nbn:de:hbz:061-20180417-080739-0
Kollektion:	Dissertationen
Sprache:	Englisch
Dokumententyp:	Wissenschaftliche Abschlussarbeiten » Dissertation
Medientyp:	Text
Autor:	Dobrikov, Ivaylo Miroslavov [Autor]
Dateien:	[Dateien anzeigen] Adobe PDF [Details] 927 KB in einer Datei [ZIP-Datei erzeugen] Dateien vom 10.04.2018 / geändert 10.04.2018
Beitragende:	Prof. Dr. Leuschel, Michael [Gutachter] Dr. Williams, David [Gutachter]
Stichwörter:	formal verification, temporal logic, model checking, state-space explosion problem, partial order reduction, ample set approach, static analysis, ProB, high-level formalisms, concurrent systems, Event-B, classical B
Dewey Dezimal-Klassifikation:	000 Informatik, Informationswissenschaft, allgemeine Werke » 004 Datenverarbeitung; Informatik
Beschreibungen:	Explizite Modellprüfung ist ein Verifikationsverfahren zur automatischen Prüfung von Eigenschaften von formalen Modellen, das auf die explizite Konstruktion des Zustandsraums des Modells baut. Die Effektivität der Modellprüfung ist zumeist eng mit der Größe des Zustandsraums des zu prüfenden Modells verknüpft. In den meisten Fällen wächst die Anzahl der Zustände eines Modells exponentiell mit der Anzahl der Variablen im Modell. Eine solche Explosion der Anzahl der Zustände im Modell ist oft die Ursache dafür, dass die Verifikation von Modellen via explizite Modellprüfung sehr oft als nicht praktikabel bewertet wird. Die Verifikation von formalen Modellen via explizite Modellprüfung kann noch problematischer werden, wenn die Modelle nebenläufige Systeme beschreiben. Auch in diesem Fall wächst die Anzahl der Zustände der formalen Modelle, die solche Systeme beschreiben, in der Regel exponentiell mit der Anzahl der parallel ausgeführten Komponenten im System. Dieses Problem ist auch unter dem Namen Zustandsexplosionsproblem bekannt. Diese Arbeit präsentiert zwei Methoden für die Bekämpfung des Zustandsexplosionsproblems, das im Kontext von automatischer Verifikation von klassischen B und Event-B Modellen behandelt wird. Das erste Verfahren nutzt Informationen über die Art und Weise wie Operationen in einer Maschine sich gegenseitig beeinflussen können. Durch das Nutzen solcher Informationen kann man voraussagen, welche Operationen in einem Zustand aktiviert oder deaktiviert sind und somit die Evaluierung der Guards dieser Operationen im Zustand vermeiden. Dadurch können überflüssige Berechnungen gespart und die Kosten für die Zustandsexploration eines klassischen B oder Event-B Modells gesenkt werden. Die neue Technik kann den Prozess der Verifikation von zustandsintensiven Modellen signifikant beschleunigen, durch Vermeidung der Evaluierung eines beträchtlichen Teils der Guard-Tests, die gebraucht werden, um den Zustandsraum einer Maschine durch klassische Explorationstechniken zu untersuchen. Dadurch können in manchen Fällen die Laufzeiten der Modellprüfung von B Spezifikationen bis zum 3-fachen beschleunigt werden. Das zweite Verfahren präsentiert eine Methode von Partial Order Reduction, eine Technik, die durch Zustandsreduktion eine Lösung des Zustandsexplosionsproblems anbietet. Die Methode nutzt die Kommutativität unabhängiger Zustandsübergänge, um redundante Pfade im Zustandsraum zu kürzen. Die Reduktionsalgorithmen, die in dieser Arbeit entwickelt wurden, präsentieren den ersten erfolgreichen Versuch für die Anwendung von Partial Order Reduction für beide Formalismen B und Event-B. Die Evaluierung der Reduktionsalgorithmen hat gezeigt, dass die Reduktionstechnik für die Modellprüfung von klassischen B und Event-B Modellen, die einen hohen Grad von Unabhängigkeit und Nebenläufigkeit aufweisen, enorm effektiv ist. Darüber hinaus wurde beobachtet, dass die Reduktionsalgorithmen eine sehr gute Reduktion des Zustandsraums von klassischen B und Event-B Modellen von reaktiven Systemen erzielen konnten. Beide Verfahren nutzen die Informationen von zwei statischen Analysen, die Enabling- und die Unabhängigkeitsanalyse, um die Modellprüfung von B Spezifikationen zu optimieren. Diese zwei Analysen nutzen syntaktische und Constraintsolving-Techniken um das gegenseitige Beeinflussen von Operationen in einer klassischen B und Event-B Maschine zu entschlüsseln. Die Nutzung der Constraintsolving-Techniken ist von großem Vorteil für die Optimierungsverfahren, da die präzisere Berechnung der Enabling- und Unabhängigkeitsrelationen von Operationen oft die Effektivität der Optimierungsalgorithmen erhöht. Diese Arbeit beschreibt die Grundlagen der beiden Analysen und zeigt, dass die Ergebnisse beider Analysen nicht nur für die Optimierung der Modellprüfung von B Systemen enorm nützlich sein können, sondern auch für das Verständnis des Kontrollflusses von klassischen B und Event-B Modellen. Die statischen Analysen und alle Optimierungsalgorithmen, die in dieser Arbeit präsentiert werden, wurden in das ProB-Toolset integriert. Alle Implementierungen wurden an einer großen Anzahl von klassischen B und Event-B Modellen evaluiert und ausgiebig diskutiert. Anschließend werden die Reduktionsergebnisse der Reduktionsalgorithmen im ProB mit den Reduktionsergebnissen des Reduktionsalgorithmus im LTSmin-Tool verglichen und analysiert. Explicit-state model checking is a verification method for checking automatically properties on formal models relying on the explicit construction of the model’s state space. The effectivity of such techniques depends mostly on the complexity and the size of the system being verified. In most of the time, the number of states of a formal model grows exponentially in the number of variables in the model. Such an explosion of the state space is often the cause for very large runtimes of verification techniques based on the explicit exploration of the state space. The verification of systems using explicit-state exploration can get even more problematic when the system under consideration has many components, which are executed concurrently. Also in this case the state space size of a model representing such a system usually grows exponentially in the number of concurrent components in the system. This problem is also known as the state space explosion problem. This thesis develops two optimisation approaches for combatting the state space explosion problem in the context of automatic verification of classical B and Event-B models. The first optimisation approach reduces the costs of exploring explicitly the state space of classical B and Event-B machines by using the information about how transitions in a machine influence each other. Using such a type of information one can predict the enabling status of transitions in a state, aiming in this way to avoid the guard evaluation of these transitions in the state. The approach, which develops a new state space exploration technique, speeds up significantly the process of verification for large state models by avoiding a chief part of the guard tests needed to explore the state space of models by classical methods. The evaluation of the technique has shown that for some examples the new state space exploration method can reduce the model checking runtimes by a factor of three. The second approach developed in this work represents a method of partial order reduction, a technique for combatting the state space explosion problem by reducing the size of the system’s state space. The method makes use of the commutativity of independent transitions to prune redundant paths in the state space. The reduction algorithms developed in this work represent the first successful attempt to apply partial order reduction for both formalisms classical B and Event-B. The reduction algorithms are vastly effective for model checking classical B and Event-B models with loosely coupled events, significantly reducing the size of the state space to be searched and consequently the runtimes for checking such models. The evaluation of the reduction algorithms showed that significant reductions could often be obtained by model checking classical B and Event-B models describing concurrent and reactive systems. Both optimisation approaches use the information provided by two static analyses, called enabling and independence analysis, to optimise model checking of classical B and Event- B specifications. Both analyses use syntactic and constraint-solving techniques to decode the mutual influence of transitions in classical B and Event-B machines. The use of the constraint-solving techniques for computing the enabling and independence relations can increase significantly the effectivity of the optimisation techniques in this work, as the accuracy of both types of relations is often decisive for the efficacy of the methods. In addition, this work describes the foundations of the enabling and independence analyses and shows that the output of the analyses is not only very valuable for improving model checking of B systems, but also very beneficial for understanding the control flow of classical B and Event-B models. The static analyses and all optimisation algorithms described in this thesis have been implemented in the ProB toolset. The implementations are discussed and evaluated on a variety of classical B and Event-B models, a large part of which represent real-world systems. Additionally, the reduction results provided by the reduction algorithms in this thesis and the reduction algorithm implemented in LTSmin are compared and thoroughly discussed.
Lizenz:	Urheberrechtsschutz
Fachbereich / Einrichtung:	Mathematisch- Naturwissenschaftliche Fakultät » WE Informatik » Softwaretechnik und Programmiersprachen
Dokument erstellt am:	17.04.2018
Dateien geändert am:	17.04.2018
Promotionsantrag am:	01.09.2017
Datum der Promotion:	15.12.2017