AsmetaF: A Flattener for the ASMETA Framework

Paolo Arcaini
(National Institute of Informatics)
Riccardo Melioli
(Dipartimento di Informatica, Università degli Studi di Milano)
Elvinia Riccobene
(Dipartimento di Informatica, Università degli Studi di Milano)

Abstract State Machines (ASMs) have shown to be a suitable high-level specification method for complex, even industrial, systems; the ASMETA framework, supporting several validation and verification activities on ASM models, is an example of a formal integrated development environment. Although ASMs allow modeling complex systems in a rather concise way -and this is advantageous for specification purposes-, such concise notation is in general a problem for verification activities as model checking and theorem proving that rely on tools accepting simpler notations.

In this paper, we propose a flattener tool integrated in the ASMETA framework that transforms a general ASM model in a flattened model constituted only of update, parallel, and conditional rules; such model is easier to map to notations of verification tools. Experiments show the effect of applying the tool to some representative case studies of the ASMETA repository.

In Paolo Masci, Rosemary Monahan and Virgile Prevosto: Proceedings 4th Workshop on Formal Integrated Development Environment (F-IDE 2018), Oxford, England, 14 July 2018, Electronic Proceedings in Theoretical Computer Science 284, pp. 26–36.
The first two authors are supported by ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST. Funding Reference number: 10.13039/501100009024 ERATO.
Published: 27th November 2018.

ArXived at: http://dx.doi.org/10.4204/EPTCS.284.3 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org