Advertisement
Published in:
2010 | OriginalPaper | Chapter
AsmetaSMV: A Way to Link High-Level ASM Models to Low-Level NuSMV Specifications
Authors : Paolo Arcaini, Angelo Gargantini, Elvinia Riccobene
Published in: Abstract State Machines, Alloy, B and Z
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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.