The Taub Faculty of Computer Science Events and Talks

Aspect-oriented programming is becoming a common approach to extend object systems with modules that cross-cut the usual class hierarchy. Aspects encapsulate treatment of concerns that otherwise would be scattered within an underlying application, and tangled with code treating other concerns. Often, insertion of several aspects into one system is desired and in that case the problem of interference among the aspects might arise, even if each aspect individually woven is correct relative to its specification. In this type of interference, one aspect can prevent another from having the required effect on a woven system. Such interference is defined and an incremental proof strategy based on off-line model checking pairs of aspects for a generic model expressing the specifications is presented. When an aspect is added to a library of noninterfering aspects, only its interaction with each of the aspects from the library needs to be checked. Such checks for each pair of aspects are proven sufficient to detect interference or establish interference freedom for any collection of aspects in a library. Several issues are treated that extend the applicability of proof methods for aspects. One extension is for treatment of interactions of aspects of all the categories, where the division of aspects to categories is done according to the possible influence of the aspects on the base system computations. An extended specification for aspects, and a new verification method based on model checking are presented. They are used to establish the correctness of strongly-invasive aspects independently of any particular base program to which they may be woven. Additional extension is needed for the case when multiple aspects can share a join-point. In this case they may, but do not have to, semantically interfere, and a specification refinement might be necessary to enable modular verification and interference detection among aspects even in the presence of shared join-points. An in depth analysis of aspect semantics and mutual influence of aspects at a shared join-point is presented, in order to enable distinguishing between potential and actual interference among aspects at shared join-points. An interactive semi-automatic procedure for specification refinement is described, that will help users define the intended aspect behavior more precisely.