Model Checking for Abstract State Machines
Kirsten Winter · Zenodo (CERN European Organization for Nuclear Research) · 2020
Abstract: In this paper, we discuss the use of a model checker in combination with the speci cation 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 o ers e ective support for verifying ASM speci cations.