Title: Using Dataflow to Avoid Model Checking for Aspects

Shmuel Katz (Technion)
 
Abstract:

Aspect-oriented programming is an extension of the Object-Oriented paradigm

that allows adding features to a system that otherwise would cut across the usual

OO class structure. Rather than applying "expensive" formal verification

techniques such as model checking or inductive verification, an automatic

data and control flow tool is used to analyze the code of an aspect system.

Families of temporal logic properties, such as safety or liveness, are shown

to be maintained if aspects of certain categories are applied to the system.

The identification of the categories is done using the automatic data and

control flow tool, and the analysis of which properties are maintained

can be done once-and-for-all, independently of any particular system.

The goal is thus to develop an effective detection tool for categories of

aspects with implications for verification, and in particular for categories

that guarantee maintaining desirable properties or are easier to verify for

certain properties.