Cutting Corners on Uncertainty: Zonotope Abstractions for Stream-based Runtime Monitoring

TL;DR

This paper introduces zonotope abstractions for stream-based runtime monitoring, enabling sound, bounded-memory analysis of sensor errors in safety-critical systems, with a focus on performance and false-positive trade-offs.

Contribution

It proposes using zonotopes as an abstract domain to accurately and efficiently approximate monitor states under sensor errors in runtime verification.

Findings

Zonotopes precisely capture affine monitor states.

Over-approximation with zonotopes provides sound bounded-memory monitoring.

Different over-approximation strategies impact performance and false-positive rates.

Abstract

Stream-based monitoring assesses the health of safety-critical systems by transforming input streams of sensor measurements into output streams that determine a verdict. These inputs are often treated as accurate representations of the physical state, although real sensors introduce calibration and measurement errors. Such errors propagate through the monitor's computations and can distort the final verdict. Affine arithmetic with symbolic slack variables can track these errors precisely, but independent measurement noise introduces a fresh slack variable upon each measurement event, causing the monitor's state representation to grow without bound over time. Therefore, any bounded-memory monitoring algorithm must unify slack variables at runtime in a way that generates a sound approximation. This paper introduces zonotopes as an abstract domain for online monitoring of RLola specifications. We demonstrate that zonotopes precisely capture the affine state of the monitor and that their over-approximation produces a sound bounded-memory monitor. We present a comparison of different zonotope over-approximation strategies in the context of runtime monitoring, evaluating their performance and false-positive rates.