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

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Frias, M.F., Galeotti, J.P., Pombo, C.G.L., Aguirre, N.M.
Formato: CONF
Materias:
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
Acceso en línea:http://hdl.handle.net/20.500.12110/paper_NIS03850_v_n_p442_Frias
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
id todo:paper_NIS03850_v_n_p442_Frias
record_format dspace
spelling todo:paper_NIS03850_v_n_p442_Frias2023-10-03T16:45:46Z DynAlloy: Upgrading alloy with actions Frias, M.F. Galeotti, J.P. Pombo, C.G.L. Aguirre, N.M. 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 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. Fil:Frias, M.F. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. Fil:Galeotti, J.P. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. Fil:Pombo, C.G.L. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. CONF info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar http://hdl.handle.net/20.500.12110/paper_NIS03850_v_n_p442_Frias
institution Universidad de Buenos Aires
institution_str I-28
repository_str R-134
collection Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
topic 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
spellingShingle 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
Frias, M.F.
Galeotti, J.P.
Pombo, C.G.L.
Aguirre, N.M.
DynAlloy: Upgrading alloy with actions
topic_facet 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
description 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.
format CONF
author Frias, M.F.
Galeotti, J.P.
Pombo, C.G.L.
Aguirre, N.M.
author_facet Frias, M.F.
Galeotti, J.P.
Pombo, C.G.L.
Aguirre, N.M.
author_sort Frias, M.F.
title DynAlloy: Upgrading alloy with actions
title_short DynAlloy: Upgrading alloy with actions
title_full DynAlloy: Upgrading alloy with actions
title_fullStr DynAlloy: Upgrading alloy with actions
title_full_unstemmed DynAlloy: Upgrading alloy with actions
title_sort dynalloy: upgrading alloy with actions
url http://hdl.handle.net/20.500.12110/paper_NIS03850_v_n_p442_Frias
work_keys_str_mv AT friasmf dynalloyupgradingalloywithactions
AT galeottijp dynalloyupgradingalloywithactions
AT pombocgl dynalloyupgradingalloywithactions
AT aguirrenm dynalloyupgradingalloywithactions
_version_ 1782024560470654976

Ejemplares similares