Abstract
This paper presents AsmetaSMV, a model checker for Abstract State Machines (ASMs). It has been developed with the aim of enriching
the ASMETA (ASM mETAmodeling) toolset, a set of tools for ASMs, with the capabilities of the model checker NuSMV to verify
properties of ASM models written in the AsmetaL language. We describe the general architecture of AsmetaSMV and the process
of automatically mapping ASM models into NuSMV programs. As a proof of concepts, we report the results of using AsmetaSMV
to verify temporal properties of various case studies of different characteristics and complexity.
[read the copyright and download the pdf file] [DOI]