A Categorical Framework for the Specification and the Verification of Aspect
Oriented Systems

One of the main goals of software engineering is to enable the construction of large, complex and reliable software in timely fashion. Object-oriented (OO) technology has provided modeling and programming principles and techniques that allow developing complex software systems both in academic and industrial areas. In return, experience gained in OO system development has allowed discovering some limitations of object technology (e.g., code scattering and poor traceability problems). Aspect Oriented (AO) Technology is a post-object-oriented technology emerged to overcome limitations of Object Oriented (OO) Technology, such as the crosscutting concern problem. Crosscutting concerns are scattered and tangled concerns. Major goals of Aspect Oriented Programming (AOP) include improving modularity, cohesion, and overall software quality. Aspect Oriented Programming results in the evolution of programming activities to fullblown software engineering processes, to preserve modularity and traceability, which are two important properties of high-quality software. Yet, there are also many challenges in AO Technology. Reasoning, specification, and verification of AO programs present unique challenges especially as such programs evolve over time. Consequently, modular reasoning of such programs is highly attractive as it enables tractable evolution, otherwise necessitating that the entire program be reexamined each time a component is changed or is added. It is well known in the literature, however, that modular reasoning about AO programs is difficult due to the fact that the aspects applied often alter the behavior of the base components [47]. The same modular reasoning difficulties are also present in the specification and verification phases of software development process. To the best of our knowledge, AO modular specification and verification is a weakly covered subject and constitutes an interesting open research field. Also, aspect interaction is a major concern in the aspect-oriented community. To deal with these problems, we choose to use category theory and algebraic specification techniques. To achieve the above thesis goals, we use the work of Wiels [110] and other contributions such as the one described in [25]. We assume at the beginning that the system under development is already decomposed into aspect and class components. The first contribution of our thesis is the extension of the algebraic specification technique to the notion of aspect. Secondly, we define a logic, LA that is used in specification bodies to describe the behavior of these components. The third contribution concerns the defini tion of the weaving operator corresponding to the weaving interconnection relationship between aspect modules and class modules. The fourth contribution consists of the design of a prevention policy that is used to prevent or avoid undesirable aspect interactions in aspect-oriented systems.

Keyphrases: Software Engineering, Modular reasoning, Aspect Oriented Development, Formal Specification, Formal Verification, Aspect Interaction, Prevention Policy, Interaction Aspect, Modularity