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.
Titolo: | AsmetaF: A flattener for the ASMETA framework |
Autori: | |
Parole Chiave: | Software |
Settore Scientifico Disciplinare: | Settore INF/01 - Informatica |
Data di pubblicazione: | 2018 |
Rivista: | |
Tipologia: | Article (author) |
Digital Object Identifier (DOI): | 10.4204/EPTCS.284.3 |
Appare nelle tipologie: | 01 - Articolo su periodico |
File in questo prodotto:
File | Descrizione | Tipologia | Licenza | |
---|---|---|---|---|
flattenerFIDE2018_cameraReady.pdf | Pre-print (manoscritto inviato all'editore) | Open Access Visualizza/Apri |