Technical Report MSC-2006-08

Title: Verifying Scenario-Based Aspect Specifications
Authors: Emilia Katz
Supervisors: Shmuel Katz
Abstract: Software systems specifications are often described as a set of typical scenarios. Some of the desired scenarios are crosscut by other requirements, called aspects, also naturally described as scenarios. Aspect descriptions are independent of the description of the non-aspectual scenarios, but the crosscutting relationship between them has to be specified, so for each aspect a description of its join-points is provided. When aspectual scenarios are added to the system, we need to prove that every execution is equivalent to one in which the aspectual scenarios occur as blocks of operations immediately at their join-points, and all the other operations form a sequence of non-aspectual scenarios, interrupted only by the aspectual scenarios. The verification process consists of three parts. First, the join-points of the aspectual scenarios are found. Then we prove that each execution is equivalent to one in which the aspectual scenarios are applied correctly, and the last part is to prove that the non-aspectual scenarios can indeed be formed into blocks interrupted only by aspect advices. We extend an existing method of automatic verification for non-aspect systems to the case of systems with scenario-based aspect specifications. A prototype implementation based on Cadence SMV is also extended accordingly, and an efficient optimization is provided, though not enforced upon the user.
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