Sciweavers

Share
ENTCS
2006

Temporal Assertions using AspectJ

8 years 10 months ago
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.
Volker Stolz, Eric Bodden
Added 12 Dec 2010
Updated 12 Dec 2010
Type Journal
Year 2006
Where ENTCS
Authors Volker Stolz, Eric Bodden
Comments (0)
books