Abstract
Aspect-oriented programming has become an increasingly important means of expressing cross-cutting program abstractions. Despite this, aspects lack support for computer-aided 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.
Original language | English |
---|---|
Pages | 137-146 |
Number of pages | 10 |
DOIs | |
State | Published - 2004 |
Event | Twelfth ACM SIGSOFT International Symposium on the Foundations of Software Engineering, SIGSOFT 2004/FSE-12 - Newport Beach, CA, United States Duration: 31 Oct 2004 → 5 Nov 2004 |
Conference
Conference | Twelfth ACM SIGSOFT International Symposium on the Foundations of Software Engineering, SIGSOFT 2004/FSE-12 |
---|---|
Country/Territory | United States |
City | Newport Beach, CA |
Period | 31/10/04 → 5/11/04 |
Keywords
- Aspect-oriented software
- Model checking
- Modular verification