Abstract:

Aspects provide a modular way to describe system concerns 
including security, monitoring, fault-tolerance, or evolving 
requirements that cross-cut normal modularity units, such as the class 
inheritance hierarchy in an object-oriented system. The separate 
description of aspects, and their subsequent integration (called 
weaving) into systems provide new kinds of compositionality and reuse 
for complex system development. But how can we show that an aspect 
really adds the functionality it is supposed to, and moreover does not 
invalidate desirable properties of the system to which it is woven? How 
do multiple aspects interact, and can we discover possible interference 
among them?
Here we survey complementary approaches to the verification of systems 
that include aspects. One approach separates the determination of 
whether the aspect causes harm to the underlying system from the 
question of whether it adds the desired properties. We also consider 
when an analysis of just the aspect code is possible, and when the 
entire combination of the system with the aspect must be treated. A 
methodology known as aspect validation is suggested as an alternative 
both to traditional testing and to a full formal proof that the aspects 
always are correct. In aspect validation we prove separately that each
new weaving of the aspects satisfies its specification and does not 
invalidate desirable properties of the underlying system. The approach 
uses an existing software model checker, and automatically generates 
several model checking tasks every time a collection of aspects is 
integrated to an underlying system. New "validation aspects" that 
augment systems with specifications are a crucial part of the approach, 
and thus show an interesting application of aspects for the purpose of 
validating other aspects.
(The talk is self-contained, and does not assume prior familiarity with 
either aspects or formal methods.)