Shmuel Katz, Technion

Aspect Categories and Classes of Temporal Properties 


Generic categories of aspects are described, and their potential value is
explained. For each such category, broad classes of syntactically
identifiable temporal properties are guaranteed to hold for a system with
any aspect of the category woven into it, if the property held of the system
without the aspect. Thus classes of properties preserved by the aspect are
defined. Moreover, simpler verification techniques are shown to hold for
classes of new temporal properties added by any aspect in the category.
Thus, the aspect categories and their relations to classes of temporal
properties can be used to construct reliable systems without expensive and
difficult proofs of properties for a system augmented with aspects.

For each category, its syntactic and semantic characteristics are presented
and a generic procedure to identify when an aspect belongs to the category
is described and related to existing code analysis systems, using static
analysis and dataflow techniques. The categories of aspects, identification
procedures, and analysis of property classes provide the needed foundations
for automatic code analysis modules to identify aspect categories.