Event-Based Runtime Checking of Timed LTL

TR-2003-37, Author: Kåre Jelling Kristoffersen

Kåre J. Kristoffersen
Christian Pedersen
Henrik R. Andersen

November 2003

Abstract

In this paper we describe an event-based algorithm for runtime verification of timed linear temporal logic. The algorithm is based on a rewriting of the formula expressing a desired or undesired property of a timed system. Rewriting takes place, at discrete points in time, but only when there is a relevant state-change taking place in the timed system, or a deadline, determined by the formula, has been passed. By limiting the rewriting to only points in time where an event occurs, and not at all discrete time-points, makes the algorithm useful in situations where there are large data sets and large differences in the relevant time scales (ranging perhaps from milliseconds to months as in business software).

The algorithm works by rewriting, for each event, the timed LTL formula into a residual formula that takes into account the time and system state at the occurence of the event. The residual formula will be the requirement for the timed system in the future, to be further rewritten at the occurrence of the next event. quad {bf Keywords: } Timed LTL, Disjunctive Normalized Equation Systems, Residual formula, Smallest Interesting Timepoint, Timed Based Fixed Point Reduction, Charaterization of Runtime Verification.

---

Technical report TR-2003-37 in IT University Technical Report Series, November 2003.

Available as PDF.