Kirsten Winter:
Model Checking for Abstract State Machines.
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.
compressed postscript
