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
Kirsten Winter
|