Graph-based Specification and Verification for Aspect-Oriented Languages

Aspect-oriented software development aims at improving separation of concerns at all levels in the software development life-cycle, from architecture to code implementation. In particular, aspect-oriented programming addresses separation of concerns at the implementation level, by allowing the modular expression of crosscutting concerns. In this thesis we strive to develop verication methods specifically for aspectoriented languages. For this purpose, we model the behaviour of these languages through an operational semantics. We use graph transformations to specify these semantics. Graph transformation has mathematical foundation, and provides an intuitive way to describe component-based systems, such as software systems. In addition, graph transformations have an executable nature, and can be used to generate the execution state space of programs. We use these state spaces for the verification of programs with aspects. We start by defining an improvement of specification by rule-based systems. Pure rule-based systems typically consist of a single, unstructured set of rules. The behaviour of such systems is that all rules are applicable in every state. Rules can then only be forced into a certain order of application by adding special elements to the states, which are tested for within the rules. In other words, control over rule applicability is not explicit but has to be encoded in the state, which reduces understandability and maintainability of the rule-based system as a whole. We propose so-called control automata, which can be added on top of pure rule-based systems. The resulting behaviour is defined as the product of the original state space and the control automaton. Our control automata include so-called failure transitions, representing the observation of the non-applicability of one or more rules. The result is a reactive semantics for control expressions, which is distinct from the usual input-output semantics. Control automata may introduce articial non-determinism into the behaviour, which is an undesirable effect. We introduce guarded control automata to get rid of this effect, and we define a semantics preserving transformation from ordinary control automata to guarded ones. In the next part of the thesis, we specify the run-time semantics of a number of aspect-oriented languages, namely of (1) Composition Filters, (2) Featherweight Java with assignments with an aspectual extension, and (3) a subset of multithreaded Java extended with a subset of AspectJ. We illustrate how such a graph-based semantics can aid in understanding the run-time behaviour of a language. Moreover, we show that such a semantics can be used to simulate a (partial) program and we expose the steps involved in the execution of such a program. We illustrate that this executable nature benefits the rigour of the specification method; mistakes are easily detected by simply testing the simulation. Finally, we show that the resulting labelled transition systems can be used for existing verification methods. Then, we propose two novel approaches that address complications caused by the use of aspect-oriented programming. The first approach addresses a problem that can occur in many aspect-oriented languages. Aspects that in isolation behave correctly may interact when being combined. When interaction changes an aspect's behaviour or disables an aspect, we call this interference. One particular type of interference occurs when aspects are applied to shared join points, since then the ordering of the aspects can also influence the behaviour of the composition. We present an approach to detect aspect interference at shared join points. The approach is based on simulation of all orderings of the advices that are scheduled for execution at a shared joinpoint. A confluence analysis is performed on the resulting state space to detect whether the execution order has aected the resulting states. The second approach addresses the problem of verification of dynamic properties of systems. These properties can only be verified by simulating the execution of the system: an execution semantics is required. More specifically, we deal with properties that require tracking of individual objects over time. We stress the need for automatic verification of properties (or constraints) for aspect-oriented programming because of the obliviousness properties of such languages: a developer cannot tell from looking at the base code that aspects are executed. When software evolves, existing functionality may break unintentionally. We propose to augment an existing graph-based execution semantics with special verification rules. These rules can, when needed, add information to the graphs for tracking of objects. The properties are specified as events (or interactions) related to roles. Once these roles are identified in the syntax, the program can be verified regardless of implementation details. We show that the approach can be applied to both object-oriented and aspect-oriented implementations