Aspect Validation Using Model Checking

Abstract

The model checking of applications of aspects is explained, by showing the stages and proof obligations when a collection of generic aspects (called a superimposition) is combined with a basic program. We assume that both the basic program and the collection of aspects have their own specifications. The Bandera tool for Java programs is used to generate input for model checkers, although any similar tool could be employed. New verification aspects and superimpositions are defined to modularize the proofs, and separate the proof-related code from the program and the aspects. This allows generating and activating a series of model checking tasks automatically each time a superimposition is applied to a basic program, achieving superimposition validation. A case study that monitors and checks an underlying bounded buffer program is presented.

Dedicated to Zohar: teacher, advisor, and friend, from whom I learned about the importance of both invariance and liveness in multiple aspects of verification and life.-Shmuel