טכניון מכון טכנולוגי לישראל
הטכניון מכון טכנולוגי לישראל - בית הספר ללימודי מוסמכים  
M.Sc Thesis
M.Sc StudentKatz Emilia
SubjectVerifying Scenario-Based Aspect Specifications
DepartmentDepartment of Computer Science
Supervisor Professor 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.