Temporal Assertions using AspectJ

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. Key words: Runtime verification, LTL, AspectJ, aspect-oriented programming, alternating automata.

• Type: Journal
• Year: 2006
• Where: ENTCS
• Authors: Volker Stolz, Eric Bodden
• Keywords: AspectJ, ENTCS 2006, Runtime Verification, Runtime Verification Framework