Model Checking Abstract State Machines

Abstract

Abstract State Machines (ASM) ist eine formale Spezifikationssprache, die es erlaubt, auf einem hohen Abstraktionsniveau zu modellieren. Sie ist gut geeignet fuer verschiedenartigste Anwendungen. Computerbasierte Werkzeugunterstuetzung ist in Form von Editoren, Typecheckern und Simulatoren vorhanden. ASM ist ausserdem in die Logiken zweier Theorembeweiser eingebettet worden, die interaktives Beweisen unterstuetzen. Diese Dissertation hat zum Ziel, die vorhandene Werkzeugunterstuetzung um einen vollstaendig automatisierten Ansatz zu erweitern, das sogenannte Modelchecking. Modelchecking ist die vollstaendige Suche im Zustandsraum des zu untersuchenden Systemmodells. Die Algorithmen arbeiten automatisch und beduerfen keiner Interaktion mit dem Benutzer oder der Benutzerin. Als zentrale Werkzeugumgebung wird die ASM Workbench verwendet, in die ein Modelchecker integriert wird. Diese Werkzeugumgebung wird mit einer allgemeinen Schnittstelle in Form einer Zwischensprache versehen. Diese allgemeine Schnittstelle dient als Grundlage zur Anbindung verschiedener Modelchecker, die auf einfachen Transitionssystemen basieren. Mit der Transformation der abstrakten Spezifikationssprache ASM in die sehr einfachen Sprachen von vollautomatischen Werkzeugen schlaegt diese Arbeit eine Bruecke ueber den tiefen Graben zwischen Modellierungssprachen, die auf hohem Niveau beschreiben, und Werkzeugsprachen, die algorithmisch einfach zu behandeln sind. Auf der Basis der allgemeinen Schnittstelle werden im Rahmen dieser Dissertation zwei konkrete Schnittstellen entwickelt: von der ASM Workbench zum Modelchecker SMV und zum MDG-Paket. Ersteres Werkzeug wird haeufig eingesetzt und implementiert symbolisches Modelchecken fuer CTL-Formeln. Die Anbindung zum Modelchecker SMV ist implementiert und zwei Fallstudien wurden mittels der entwickelten Transformation und dem SMV Werkzeug untersucht. Die Ergebnisse zeigen die Anwendbarkeit aber auch die Grenzen dieses Ansatzes auf. Diese Grenzen motivieren die Entwicklung der zweiten Schnittstelle zum MDG-Paket. Dieses Paket umfasst die Basisfunktionalitaet fuer symbolisches Modelchecking auf der Grundlage von Multiway Decision Graphs (MDGs). Diese Graphenstruktur erlaubt die Repraesentation von moeglicherweise unendlichen Transitionssystemen mit Hilfe von abstrakten Sorten und Funktionen. Sie bietet daher ein einfaches Mittel, um die Abstraktion von Modellen zu unterstuetzen.

Abstract State Machines (ASM) constitute a high-level specification language for a wide range of applications. The existing tool support for ASM includes editors, type-checkers, and simulators. Moreover, ASM are encoded into the logic of two theorem provers that provide support for mechanical interactive proofs. This thesis aims to extend this tool support by means of a fully algorithmic approach, namely model checking. We use the ASM Workbench as a core tool framework for ASM and provide a general interface into an intermediate language. This general interface can be exploited for interfacing various tools that allow the treatment of simple transition systems. With this transformation step we bridge a gap between the high-level modelling language ASM and the low-level input language of model checkers. Based on this general interface, we develop two interfaces: from the ASM Workbench to the model checker SMV and to the MDG-Package. The former is a widely used model checker that implements symbolic model checking for CTL formulas. We implement the interface and investigate two case studies by means of our transformation and the SMV tool. The results illustrate the practicability of this approach as well as its limitations. These limitations motivate the second interface to the MDG-Package. This package comprises the basic functionality for symbolic model checking based on multiway decision graphs (MDGs). This graph structure allows the representation of possibly infinite system through abstract data types and functions. Thus, it provides a simple means for supporting abstraction of complex systems. Moreover, in this framework assumptions on the system environment can be modelled as temporal logic formulas which are conjoined with the system model. This extends the limits of this fully automatic analysis provided by model checking.