Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2005 | 10.1145/1062455.1062535 | ICSE |
Keywords | DocType | ISSN |
empirical result,alloy specification language,system specification,dynamic aspect,dynamic property,execution trace,dynamic logic specification,alloy tool,standard alloy specification,dynalloy specification,computer science,software engineering,formal specification,formal specifications,software design,software specification,logic design,separation of concern,specification language,software validation,dynamic logic | Conference | 0270-5257 |
ISBN | Citations | PageRank |
1-58113-963-2 | 57 | 1.97 |
References | Authors | |
5 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Marcelo F. Frias | 1 | 295 | 35.57 |
| Juan P. Galeotti | 2 | 166 | 9.64 |
| Carlos G. Lopez Pombo | 3 | 144 | 8.51 |
| Nazareno M. Aguirre | 4 | 119 | 12.03 |