Asmeta Model checker

The AsmetaSMV model checker can be used to automatically verify Asmeta properties by translating AsmetaL specifications in NuSMV specifications.

Installation

The model checker can be used either embedded in eclipse or as standalone program. For the eclipse version, follow the instructions here

Use in eclipse

You can run the tool in two modes:

  • translates the AsmetaL model in NuSMV
  • translates the AsmetaL model in NuSMV and then executes the NuSMV model

Other options can be set in the preferences: Window -> Preferences -> Asmeta -> AsmetaSMV

Download as standalone

Download the tool: AsmetaSMV.jar

How to run

To run AsmetaSMV

java -jar AsmetaSMV.jar [options...] file.asm
 -debug   : set log4j level to debug
 -en      : execute the NuSMV model after the mapping
 -kf      : keep the NuSMV file. To be used with the -en option enabled. If the -en option is not enabled, the option -kf is enabled by default.
 -log VAL : log4j configuration file
 -nc      : do not add the check on integer enum
 -ns      : do not simplify the boolean conditions in NuSMV code

Paper

P. Arcaini, A. Gargantini, E. Riccobene. AsmetaSMV: A Way to Link High-Level ASM Models to Low-Level NuSMV Specifications, in 2nd International Conference on Abstract State Machines, Alloy, B and Z (ABZ 2010), Orford, QC, Canada, February 22-25, 2010 doi