Efficient Analysis of DynAlloy Specifications

DynAlloy is an extension of Alloy to support the definition of actions and the specification of assertions regarding execution traces. In this article 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 indicating that the analysis of DynAlloy specifications can be performed efficiently.