Distributed Monitoring of Timed Properties

TL;DR

This paper introduces an online distributed monitoring algorithm for timed properties that accounts for clock imprecision and partial information, enabling early and reliable verdicts in complex systems.

Contribution

It presents a novel algorithm for distributed runtime monitoring of timed automata that handles clock imprecision and event reordering, improving verdict accuracy and timeliness.

Findings

Algorithm effectively manages clock imprecision and event reordering.

Monitors can determine safe verdicts based on partial information.

The approach enhances early detection of property satisfaction or violation.

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.