Skip to main content

Sampling-based Runtime Verification

Publication Type
Year of Publication
Conference/Journal Name
International Symposium on Formal Methods (FM)
The goal of runtime verification is to monitor the behavior of a system to check its conformance to a set of desirable logical properties.
The literature of runtime verification mostly focuses on event-triggered solutions, where a monitor is invoked by every change in the state of the system and evaluates properties of the system. This constant invocation introduces two major defects to the system under scrutiny at runtime: (1) significant overhead, and (2) unpredictability. To circumvent the latter defect, in this paper, we introduce a novel time-triggered approach, where the monitor frequently takes samples from the system in order to analyze the system’s health. We propose formal semantics of sampling-based monitoring and discuss how to optimize the sampling period using minimum auxiliary memory. We show that such optimization is NP-complete and consequently introduce a mapping to Integer Linear Programming. Experiments on real-world applications show that our approach introduces bounded overhead and effectively reduces involvement of the monitor at runtime using negligible auxiliary memory. We also show that in some cases it is even possible to reduce the overall overhead of runtime verification using our sampling-based approach when the structure of the system allows choosing long enough sampling period.