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

TL;DR

This paper introduces zone-based online monitoring algorithms for real-time systems that accurately handle variable communication delays, improving upon traditional methods that require costly parametric automata verification.

Contribution

It presents novel zone-based algorithms for runtime verification of real-time systems with parametric delays, implemented within UPPAAL, avoiding complex parametric automata verification.

Findings

Algorithms handle parametric delays exactly

Implementation in UPPAAL shows promising results

Avoids costly parametric automata verification

Abstract

Timed B\"uchi 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. This direct construction however only is faithful if observation of the trace is immediate in the sense that the monitor (or test harness, respectively) can assign exact time stamps to the actions it observes, which 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.