Sampling-based Runtime Verification

TitleSampling-based Runtime Verification
Publication TypeConference Paper
Year of Publication2011
AuthorsBonakdarpour, B., S. Navabpour, and S. Fischmeister
Conference NameProceedings of the 17th International Conference on Formal Methods (FM)
Date PublishedJune
Conference LocationLimerick, Ireland
ISBN Number978-3-642-21436-3
Keywordsmonitoring, predictability, Runtime verification, time-triggered

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 drawbacks to the system under scrutiny at run time: (1) significant overhead and (2) unpredictability. To circumvent the latter drawback, in this paper, we introduce a time-triggered approach, where the monitor frequently takes samples from the system 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 benchmark applications show that our approach introduces bounded overhead and effectively reduces involvement of the monitor at run time using negligible auxiliary memory.

Refereed DesignationRefereed
Related files: 


Looking for motivated students (undergrads and grads) interested in working on embedded software and systems research. Mail Sebastian Fischmeister for further information.