Runtime Verification of LTL on Lossy Traces

TitleRuntime Verification of LTL on Lossy Traces
Publication TypeConference Paper
Year of Publication2017
AuthorsJoshi, Y., G. M. Tchamgoue, and S. Fischmeister
Conference Name32nd ACM Symposium on Applied Computing (SAC)
Conference LocationMarrakech, Morocco
Abstract

Runtime verification techniques mostly assume the existence of complete execution traces. However, real-world systems often produce lossy traces due to network issues, partial instrumentation, sampling, and logging failures. A few verification techniques have recently emerged to handle systems with incomplete traces. Some of these techniques sacrifice soundness and may produce imprecise verdicts. The others depend on the recovery of lost events for a sound and meaningful verdict. In this paper, we present an offine algorithm that identifies whether an Ltl (Linear Temporal Logic) formula can be soundly monitored in the presence of a transient loss of events in a trace and constructs a monitor accordingly. More, we introduce the concept of monotonicity to express the persistence of the verdicts of a loss-tolerant monitor regardless of the recovery of the lost events.  Our evaluation demonstrates the applicability, effciency and practicality of the technique on common LTL patterns, but also on traces from Google Clusters and MPlayer.

Refereed DesignationRefereed
Related files: 

Opportunities

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