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
