Stream-based Decentralized Runtime Verification

TL;DR

This paper introduces a stream-based decentralized runtime verification method for distributed industrial control systems, enabling real-time monitoring and aggregation of system behavior despite asynchrony and imperfect synchronization.

Contribution

It presents a novel technique for runtime monitoring of distributed systems modeled as input/output streams with partial synchrony, and provides a generalized decentralized verification approach.

Findings

Effective in synthetic experiments

Applicable to ICS and aircraft datasets

Handles asynchrony and imperfect clocks

Abstract

Industrial Control Systems (ICS) are often built from geographically distributed components and often use programmable logic controllers for localized processes. Since verification of such systems is challenging because of both time sensitivity of the system specifications and the inherent asynchrony in distributed components, developing runtime assurance that verifies not just the correctness of different components, but also generates aggregated statistics of the systems is of interest. In this paper, we first present a general technique for runtime monitoring of distributed applications whose behavior can be modeled as input/output {\em streams} with an internal computation module in the partially synchronous semantics, where an imperfect clock synchronization algorithm is assumed. Second, we propose a generalized stream-based decentralized runtime verification technique. We also rigorously evaluate our algorithm on extensive synthetic experiments and several ICS and aircraft SBS message datasets.