Symbolic Runtime Verification for Monitoring under Uncertainties and Assumptions

TL;DR

This paper introduces a symbolic runtime verification framework that handles uncertainties and assumptions in system observations, enabling precise monitoring with constant memory in complex logical domains, demonstrated through automotive and health monitoring case studies.

Contribution

It proposes a novel symbolic approach to runtime verification that manages uncertainties and assumptions, with pruning strategies for constant memory monitoring in rich logical theories.

Findings

Constant memory monitoring achieved in Boolean and Linear Algebra domains.

Effective handling of imprecise inputs and assumptions improves verdict accuracy.

Prototype implementation successfully applied to car emissions and heart-rate monitoring.

Abstract

Runtime Verification deals with the question of whether a run of a system adheres to its specification. This paper studies runtime verification in the presence of partial knowledge about the observed run, particularly where input values may not be precise or may not be observed at all. We also allow declaring assumptions on the execution which permits to obtain more precise verdicts also under imprecise inputs. To this end, we show how to understand a given correctness property as a symbolic formula and explain that monitoring boils down to solving this formula iteratively, whenever more and more observations of the run are given. We base our framework on stream runtime verification, which allows to express temporal correctness properties not only in the Boolean but also in richer logical theories. While in general our approach requires to consider larger and larger sets of formulas, we identify domains (including Booleans and Linear Algebra) for which pruning strategies exist, which allows to monitor with constant memory (i.e. independent of the length of the observation) while preserving the same inference power as the monitor that remembers all observations. We empirically exhibit the power of our technique using a prototype implementation under two important cases studies: software for testing car emissions and heart-rate monitoring.