Model Checking Aspect-Oriented Design Specification

Aspects can be used in a harmful way that invalidates desired properties. Rigorous specification and analysis of aspect design is thus highly desirable. This paper presents an approach to model-checking state-based specification of aspect-oriented design. It is based on a rigorous formalism for capturing crosscutting concerns with respect to the design-level state models of classes. An aspect model not only encapsulates pointcuts and advice, but also supports inter-model declarations, aspect precedence, and references to the behaviors of other classes in advice models. For verification purposes, we convert the aspect-oriented state model of a system into woven models and further transform the woven models and the non-base class models into FSP processes. The generated FSP processes are checked by the LTSA model checker against the desired system properties. We have applied our approach to the modeling and verification of a non-trivial aspect-oriented cruise control system. A total of 21 properties that provide a comprehensive coverage of the system requirements are successfully formalized and verified.