About Eagle Flier

Eagle Flier is a rule-based runtime verification framework. Given a finite sequence of program states and a set of formulas written in the temporal logic Eagle, the tool checks if the trace satifies the set of formulas. The logic Eagle has been designed to allow users define their own recursive temporal operators and then write monitors using those operators. The logic Eagle introduced in [BGHSvmcai04] supports recursive parameterized equations, with a minimal/maximal fix-point semantics, together with three temporal operators: next-time, previous-time, and concatenation. Rules which are used to define new temporal operators can be parameterized with formulas and data-values, thus supporting specifications that can reason about data which can span over an execution trace. The expressivity of Eagle, which is indeed very rich, as shown in [BGHSpadtad04] and [BGHSvmcai04], can express specifications about real-time, statistics and data-values. The tool, Eagle Flier, is implemented as a Java library and involves novel techniques for monitoring Eagle formulas. Monitoring is done on a state-by-state basis, without storing the execution trace.