S.: Verifying scenario-based aspect specifications

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. As-pect descriptions are independent of the description of the non-aspectual scenarios, but the crosscutting relationship between them has to be spec-ified, 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 ev-ery execution is equivalent to one in which the aspectual scenarios oc-cur 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. We extend an existing method of au-tomatic 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