Verifying aspect advice modularly

Aspect-oriented programming has become an increasingly important means of expressing cross-cutting program abstractions. Despite this, aspects lack support for computeraided verification. We present a technique for verifying aspect-oriented programs (expressed as state machines). Our technique assumes that the set of pointcut designators is known statically, but that the actual advice can vary. This calls for a modular technique that does not require repeated analysis of the entire system every time a developer changes advice. We present such an analysis, addressing several subtleties that arise. We also present an important optimization for handling multiple pointcut designators. We have implemented a prototype verifier and applied it to some simple but interesting cases. Categories and Subject Descriptors: D.2.4 [Software Engineering]: Software/Program Verification; D.3.2 [Programming Languages]: Language Classifications General Terms: Algorithms, Languages, Verification

• Type: Conference
• Year: 2004
• Where: SIGSOFT
• Authors: Shriram Krishnamurthi, Kathi Fisler, Michael Greenberg
• Keywords: Cross-cutting Program Abstractions, Multiple Pointcut Designators, Pointcut Designators, SIGSOFT 2004, Software Engineering