Runtime Verification over Out-of-order Streams

TL;DR

This paper introduces a runtime verification method for distributed systems with unreliable communication, using an expressive logic with a novel three-valued semantics, enabling sound and complete reasoning over out-of-order event streams.

Contribution

It proposes a new three-valued semantics for real-time logic with freeze quantifiers, tailored for runtime verification of out-of-order distributed streams.

Findings

Prototype scales to hundreds of thousands of events per second

Algorithms reason soundly and completely over out-of-order streams

Approach effectively verifies distributed systems with unreliable channels

Abstract

We present an approach for verifying systems at runtime. Our approach targets distributed systems whose components communicate with monitors over unreliable channels, where messages can be delayed, reordered, or even lost. Furthermore, our approach handles an expressive specification language that extends the real-time logic MTL with freeze quantifiers for reasoning about data values. The logic's main novelty is a new three-valued semantics that is well suited for runtime verification as it accounts for partial knowledge about a system's behavior. Based on this semantics, we present online algorithms that reason soundly and completely about streams where events can occur out of order. We also evaluate our algorithms experimentally. Depending on the specification, our prototype implementation scales to out-of-order streams with hundreds to thousands of events per second.