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.
This work is supported in part by the PRIN project D-ASAP (Dependable Adaptable Software Architecture for Pervasive computing).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Mastercard international inc.: Mondex, http://www.mondex.com/
The NuSMV website, http://nusmv.itc.it/
The ASMETA website (2006), http://asmeta.sourceforge.net/
Arcaini, P., Gargantini, A., Riccobene, E.: AsmetaSMV: a model checker for AsmetaL models. tutorial. TR 120, DTI Dept., Univ. of Milan (2009)
Beckers, J., Klünder, D., Kowalewski, S., Schlich, B.: Direct support for model checking abstract state machines by utilizing simulation. In: Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, pp. 112–124. Springer, Heidelberg (2008)
Börger, E.: The Abstract State Machines Method for High-Level System Design and Analysis. Technical report, BCS Facs Seminar Series Book (2007)
Börger, E., Stärk, R.: Abstract State Machines: A Method for High-Level System Design and Analysis. Springer, Heidelberg (2003)
Carioni, A., Gargantini, A., Riccobene, E., Scandurra, P.: A scenario-based validation language for ASMs. In: Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, pp. 71–84. Springer, Heidelberg (2008)
Castillo, G.D., Winter, K.: Model checking support for the ASM high-level language. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 331–346. Springer, Heidelberg (2000)
Farahbod, R., Glässer, U., Ma, G.: Model checking coreasm specifications. In: Prinz, A. (ed.) Proceedings of the ASM 2007, The 14th International ASM Workshop (2007)
Gargantini, A., Riccobene, E., Rinzivillo, S.: Using Spin to generate tests from ASM specifications. In: Börger, E., Gargantini, A., Riccobene, E. (eds.) ASM 2003. LNCS, vol. 2589, pp. 263–277. Springer, Heidelberg (2003)
Gargantini, A., Riccobene, E., Scandurra, P.: A metamodel-based language and a simulation engine for abstract state machines. J. UCS 14(12), 1949–1983 (2008)
Gargantini, A., Riccobene, E., Scandurra, P.: Model-driven language engineering: The ASMETA case study. In: International Conference on Software Engineering Advances, ICSEA, pp. 373–378 (2008)
Gargantini, A., Riccobene, E., Scandurra, P.: Ten reasons to metamodel ASMs. In: Jean-Raymond, Glässer, U. (eds.) Rigorous Methods for Software Construction and Analysis. LNCS, vol. 5115, pp. 33–49. Springer, Heidelberg (2009)
Kardos, M.: An approach to model checking asml specifications. In: Abstract State Machines, pp. 289–304 (2005)
Kupferman, O., Vardi, M.: Vacuity detection in temporal model checking. International Journal on Software Tools for Technology Transfer (STTT) 4(2), 224–233 (2003)
McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Norwell (1993)
Schellhorn, G., Banach, R.: A concept-driven construction of the mondex protocol using three refinements. In: Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, pp. 57–70. Springer, Heidelberg (2008)
Spielmann, M.: Automatic verification of abstract state machines. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 431–442. Springer, Heidelberg (1999)
Winter, K.: Model Checking for Abstract State Machines. Journal of Universal Computer Science (J.UCS) 3(5), 689–701 (1997)
Winter, K.: Towards a methodology for model checking ASM: Lessons learned from the FLASH case study. In: Gurevich, Y., Kutter, P.W., Odersky, M., Thiele, L. (eds.) ASM 2000. LNCS, vol. 1912, pp. 341–360. Springer, Heidelberg (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Arcaini, P., Gargantini, A., Riccobene, E. (2010). AsmetaSMV: A Way to Link High-Level ASM Models to Low-Level NuSMV Specifications. In: Frappier, M., Glässer, U., Khurshid, S., Laleau, R., Reeves, S. (eds) Abstract State Machines, Alloy, B and Z. ABZ 2010. Lecture Notes in Computer Science, vol 5977. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11811-1_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-11811-1_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-11810-4
Online ISBN: 978-3-642-11811-1
eBook Packages: Computer ScienceComputer Science (R0)