Previous article

Next article

Design-level Detection of Interactions in Aspect-UML models using Alloy

Farida Mostefaoui and Julie Vachon, DIRO, University of Montreal, Quebec, Canada


PDF Icon
PDF Version


Aspect-oriented (AO) programming has emerged as a promising paradigm to improve modularity by providing mechanisms to capture and execute crosscutting concerns in software applications. Among others, AO allows developers to incrementally modify the behavior of a base program, by introducing aspects which implement crosscutting concerns having effects at various points throughout a program. Hence, despite the clean separation of concerns in aspect-oriented systems, it remains difficult to predict the effect of a given aspect on this base program. Once woven, does an aspect still achieve what it was intended for? Does it violate base program properties that should be preserved? Does it interfere with the properties of other aspects? These questions address the well known aspect interaction problem, encountered within the AO paradigm. This article tackles the interaction problem in the context of formal AO system model analysis and verification. To be more precise, this work considers AO models written in Aspect-UML (our UML profile). Aspect-UML does not depend on any AO language specific features nor is it associated with any specific development process. This paper first explains how Aspect-UML models can be translated into Alloy, a simple structural first-order logic modeling language which can be formally analyzed. Given this translation, it then demonstrates how Alloy’s model analyzer can be used to verify aspect interactions of an Aspect-UML model.

Note: Due to the typographical sophistication of this article, no HTML version is available. Please use the PDF version.

About the authors

  Farida Mostefaoui is a PhD candidate at University of Montreal (DIRO), Quebec, Canada. She is a member of the GEODES Laboratory, pursuing a Ph.D. thesis on an aspect oriented approach for the detection and the verification of aspect interactions. She can be reached at

  Julie Vachon works as an assistant professor at the Departement of Computer Science of University of Montreal in the software engineering lab GEODES. She studied computer science in Montreal, Lyon and Lausanne where she obtained, in 2000, a Ph.D. degree from the Swiss Federal Institute of Technology. Her research interests include aspect-oriented modeling, incremental design of safe and fault-tolerant systems, formal specification and verification. She can be reached at

Cite this article as follows: Farida Mostefaoui and Julie Vachon: Design-level Detection of Interactions in Aspect-UML models using Alloy, in Journal of Object Technology, vol. 6, no. 7, Special Issue: Aspect-Oriented Modeling, August 2007, pages 137–165, 2007 08/article6


Previous article

Next article