INVESTIGADORES
LOPEZ POMBO Carlos Gustavo
artículos
Título:
Efficient Analysis of DynAlloy Specifications
Autor/es:
FRIAS, MARCELO FABIÁN; LOPEZ POMBO, CARLOS GUSTAVO; GALEOTTI, JUAN PABLO; AGUIRRE, NAZARENO M.
Revista:
ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY
Editorial:
ACM Press
Referencias:
Lugar: New York; Año: 2006 vol. 17 p. 1 - 34
ISSN:
1049-331X
Resumen:
DynAlloy is an extension of Alloy to support the definition of actions and the specification of assertions regarding execution traces. In this paper we show how we can extend the Alloy tool so that DynAlloy specifications can be automatically analyzed in an efficient way. We also demonstrate that DynAlloy´s semantics allows for a sound technique that we call program atomization, which improves the analyzability of properties regarding execution traces by considering certain programs as atomic steps in a trace. We present the foundations, case studies, and empirical results evidencing that the analysis of DynAlloy specifications can be performed efficiently.
