טכניון מכון טכנולוגי לישראל
הטכניון מכון טכנולוגי לישראל - בית הספר ללימודי מוסמכים  
M.Sc Thesis
M.Sc StudentGoldman Max
SubjectModular Verification of Aspects
DepartmentDepartment of Computer Science
Supervisor Professor 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.