Runtime Verification of Timed LTL using Disjunctive Normalized Equation Systems

Abstract

In this paper we present a new framework for runtime verification of properties of real time systems such as financial systems or backend databases. Such a systems has a semantics which resemples that of timed traces, namely a sequence of states where each state consists of predicates true in this state and then a timestamp explaining when the state is valid. We present a logic, LTLt, which is an extension of LTL with time constraints and a freeze quantifier and show how formulae in this logic are able to express properties of bounded liveness and safety which are ideal for these systems. It is shown how a formula in LTLt may be rewritten to a certain disjunctive normal form suitable for checking a real time system at runtime. The normal form captures the essential part of runtime verification by a set of mutually defined formula identifiers, each expressing two things: What should hold now and which formula identifiers that will need to hold in the next state. As part of the theoretical foundation for this work we propose a characterization of Runtime Verification and address the challenges in developing a method which is both sound and complete while at the same time efficient.