DynAlloy: Upgrading alloy with actions
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 Al...
Guardado en:
| Autor principal: | |
|---|---|
| Otros Autores: | , , |
| Formato: | Acta de conferencia Capítulo de libro |
| Lenguaje: | Inglés |
| Publicado: |
2005
|
| Acceso en línea: | Registro en Scopus Handle Registro en la Biblioteca Digital |
| Aporte de: | Registro referencial: Solicitar el recurso aquí |
| LEADER | 04931caa a22006737a 4500 | ||
|---|---|---|---|
| 001 | PAPER-3850 | ||
| 003 | AR-BaUEN | ||
| 005 | 20230518203319.0 | ||
| 008 | 190411s2005 xx ||||fo|||| 10| 0 eng|d | ||
| 024 | 7 | |2 scopus |a 2-s2.0-33244466281 | |
| 040 | |a Scopus |b spa |c AR-BaUEN |d AR-BaUEN | ||
| 100 | 1 | |a Frias, M.F. | |
| 245 | 1 | 0 | |a DynAlloy: Upgrading alloy with actions |
| 260 | |c 2005 | ||
| 270 | 1 | 0 | |m Frias, M.F.; Department of Computer Science, FCEyN, Universidad de Buenos AiresArgentina; email: mfrias@dc.uba.ar |
| 506 | |2 openaire |e Política editorial | ||
| 504 | |a Dijkstra, E.W., Scholten, C.S., (1990) Predicate Calculus and Program Semantics, , Springer-Verlag | ||
| 504 | |a 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 | ||
| 504 | |a Harel, D., Kozen, D., Tiuryn, J., (2000) Dynamic Logic, , Foundations of Computing. MIT Press | ||
| 504 | |a Jackson, D., Alloy: A lightweight object modelling notation (2002) ACM Transactions on Software Engineering and Methodology | ||
| 504 | |a Jackson, D., (2002) A Micromodels of Software: Lightweight Modelling and Analysis with Alloy, , MIT Laboratory for Computer Science, Cambridge, MA | ||
| 504 | |a 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 | ||
| 504 | |a 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 | ||
| 504 | |a Spivey, J.M., (1988) Understanding Z: A Specification Language and Its Formal Semantics, , Cambridge University PressA4 - ACM SIGSOFT; IEEE Computer Society | ||
| 520 | 3 | |a 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. |l eng | |
| 593 | |a Department of Computer Science, FCEyN, Universidad de Buenos Aires, Argentina | ||
| 593 | |a Department of Computer Science, FCEFQyN-Universidad Nacional de Río Cuarto, Argentina | ||
| 593 | |a CONICET, Argentina | ||
| 690 | 1 | 0 | |a ALLOY |
| 690 | 1 | 0 | |a DYNAMIC LOGIC |
| 690 | 1 | 0 | |a SOFTWARE SPECIFICATION |
| 690 | 1 | 0 | |a SOFTWARE VALIDATION |
| 690 | 1 | 0 | |a ALLOY |
| 690 | 1 | 0 | |a DYNAMIC LOGIC |
| 690 | 1 | 0 | |a SOFTWARE SPECIFICATION |
| 690 | 1 | 0 | |a SOFTWARE VALIDATION |
| 690 | 1 | 0 | |a DYNALLOY |
| 690 | 1 | 0 | |a SOFTWARE SPECIFICATIONS |
| 690 | 1 | 0 | |a COMPUTATIONAL COMPLEXITY |
| 690 | 1 | 0 | |a COMPUTER PROGRAMMING LANGUAGES |
| 690 | 1 | 0 | |a FORMAL LOGIC |
| 690 | 1 | 0 | |a STANDARDS |
| 690 | 1 | 0 | |a AUTOMATION |
| 690 | 1 | 0 | |a DYNAMIC PROGRAMMING |
| 690 | 1 | 0 | |a SEMANTICS |
| 690 | 1 | 0 | |a SYNTACTICS |
| 690 | 1 | 0 | |a SOFTWARE ENGINEERING |
| 690 | 1 | 0 | |a COMPUTER HARDWARE DESCRIPTION LANGUAGES |
| 700 | 1 | |a Galeotti, J.P. | |
| 700 | 1 | |a Pombo, C.G.L. | |
| 700 | 1 | |a Aguirre, N.M. | |
| 711 | 2 | |c St. Louis, MO |d 15 May 2005 through 21 May 2005 |g Código de la conferencia: 66729 | |
| 773 | 0 | |d 2005 |h pp. 442-450 |p Proc. Int. Conf. Softw. Eng. |n Proceedings - 27th International Conference on Software Engineering, ICSE05 |t 27th International Conference on Software Engineering, ICSE05 | |
| 856 | 4 | 1 | |u https://www.scopus.com/inward/record.uri?eid=2-s2.0-33244466281&partnerID=40&md5=af5c3cebd1fb187ac59bd23298f4d424 |y Registro en Scopus |
| 856 | 4 | 0 | |u https://hdl.handle.net/20.500.12110/paper_NIS03850_v_n_p442_Frias |y Handle |
| 856 | 4 | 0 | |u https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_NIS03850_v_n_p442_Frias |y Registro en la Biblioteca Digital |
| 961 | |a paper_NIS03850_v_n_p442_Frias |b paper |c PE | ||
| 962 | |a info:eu-repo/semantics/conferenceObject |a info:ar-repo/semantics/documento de conferencia |b info:eu-repo/semantics/publishedVersion | ||
| 999 | |c 64803 | ||