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.
AsmetaF: A flattener for the ASMETA framework / P. Arcaini, R. Melioli, E. Riccobene. - In: ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE. - ISSN 2075-2180. - 284(2018), pp. 26-36. ((Intervento presentato al 4. convegno Workshop on Formal Integrated Development Environment, F-IDE tenutosi a Oxford nel 2018.
AsmetaF: A flattener for the ASMETA framework
P. Arcaini;E. Riccobene
Co-primo
Methodology
2018
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.File | Dimensione | Formato | |
---|---|---|---|
flattenerFIDE2018_cameraReady.pdf
accesso aperto
Tipologia:
Pre-print (manoscritto inviato all'editore)
Dimensione
240.05 kB
Formato
Adobe PDF
|
240.05 kB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.