A closer look at aspect interference and cooperation

In this work we consider specification and compositional verification for interference detection when several aspects are woven together under joint-weaving semantics without recursion. In this semantics, whenever a joinpoint of an aspect is reached, the corresponding advice is begun even if the joinpoint is inside the advice of other aspects. This captures most of the possible aspect interference cases in AspectJ. Moreover, the given technique is used to capture cooperation among aspects, which enhances modularity. The extended specification and proof obligations should provide insight to the possible interactions among aspects in a reusable library. Categories and Subject Descriptors D.2.1 [Software Engineering]: Requirements/Specifications; D.2.4 [Software Engineering]: Software/Program Verification—Correctness proofs, Model checking General Terms Languages, Verification Keywords Aspects, Joint-Weaving, Verification, Composition, Cooperation, Interference

• Type: Journal
• Year: 2012
• Where: AOSD
• Authors: Cynthia Disenfeld, Shmuel Katz
• Keywords: AOSD 2012, Correctness Proofs, Interference Detection, Proof Obligations, Software Engineering