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.
AsmetaSMV : a way to link high-level ASM models to low-level nuSMV specifications / P. Arcaini, A. Gargantini, E. Riccobene - In: Abstract state machines, Alloy, B and Z : second international conference, ABZ 2010 : Orford, QC, Canada, february 22-25, 2010 : proceedings / [a cura di] M. Frappier, U. Glässer, S. Khurshid, R. Laleau, S. Reeves. - Berlin : Springer, 2010. - ISBN 9783642118104. - pp. 61-74 (( Intervento presentato al 2. convegno ABZ international conference tenutosi a Orford, Canada nel 2010 [10.1007/978-3-642-11811-1_6].
AsmetaSMV : a way to link high-level ASM models to low-level nuSMV specifications
P. ArcainiPrimo
;E. RiccobeneUltimo
2010
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.
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
