Decentralized Stream Runtime Verification for Timed Asynchronous Networks

TL;DR

This paper introduces a decentralized stream runtime verification approach for timed asynchronous networks, enabling effective monitoring of distributed systems with minimal resource use despite network delays and failures.

Contribution

It presents the first solution for timed asynchronous monitoring, generalizing previous synchronous methods and establishing conditions for resource-bounded monitoring independent of trace length.

Findings

Effective monitoring in asynchronous networks demonstrated

Resource bounds achieved regardless of trace length

Empirical evaluation confirms theoretical effectiveness

Abstract

We study the problem of monitoring distributed systems where computers communicate using message passing and share an almost synchronized clock. This is a realistic scenario for networks where the speed of the monitoring is sufficiently slow (at the human scale) to permit efficient clock synchronization, where the clock deviations is small compared to the monitoring cycles. This is the case when monitoring human systems in wide area networks, the Internet or including large deployments. More concretely, we study how to monitor decentralized systems where monitors are expressed as stream runtime verification specifications, under a timed asynchronous network. Our monitors communicate using the network, where messages can take arbitrarily long but cannot be duplicated or lost. This communication setting is common in many cyber-physical systems like smart buildings and ambient living. Previous approaches to decentralized monitoring were limited to synchronous networks, which are not easily implemented in practice because of network failures. Even when networks failures are unusual, they can require several monitoring cycles to be repaired. In this work we propose a solution to the timed asynchronous monitoring problem and show that this problem generalizes the synchronous case. We study the specifications and conditions on the network behavior that allow the monitoring to take place with bounded resources, independently of the trace length. Finally, we report the results of an empirical evaluation of an implementation and verify the theoretical results in terms of effectiveness and efficiency.