Winter, K.K.Winter2022-03-032022-03-031997https://publica.fraunhofer.de/handle/publica/19188110.3217/jucs-003-05-0689In 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.enformal methodabstract state machinemodel checkingtool supportrequirement specificationverification004006400journal article