Distributed Monitoring of Timed Properties
Léo Henry, Thierry Jéron, Nicolas Markey, Victor Roussanaly
TL;DR
The paper addresses online distributed runtime verification for properties specified as deterministic timed automata in systems with asynchronous monitors and local clock skew $\sk$. It introduces approximate timed words (ATWs) to capture imprecise timestamps and potential inter-component reorderings, and develops a decomposition-based data structure $\CS(t)$ together with a $\Decomp(\atw,T)$ operator to incrementally compute verdicts. The main results prove soundness and completeness (up to $2\sk$-conclusive executions) of the verdict computation at the earliest safe date $\tmin_1(t)-\sk$ using reachability sets $\Inev(\Final_i)$ and $\Never(\Final_i)$. The work situates the approach within decentralized runtime verification, outlines related models and potential extensions (non-deterministic TA, reduced communication), and discusses practical implications for distributed real-time monitoring.
Abstract
In formal verification, runtime monitoring consists of observing the execution of a system in order to decide as quickly as possible whether or not it satisfies a given property. We consider monitoring in a distributed setting, for properties given as reachability timed automata. In such a setting, the system is made of several components, each equipped with its own local clock and monitor. The monitors observe events occurring on their associated component, and receive timestamped events from other monitors through FIFO channels. Since clocks are local, they cannot be perfectly synchronized, resulting in imprecise timestamps. Consequently, they must be seen as intervals, leading monitors to consider possible reorderings of events. In this context, each monitor aims to provide, as early as possible, a verdict on the property it is monitoring, based on its potentially incomplete and imprecise knowledge of the current execution. In this paper, we propose an on-line monitoring algorithm for timed properties, robust to time imprecision and partial information from distant components. We first identify the date at which a monitor can safely compute a verdict based on received events. We then propose a monitoring algorithm that updates this date when new information arrives, maintains the current set of states in which the property can reside, and updates its verdict accordingly.