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. Copyright 2005 ACM.
Registro:
| Documento: |
Conferencia
|
| Título: | DynAlloy: Upgrading alloy with actions |
| Autor: | Frias, M.F.; Galeotti, J.P.; Pombo, C.G.L.; Aguirre, N.M. |
| Ciudad: | St. Louis, MO |
| Filiación: | Department of Computer Science, FCEyN, Universidad de Buenos Aires, Argentina
Department of Computer Science, FCEFQyN-Universidad Nacional de Río Cuarto, Argentina
CONICET, Argentina
|
| Palabras clave: | Alloy; Dynamic logic; Software specification; Software validation; Alloy; Dynamic logic; Software specification; Software validation; DynAlloy; Software specifications; Computational complexity; Computer programming languages; Formal logic; Standards; Automation; Dynamic programming; Semantics; Syntactics; Software engineering; Computer hardware description languages |
| Año: | 2005
|
| Página de inicio: | 442
|
| Página de fin: | 450
|
| Título revista: | 27th International Conference on Software Engineering, ICSE05
|
| Título revista abreviado: | Proc. Int. Conf. Softw. Eng.
|
| Registro: | https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_NIS03850_v_n_p442_Frias |
Referencias:
- Dijkstra, E.W., Scholten, C.S., (1990) Predicate Calculus and Program Semantics, , Springer-Verlag
- Goldberg, E., Novikov, Y., BerkMin: A fast and robust sat-solver (2002) Proceedings of the Conference on Design, Automation and Test in Europe, pp. 142-149. , IEEE Computer Society
- Harel, D., Kozen, D., Tiuryn, J., (2000) Dynamic Logic, , Foundations of Computing. MIT Press
- Jackson, D., Alloy: A lightweight object modelling notation (2002) ACM Transactions on Software Engineering and Methodology
- Jackson, D., (2002) A Micromodels of Software: Lightweight Modelling and Analysis with Alloy, , MIT Laboratory for Computer Science, Cambridge, MA
- Jackson, D., Shlyakhter, I., Sridharan, M., A micromodularity mechanism (2001) Proceedings of the 8th European Software Engineering Conference Held Together with the 9th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 62-73. , Vienna, Austria, Association for the Computer Machinery, ACM Press
- Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S., Chaff: Engineering an efficient SAT solver (2001) Proceedings of the 88th Conference on Design Automation, pp. 530-535. , J. Rabaey, editor, Las Vegas, Nevada, United States, ACM Press
- Spivey, J.M., (1988) Understanding Z: A Specification Language and Its Formal Semantics, , Cambridge University PressA4 - ACM SIGSOFT; IEEE Computer Society
Citas:
---------- APA ----------
Frias, M.F., Galeotti, J.P., Pombo, C.G.L. & Aguirre, N.M.
(2005)
. DynAlloy: Upgrading alloy with actions. 27th International Conference on Software Engineering, ICSE05, 442-450.
Recuperado de https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_NIS03850_v_n_p442_Frias [ ]
---------- CHICAGO ----------
Frias, M.F., Galeotti, J.P., Pombo, C.G.L., Aguirre, N.M.
"DynAlloy: Upgrading alloy with actions"
. 27th International Conference on Software Engineering, ICSE05
(2005) : 442-450.
Recuperado de https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_NIS03850_v_n_p442_Frias [ ]
---------- MLA ----------
Frias, M.F., Galeotti, J.P., Pombo, C.G.L., Aguirre, N.M.
"DynAlloy: Upgrading alloy with actions"
. 27th International Conference on Software Engineering, ICSE05, 2005, pp. 442-450.
Recuperado de https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_NIS03850_v_n_p442_Frias [ ]
---------- VANCOUVER ----------
Frias, M.F., Galeotti, J.P., Pombo, C.G.L., Aguirre, N.M. DynAlloy: Upgrading alloy with actions. Proc. Int. Conf. Softw. Eng. 2005:442-450.
Available from: https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_NIS03850_v_n_p442_Frias [ ]
