Efficient Analysis of DynAlloy Specifications Journal Articles

abstract

• 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.

authors

• Frias, Marcelo F
• Pombo, Carlos Gustavo Lopez
• Galeotti, Juan P
• Aguirre, Nazareno M

status

• published 

publication date

• December 2007

has subject area

• 0803 Computer Software (FoR)
• 0806 Information Systems (FoR)
• Software Engineering (Science Metrix)

published in

• ACM Transactions on Software Engineering and Methodology  Journal

keywords

• ALLOY
• Computer Science
• Computer Science, Software Engineering
• Science & Technology
• Technology
• alloy
• design
• dynamic logic
• languages
• software specification
• software validation
• verification

Digital Object Identifier (DOI)

• 10.1145/1314493.1314497

start page

• 1

end page

• 34

volume

• 17

issue

• 1