Name
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. |
Year | DOI | Venue |
|---|---|---|
2007 | 10.1145/1314493.1314497 | ACM Trans. Softw. Eng. Methodol. |
Keywords | Field | DocType |
dynamic logic,empirical result,dynalloy specifications,efficient analysis,software validation acm reference format:,certain program,software specification,case study,additional key words and phrases: alloy,dynalloy specification,atomic step,sound technique,program atomization,execution trace,alloy tool,software validation | Programming language,Computer science,Dynamic logic (digital electronics),Software requirements specification,Software verification and validation,Semantics | Journal |
Volume | Issue | ISSN |
17 | 1 | 1049-331X |
Citations | PageRank | References |
12 | 0.59 | 10 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Marcelo F. Frias | 1 | 295 | 35.57 |
| Carlos G. Lopez Pombo | 2 | 144 | 8.51 |
| Juan P. Galeotti | 3 | 166 | 9.64 |
| Nazareno M. Aguirre | 4 | 119 | 12.03 |