INVESTIGADORES
FRIAS Marcelo Fabian
congresos y reuniones científicas
Título:
DynAlloy: Upgrading Alloy with Actions
Autor/es:
FRIAS, MARCELO FABIAN; GALEOTTI, JUAN PABLO; LOPEZ POMBO, CARLOS GUSTAVO; AGUIRRE, NAZARENO
Lugar:
St. Louis, Missouri, USA
Reunión:
Congreso; ICSE 2005, International Conference on Software Engineering; 2005
Institución organizadora:
ACM/IEEE
Resumen:
We present DynAlloy, an extension to the Alloy specification
language to describe dynamic properties of systems using actions.
Actions allow us to appropriately specify dynamic properties,
particularly, properties regarding execution traces, in the style of dynamic
logic specifications.
We extend Alloy's syntax with a notation for partial correctness assertions,
whose semantics relies on an adaptation of Dijkstra's weakest liberal
precondition. These assertions, defined in terms of actions, allow us to easily
express properties regarding executions, favoring the separation of concerns
between the static and dynamic aspects of a system specification.
We also extend the Alloy tool in such a way that DynAlloy specifications are
also automatically analyzable, as standard Alloy specifications. We present the
foundations, two case-studies, and empirical results evidencing that the
analysis of DynAlloy specifications can be performed efficiently.