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|
RICCOBENE, ELVINIA MARIA (Co-primo) [Methodology] (Corresponding)
|Settore Scientifico Disciplinare:||Settore INF/01 - Informatica|
|Data di pubblicazione:||2018|
|Digital Object Identifier (DOI):||10.4204/EPTCS.284.3|
|Appare nelle tipologie:||01 - Articolo su periodico|