Optimal Runtime Verification of Finite State Properties over Lossy Event Streams
This work addresses the challenge of efficient runtime verification for systems with event loss, offering a solution that is incremental in improving monitor design for specific domains like embedded systems.
The authors tackled the problem of monitoring finite state properties over lossy event streams, which reduces overhead but introduces uncertainty, by presenting a theoretical framework and constructing a monitor that is optimally sound and avoids false positives.
Monitoring programs for finite state properties is challenging due to high memory and execution time overheads it incurs. Some events if skipped or lost naturally can reduce both overheads, but lead to uncertainty about the current monitor state. In this work, we present a theoretical framework to model these lossy event streams and provide a construction for a monitor which observes them without producing false positives. The constructed monitor is optimally sound among all complete monitors. We model several loss types of practical relevance using our framework and provide construction of smaller approximate monitors for properties with a large number of states.