Aspect Validation Using Model Checking

Aspects are intended to add needed functionality to a system or to treat concerns of the system by augmenting or changing the existing code in a manner that cross-cuts the usual class or process hierarchy. However, sometimes aspects can invalidate some of the already existing desirable properties of the system. This paper shows how to automatically identify such situations. The importance of specifications of the underlying system is emphasized, and shown to clarify the degree of obliviousness appropriate for aspects. The use of regression testing is considered, and regression verification is recommended instead, with possible division into static analysis, deductive proofs, and aspect validation using model checking. Static analysis of only the aspect code is effective when strongly typed and clearly parameterized aspect languages are used. Spectative aspects can then be identified, and imply absence of harm for all safety and liveness properties involving only the variables and fiel...

• Type: Conference
• Year: 2003
• Where: BIRTHDAY
• Authors: Shmuel Katz, Marcelo Sihman
• Keywords: Applied Computing, Aspect Code, Aspect Validation, BIRTHDAY 2003, Deductive Proofs