Temporal Assertions using AspectJ

Eric Bodden, Volker Stolz, RWTH Aachen

We present a runtime verification framework for Java programs.
Properties can be specified in Linear-time Temporal Logic (LTL) over
AspectJ pointcuts.
These properties are checked during
program-execution by an automaton-based approach where transitions are
triggered through aspects.
No Java source code is necessary since AspectJ works on the bytecode
level, thus even allowing instrumentation of third-party applications.
As an example, we discuss safety properties and lock-order reversal.