Aspect Validation Using Model Checking

11 years 10 months ago
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...
Shmuel Katz, Marcelo Sihman
Added 23 Aug 2010
Updated 23 Aug 2010
Type Conference
Year 2003
Authors Shmuel Katz, Marcelo Sihman
Comments (0)