Go home now Header Background Image
Submission Procedure
share: |
Follow us
Volume 3 / Issue 5

available in:   PDF (241 kB) PS (71 kB)
Similar Docs BibTeX   Write a comment
Links into Future
DOI:   10.3217/jucs-003-05-0689


Model Checking for Abstract State Machines

Kirsten Winter (GMD FIRST, Rudower Chaussee 5, Germany)

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