Fraunhofer-Gesellschaft

Publica

Hier finden Sie wissenschaftliche Publikationen aus den Fraunhofer-Instituten.

Model checking ASM: the MDG approach

 
: Winter, K.

:
urn:nbn:de:0011-b-731755 (1012 KByte PDF)
MD5 Fingerprint: f27d8073128bde3d35400f13caf9d532
Created on: 31.07.2002


Sankt Augustin: GMD Forschungszentrum Informationstechnik, 2001, 25 pp.
GMD Report, 125
English
Study, Electronic Publication
Fraunhofer FIRST ()
ASM; MDC; Verifikation; Werkzeugunterstützung; model checking; verification; tool support

Abstract
Abstract State Machines (ASM) ist eine mächtige Sprache zum Modellieren und Analysieren einer Vielzahl von Systemen, worunter Software sowie Hardware Systeme zu verstehen sind. Das Ziel dieser Arbeit ist, den ASM Ansatz mit computerbasierten Werkzeugen zu unterstützen. Als Kern dieser Werkzeugunterstützung wird die ASM Workbench verwendet. Ausgehend von diesem Framework für ASM ist eine Schnittstelle zu dem MDG Paket entwickelt worden, die hier vorgestellt wird. Das MDG Paket bietet eine Sammlung von elementaren Funktionen auf der Grundlage von "Multiway Decision Graphs" (MDGs) an, die genügen, um Model Checking Algorithmen für ASM zu entwickeln. Die Erfordernisse, die ein solcher neu entwickelter ASM Model Checker erfüllen sollte, sind anhand von früheren Erfahrungen im Bereich Model Checking für ASM ermittelt worden. Eine genauere Untersuchung beider Sprachmittel, ASM und MDGs, zeigt, daß MDGs ein geeignetes Mittel zur effizienten Darstellung und Analyse von ASM sind.

 

Abstract State Machines (ASM) is a powerful means for modelling and analysing various kinds of system, software as well as hardware systems. Our aim is to support the ASM method with tools for analysis. For this concern we use the ASM Workbench as a core tool. In this work we introduce an interface from the ASM Workbench to the MDG package. This package provides basic functionality and algorithms for Multiway Decision Diagrams (MDG) that are sufficient to develop a model checker for our needs. These needs are determined by our experience in model checking ASM on various examples so far. Our claim is that the use of MDG is very well suited for model checking ASM.

: http://publica.fraunhofer.de/documents/B-73175.html