Modular Verification of Strongly Invasive Aspects

An extended specification for aspects, and a new verification method based on model checking are used to establish the correctness of strongly-invasive aspects, independently of any particular base program to which they may be woven. Such aspects can change the underlying base program variables to new states, and after the aspect advice has completed, the base program code continues from states that were previously unreachable. The needed changes in the MAVEN model checker are described, and the soundness of the verification method is proven. An example is shown of its application to aspects that provide various bonus points to student grading programs. Categories and Subject Descriptors D.2.4 [Software Engineering]: Software/Program Verification--Model Checking; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs General Terms Verification, languages Keywords Aspects, model-checking, specification, modularity

• Type: Conference
• Year: 2009
• Where: BIRTHDAY
• Authors: Emilia Katz, Shmuel Katz
• Keywords: Applied Computing, Base Program, BIRTHDAY 2009, Particular Base Program, Verification Method