AsmetaMA (Asmeta Model Advisor) can be used to check for common defects of AsmetaL models.

Installation

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

The NuSMV model checker must be installed in the system and added to the system path. NuSMV can be downloaded from here: http://nusmv.fbk.eu/

Use in eclipse

In order to run the model advisor you have:

• Select the desired metaproperties in Window -> Preferences -> Asmeta -> AsmetaMA
• Run the tool from the toolbar

Download as standalone

Download the tool: AsmetaMA.jar

How to run

To run AsmetaMA

java -jar AsmetaMA.jar [options...] asmetalFileName.asm
 -kf    : keep the NuSMV file.
 -mp1   : No inconsistent update is ever performed
 -mp2   : Every conditional rule must be complete
 -mp3   : Every rule can eventually fire
 -mp4   : No assignment is always trivial
 -mp5   : For every domain element e there exists a location which has value e
 -mp6   : Every controlled function can take any value in its co-domain
 -mp7   : Every controlled location is updated and every location is read
 -mpAll : Execute all the metaproperties

Paper

P. Arcaini, A. Gargantini, E. Riccobene. Automatic review of Abstract State Machines by Meta Property Verification, in 2nd NASA Formal Methods Symposium (NFM 2010) link