|Ph.D Student||Katz Emilia|
|Subject||Analysis and Detection of Interactions among Aspects|
|Department||Department of Computer Science||Supervisor||Professor Shmuel Katz|
|Full Thesis text|
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.
Several issues are treated that extend the applicability of proof methods for aspects, with emphasis on interference among aspects.
One extension is for treatment of aspects that might bring the computation to a state previously unreachable in the base system. Such aspects are termed strongly invasive and they were not covered by previous verification methods. 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.
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 is presented based on off-line model checking of pairs of aspects for a generic model expressing the specifications. When an aspect is added to a library of non-interfering 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.
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.
Extensions to the MAVEN system implementing the theory are de-scribed, and a case study of specification and interference checks for a library of aspects is given.