Max Goldman

Modular Verification of Aspects

M.Sc. Thesis

Supervisor: Assoc. Prof. Shmuel Katz

Aspects are separate code modules that can capture crosscutting concerns more effectively than existing object-oriented techniques. An aspect is combined, or "woven," with a base program at joinpoints, locations where the aspect code will run in the resulting augmented system.

We define a novel formal approach to verify that an aspect will provide desired properties to the augmented system whenever it is woven with a base program that satisfies the assumptions of the aspect. This verification uses state machine models of aspects, constructing a single state machine based on the linear temporal logic (LTL) description of the assumptions, a description of the joinpoints, and the state machine of the aspect code. A theorem is shown that if this constructed machine satisfies the desired properties, so will an augmented state machine built from any base machine satisfying the assumptions. This theorem holds under a somewhat restricted form of joinpoint description, and for aspects whose code always returns to states reachable in the original base machine.

This technique is the first example of once-and-for-all verification of aspects in which the verification examines only the aspect in isolation, rather than an augmented system or the aspect together with a particular base program. The usefulness of the technique is demonstrated with MAVEN, a prototype implementation sufficient to verify a number of example aspects. Language-based descriptions of aspects, as in AspectJ, can be converted to state machine versions using existing tools, thus providing generic modular verification of code-level aspects.