Technical Report MSC-2006-23

Title: Modular Verification of Aspects
Authors: Max Goldman
Supervisors: Shmuel Katz
Abstract: 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.

CopyrightThe above paper is copyright by the Technion, Author(s), or others. Please contact the author(s) for more information

Remark: Any link to this technical report should be to this page (, rather than to the URL of the PDF files directly. The latter URLs may change without notice.

To the list of the MSC technical reports of 2006
To the main CS technical reports page

Computer science department, Technion