Fraunhofer-Gesellschaft

Publica

Hier finden Sie wissenschaftliche Publikationen aus den Fraunhofer-Instituten.

Model checking for abstract state machines

 
: Winter, K.

:

Journal of universal computer science : JUCS 3 (1997), No.5, pp.689
ISSN: 0948-695X
ISSN: 0948-6968
English
Journal Article
Fraunhofer FIRST ()
formal method; abstract state machine; model checking; tool support; requirement specification; verification

Abstract
In this paper, we discuss the use of a model checker in combination with the specification method of Abstract State Machines (ASMs). A schema is introduced for transforming ASM models into the language of a model checker. We prove that the transformation preserves the semantics of ASMs and provide a theoretical framework for a transformation tool. Experience with model-checking the ASM model of the Production Cell demonstrates that this approach offers effective support for verifying ASM specifications.

: http://publica.fraunhofer.de/documents/970687.html