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

(2010). AsmetaSMV: A Way to Link High-Level ASM Models to Low-Level NuSMV Specifications [conference presentation - intervento a convegno]. Retrieved from http://hdl.handle.net/10446/25159

AsmetaSMV: A Way to Link High-Level ASM Models to Low-Level NuSMV Specifications

GARGANTINI, Angelo Michele;ARCAINI, Paolo
2010-01-01

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
WOS:000279356900005
2-s2.0-77950790766
2010
Inglese
[Proceedings of the] 2nd International Conference on Abstract State Machines, Alloy, B and Z, ABZ 2010; Orford, QC; Canada; 22 February 2010 through 25 February 2010
Marc Frappier, Uwe Glässer, Sarfraz Khurshid, Régine Laleau and Steve Reeves
978-3-642-11810-4
LECTURE NOTES IN COMPUTER SCIENCE
5977
61
74
cartaceo
online
Springer
2nd International Conference on Abstract State Machines, Alloy, B and Z, ABZ 2010
2nd
Orford (QC), Canada
22 February 2010 through 25 February 2010
Settore ING-INF/05 - Sistemi di Elaborazione delle Informazioni
Abstract state machines; ASMETA; Model checking; NuSMV
Compare in: Lecture Notes in Computer Science Volume 5977, 2010, DOI: 10.1007/978-3-642-11811-1 Abstract State Machines, Alloy, B and Z Second International Conference, ABZ 2010, Orford, QC, Canada, February 22-25, 2010. Proceedings Editors: Marc Frappier, Uwe Glässer, Sarfraz Khurshid, Régine Laleau and Steve Reeves
info:eu-repo/semantics/conferenceObject
3
Gargantini, Angelo Michele; Riccobene, Elvinia; Arcaini, Paolo
1.4 Contributi in atti di convegno - Contributions in conference proceedings::1.4.01 Contributi in atti di convegno - Conference presentations
none
no full text
273
(2010). AsmetaSMV: A Way to Link High-Level ASM Models to Low-Level NuSMV Specifications [conference presentation - intervento a convegno]. Retrieved from http://hdl.handle.net/10446/25159
File allegato/i alla scheda:
Non ci sono file allegati a questa scheda.
Pubblicazioni consigliate

Aisberg ©2008 Servizi bibliotecari, Università degli studi di Bergamo | Terms of use/Condizioni di utilizzo

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/10446/25159
Citazioni
  • Scopus 61
  • ???jsp.display-item.citation.isi??? 51
social impact