Dynamic trace checking with AspectJ

 

Eric Bodden

Mc Gill Univ., CA

Abstract:

We present Tracechecks, a formalism for specifying 'temporal
assertions' and semantic interfaces using Linear Time Logic (LTL).
Semantic interfaces allow developers to document and verify contracts
on the dynamic control flow of an application.  Our framework allows
binding of objects in matched states and triggering actions when
a temporal assertion has been violated, thus accessing the program
history.

We discuss the efficiency of our and related approaches using
regular expressions or context-free grammars. Latest static
optimization techniques have brought trace based evaluation from
``infeasible'' to ``feasible'' but have now almost reached their
boundaries, so that we have to exploit even more advanced techniques
to optimize any further. Hence, we propose optimizations
based on dynamic advice deployment to the annotated application
which will benefit other trace mechanisms (for example, Tracematches)
as well.