Efficient Runtime Verification of Real-Time Systems under Parametric Communication Delays

Timed Büchi automata provide a very expressive formalism for expressing requirements of real-time systems. Online monitoring and active testing of embedded real-time systems can then be achieved by symbolic execution of such automata on the trace observed from the system. However, this direct construction is only faithful if the observation of the trace is immediate in the sense that the monitor (or test harness, respectively) can assign exact timestamps to the actions it observes. This is rarely true in practice due to the substantial and fluctuating parametric delays introduced by the circuitry connecting the observed system to its monitoring or testing device. We present purely zone-based online monitoring and testing algorithms, which handle such parametric delays exactly without recurrence to costly verification procedures for parametric timed automata. We have implemented our algorithms on top of the real-time model checking tool Uppaal , and report on encouraging initial results.