|M.Sc Student||Katz Emilia|
|Subject||Verifying Scenario-Based Aspect Specifications|
|Department||Department of Computer Science||Supervisor||Professor Shmuel Katz|
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.