Giuseppe Del Castillo, Kirsten Winter:
Model Checking Support for the ASM High-Level Language.
Abstract
Gurevich's Abstract State Machines (ASM) constitute a high-level specification language for a wide range of applications. The existing tool support for ASM---currently including type-checking, simulation and debugging---should be extended to support computer-aided verification, in particular by model checking. In this paper we introduce an interface from our existing tool environment to the model checker SMV, based on a transformation which maps a large subset of ASM into the SMV language. Through a case study we show how the proposed approach can ease the validation process.
compressed postscript
