Emilia Katz, Ph.D. Thesis Seminar
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.