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

Paolo Arcaini, Angelo Gargantini, Elvinia Riccobene
Digital Printed Abstract View Cite
Type
Conference paper
Publication
2nd International Conference on ASM, Alloy, B, and Z (ABZ'10)

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.

Document

If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.

Reference

% BibTex
@inproceedings{ArcainiGR10,
  author       = {Paolo Arcaini and
                  Angelo Gargantini and
                  Elvinia Riccobene},
  editor       = {Marc Frappier and
                  Uwe Gl{\"{a}}sser and
                  Sarfraz Khurshid and
                  R{\'{e}}gine Laleau and
                  Steve Reeves},
  title        = {AsmetaSMV: {A} Way to Link High-Level {ASM} Models to Low-Level NuSMV
                  Specifications},
  booktitle    = {Abstract State Machines, Alloy, {B} and Z, Second International Conference,
                  {ABZ} 2010, Orford, QC, Canada, February 22-25, 2010. Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {5977},
  pages        = {61--74},
  publisher    = {Springer},
  year         = {2010},
  url          = {https://doi.org/10.1007/978-3-642-11811-1\_6},
  doi          = {10.1007/978-3-642-11811-1\_6},
  timestamp    = {Tue, 14 May 2019 10:00:50 +0200},
  biburl       = {https://dblp.org/rec/conf/asm/ArcainiGR10.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
ABZ'10

Related