IntroductionFrom LTL to alternating automataPath semantics for LTLGenerating automataDeterminisationSoundness on finite pathsInstrumenting the program with AspectJPutting it all togetherLTL in the state space of a Java programCan we see the code, please?Running the applicationOverheadLock-order reversalRelated workConclusion and future workReferencesRV 2005 Preliminary VersionTemporal Assertions using AspectJVolker Stolz and Eric BoddenDept. of Computer ScienceProgramming Language s and Program AnalysisRWTH Aac he n University52056 Aache n, GermanyEmail: {stolz,bodden}@i2.informatik.rwth-aachen.deAbstractWe present a runtime verification framework for Java programs. Properties canbe specified in Linear-time Temporal Logic (LTL) over AspectJ pointcuts. Theseproperties are checked during program-execution by an automaton-based approachwhere transitions are triggered through aspects. No Java source code is necessarysince AspectJ works on the bytecode level, thus even allowing instrumentation ofthird-party applications. As an example, we discuss safety properties and lock-orderreversal.Key words: Runtime verification, LTL, AspectJ, aspect-orientedprogramming, alternating automata.1 IntroductionTo avoid misbehaviour, many software products include assertions which checkthat certain states on the execution path satisfy given constraints and other-wise either abort execution or execute specific error-handling. These assertionsare usually limited to testing the values of variables. However, often it wouldbe convenient not only to reason about a single state but also about a se-quence of states. This enables the developer to reason about control flow andexecution paths. In previous work [15], we discussed a symbolic checker forparametrised LTL formulae over finite paths which allowed us e.g. to reasonabout a problem found in multi-threaded applications commonly referred toas lock order reversal. At runtime, potential problems would be pointed outto the developer. We have implemented a working prototype with similarfunctionality for Java applications using a symbolic checker based on the codegeneration approach we describe in the following. The major contribution ofthis work is to propose an alternative, automaton-based solution which allowsfor even more expressiveness, though yielding better performance.This is a preliminary version. The final version will be published inElectronic Notes in Theoretical Computer ScienceURL: www.elsevier.nl/locate/entcsStolz and BoddenA major drawback of the former approach was that annotations drivingthe checker had to be inserted into the source code of the application undertest. For practical purposes, we supplied an annotated replacement for theconcurrency-library. Applications wishing to use this framework thus had tobe recompiled.Also, such source code-based hooks may lead to severe problems with re-spect to object-oriented properties such as behavioural subtyping: Any speci-fication which is stated for a certain class should also hold for all its subclasses.The use of source code annotations within method bodies does not reflect suchimplicit rules. Thus we restrict our formalism in such a way that it only al-lows to reason about well-defined interfaces, meaning method calls and fieldaccesses. The recent success of the utility Valgrind [11] shows that there issufficient demand for better debugging support (in contrast to techniques likemodel checking).In Section 2 we give a short introduction into temporal logic. Insteadof symbolically checking a formula, we use a translation into an alternatingautomaton. Section 3 discusses instrumentation of (Java) applications andfocuses on aspect-oriented programming in AspectJ. The combination of LTLand AspectJ in Section 4 yields a state-m achine for each formula to be checkedthrough a finite automaton where transitions are driven by an aspect. Wediscuss an extension to parametrised automata for handling recurring patternswith state and conclude in Section 5.2 From LTL to alternating automataIn this section we give a finite path semantics for LTL and remind the readeron how to translate LTL formulae into alternating automata.2.1 Path semantics for LTLLinear-time temporal logic (LTL) [12] is a subset of the Computation TreeLogic CTL∗and extends propositional logic with operators which describeevents along a computation path. The operators of LTL have the followingmeaning:•“Next” (X ϕ): The property ϕ holds in the next step•“Finally” (F ϕ): ϕ will hold at some state in the future•“Globally” (G ϕ): At every state on the path φ holds•“Until” (ϕ U ψ): ϕ has to hold until finally ψ holds.•“Release” (ϕ R ψ): Dual of U; expresses that the second property holdsalong the path up to and including the first state where the first propertyholds, although the first property is not required to hold eventually.Usually LTL is defined over infinite paths. For runtime verification, weassume that the verification process is stopped at some point in time and2Stolz and Boddencorrespondingly the LTL formulae have to be evaluated over a finite path.Thus we declare the semantics as follows.Let PROP be a set of atomic propositions and w = w[1]...w[n] ∈ (2PROP)na finite path. For each path position w[j] (1 ≤ j ≤ n) and propositionp ∈ {p1, ..., pm} and formulae ϕ and ψ:w[j] |= tt, w[j] 6|= ff,w[j] |= p iff p ∈ w[j]|= X ϕ iff j < n and w[j + 1] |= ϕ|= F ϕ iff ∃k (j ≤ k ≤ n) s.th. w[k] |= ϕ|= G ϕ iff ∀k (j ≤ k ≤ n) → w[k] |= ϕ|= ϕ U ψ iff ∃k (j ≤ k ≤ n) s.th. w[k] |= ψ∧ ∀l (j ≤ l < k) → w[l] |= ϕ|= ϕ R ψ iff ∀k (j ≤ k ≤ n) → w[k] |= ψ∨ ∃l (j ≤ l < k) s.th. w[l] |= ϕWe write w |= ϕ if w[1] |= ϕ. Furthermore we consider formulae in nega-tion normal form where negations are pushed down to the propositions usingbasic equivalences. We call the set of all LTL formulae in this form LTLNN.Our implementation will be b uilt on Next, Until and Release, so we use thefollowing equivalences to express Finally and Globally:F ϕ = tt U ϕ G ϕ = ff R ϕ2.2 Generating automataIn our previous approach, we successively check all propositions on top-levelof the formula, i.e. those that are not shadowed by temporal operators. Then,the outer temporal operators are unrolled once. But nested temporal oper-ators will lead to constantly expanding formulae. It is hard to reason whatset of minimisation step s would be complete in order to counterbalance