Aspects and formal methods

Aspects are now commonly used to add functionality that otherwise would cut across the structure of object systems. In this survey, both directions in the connection between aspects and formal methods are examined. On the one hand, the use of aspects to facilitate (general) software verification, and especially model checking, is demonstrated. On the other hand, the new challenges to formal specification and verification posed by aspects are defined, and several existing solutions are described.