Loading...
DynAlloy analyzer: a tool for the specification and analysis of Alloy models with dynamic behaviour
Regis, Germán Cornejo, César Gutiérrez Brida, Simón Politano, Mariano Raverta, Fernando Ponzio, Pablo Aguirre, Nazareno Galeotti, Juan Pablo Frías, Marcelo
Regis, Germán
Cornejo, César
Gutiérrez Brida, Simón
Politano, Mariano
Raverta, Fernando
Ponzio, Pablo
Aguirre, Nazareno
Galeotti, Juan Pablo
Frías, Marcelo
Type
Ponencia en congreso
Citations
Altmetric:
Abstract
"We describe DynAlloy Analyzer, a tool that extends Alloy Analyzer with support for dynamic elements in Alloy models. The tool builds upon Alloy Analyzer in a way that makes it fully compatible with Alloy models, and extends their syntax with a particular idiom, inspired in dynamic logic, for the description of dynamic behaviours, understood as sequences of states over standard Alloy models, in terms of programs. The syntax is broad enough to accommodate abstract dynamic behaviours, e.g., using nondeterministic choice and finite unbounded iteration, as well as more concrete ones, using standard sequential programming constructions. The analysis of DynAlloy models resorts to the analysis of Alloy models, through an optimized translation that often makes the analysis more efficient than that of typical ad-hoc constructions to capture dynamism in Alloy."
Description
Date
2017-09
Journal Title
Journal ISSN
Volume Title
Publisher
Collections
Files
Loading...
Ponencia_Regis
Adobe PDF, 555.99 KB
Research Projects
Organizational Units
Journal Issue
Keywords
ALLOY, VALIDACION DE SOFTWARE, RESPUESTA DINAMICA, LENGUAJES DE ESPECIFICACION, VERIFICACION DE SOFTWARE