Decentralized Stream Runtime Verification for Timed Asynchronous Networks

Abstract

Problem: We study the problem of monitoring distributed systems such as smart buildings, ambient living, wide area networks and other distributed systems that get monitored periodically in human scale times. In these systems 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 (like seconds or tens of seconds) to permit efficient clock synchronization, where clock deviations are small compared to the time precision and frequency required by the monitoring. Solution: More concretely, we propose a solution to monitor decentralized systems where monitors are expressed as stream runtime verification specifications. We solve the problem for “timed asynchronous networks”, where computational nodes where the monitors run have a synchronized clock with a small bounded maximum drift. These nodes communicate using a network, where messages can take arbitrarily long but cannot be duplicated or lost. his setting is common in many cyber-physical systems like smart buildings and ambient living. This assumption generalizes the synchronous monitoring case. Previous approaches to decentralized monitoring were limited to synchronous networks, which are not easily implemented in practice because of network failures. Even when network failures are unusual, they can require several monitoring cycles to be repaired. Methodology: We describe formally the monitoring problem for timed-asynchronous networks, we describe a decentralized algorithm and provide proofs of its correctness. Afterwards, we formally analyze the complexity of our solutions and provide two analysis techniques to approximate the memory requirements. Finally, we implement the algorithm and perform an empirical evaluation with real data extracted from four different datasets. Contributions: We propose a solution to the timed asynchronous decentralized monitoring problem. 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.