Runtime Verification of Timed LTL using Disjunctive Normalized Equation Systems |
| |
Authors: | Kre Jelling Kristoffersen Christian Pedersen Henrik Reif Andersen |
| |
Affiliation: | aDepartment of Innovation, IT University of Copenhagen, Copenhagen, 2400 NV, Denmark |
| |
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. |
| |
Keywords: | Timed LTL Disjunctive Normalized Equation Systems Charaterization of Runtime Verification Property Tranformation |
本文献已被 ScienceDirect 等数据库收录! |