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
Open Access
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.
Formal Methods, Abstract State Machines, Model Checking, Tool Support, Requirement Specification, Verification