Universidad de Buenos Aires and (2009)
Marcelo F. Frias, Juan P. Galeotti, Nazareno M. Aguirre, Río Cuarto
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...
Towards Abstraction for DynAlloy Specifications (2009)
Nazareno M. Aguirre, Marcelof. Frias, Pablo Ponzio, Brian J. Cardiff, Juan P. Galeotti, Germán Regis
Abstract. DynAlloy is an extension of the Alloy language to better describe state change via actions and programs, in the style of dynamic logic. In this paper, we report on our experience in trying...
DynAlloy: Upgrading Alloy with Actions (Extended Abstract) (2009)
Marcelo F. Frias, Juan P. Galeotti, Nazareno M. Aguirre
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,...
DynAlloy: Upgrading Alloy with Actions ABSTRACT (2009)
Marcelo F. Frias, Juan P. Galeotti, Nazareno M. Aguirre
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,...
Dynamic Software Architectures Verification using DynAlloy (2009)
Antonio Bucchiarone, Juan P. Galeotti, Claudia Ermel, Reiko Heckel, Juan De Lara, Tiziana Margaria, ...
Abstract: Graph Grammars have been often used for modeling dynamic changes in software architectures. In particular, we have previously characterized some classes of dynamicity in terms of particular...
Fork Algebras as a Formalism to Reason Across Behavioral Specifications (Extended Abstract) (2008)
Marcelo F. Frias, Juan P. Galeotti
Abstract. Describing systems through the specification of different views is a well accepted practice in modern software engineering. In this paper we show how to reason across behavioral...
DynAlloy as a Formal Method for the Analysis of Java Programs (2008)
Juan P. Galeotti, Marcelo F. Frias
Abstract. DynAlloy is an extension of the Alloy specification language that allows one to specify and analyze dynamic properties of models. The analysis is supported by the DynAlloy Analyzer tool. In...