Verifying aspect advice modularly

Shriram Krishnamurthi, Kathi Fisler, Michael Greenberg

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.

BibTeX

@inproceedings{Krishnamurthi-al:FSE04,
  author    = {Shriram Krishnamurthi and
               Kathi Fisler and
               Michael Greenberg},
  title     = {Verifying aspect advice modularly},
  booktitle = {FSE},
  pages     = {137--146},
  publisher = {{ACM}},
  year      = {2004},
}

Verifying aspect advice modularly

Abstract

Related papers