Please use this identifier to cite or link to this item:
http://dx.doi.org/10.14279/depositonce-423
For citation please use:
For citation please use:
Main Title: | Model Checking Abstract State Machines |
Translated Title: | Modelchecken von Abstract State Machines |
Author(s): | Winter, Kirsten |
Advisor(s): | Jaehnichen, Stefan |
Granting Institution: | Technische Universität Berlin, Fakultät IV - Elektrotechnik und Informatik |
Type: | Doctoral Thesis |
URI: | urn:nbn:de:kobv:83-opus-3255 http://depositonce.tu-berlin.de/handle/11303/720 http://dx.doi.org/10.14279/depositonce-423 |
License: | http://rightsstatements.org/vocab/InC/1.0/ |
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. |
Subject(s): | Abstract State Machines Analysewerkzeuge Formale Methoden Modelchecking Multiway Decision Graphs SMV Abstract State Machines Formal Methods Model Checking Multiway Decision Graphs SMV Verification Tools |
Issue Date: | 5-Nov-2001 |
Date Available: | 5-Nov-2001 |
Exam Date: | 17-Jul-2001 |
Language: | English |
Language Code: | en |
DDC Class: | 004 Datenverarbeitung; Informatik |
TU Affiliation(s): | Fak. 4 Elektrotechnik und Informatik |
Appears in Collections: | Technische Universität Berlin » Publications |
Files in This Item:
Items in DepositOnce are protected by copyright, with all rights reserved, unless otherwise indicated.