JUCS - Journal of Universal Computer Science 3(5): 689-701, doi: 10.3217/jucs-003-05-0689
Model Checking for Abstract State Machines
expand article infoKirsten Winter‡
‡ GMD FIRST, Rudower Chaussee 5, Berlin, Germany

Corresponding author: Kirsten Winter ( kirsten@first.gmd.de )

© Kirsten Winter.
This article is freely available under the J.UCS Open Content License.
Citation: Winter K (1997) Model Checking for Abstract State Machines. JUCS - Journal of Universal Computer Science 3(5): 689-701. https://doi.org/10.3217/jucs-003-05-0689
Open Access
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.
Keywords
Formal Methods, Abstract State Machines, Model Checking, Tool Support, Requirement Specification, Verification