Prevent: a Predictive Run-time Verification Framework Using Statistical Learning

TitlePrevent: a Predictive Run-time Verification Framework Using Statistical Learning
Publication TypeConference Paper
Year of Publication2018
AuthorsBabaee, R., A. Gurfinkel, and S. Fischmeister
Conference Name16th International Conference on Software Engineering and Formal Methods
Conference LocationToulouse, France

Run-time Verification (RV) is an essential component of developing cyber-physical systems, where often the actual model of the system is infeasible to obtain or is not available. In the absence of a model, i.e., black-box systems, RV techniques evaluate a property on the execution path of the system and reach a verdict that the current state of the system satisfies or violates a given property.
In this paper, we introduce Prevent, a predictive runtime verification framework, in which if a property is not currently satisfied, the monitor generates the probability based on the finite extensions of the execution path, that satisfy the specification property. We use Hidden Markov Model (HMM) to extend the partially observable paths of the system.  The HMM is trained on a set of iid samples generated by the system.  We then use reachability analysis to construct a tabular monitor that provides the probability that the extended path satisfies or violates the specification from the current state. The current state is estimated at run-time using Viterbi algorithm which gives the most probable state.  We show the empirical evaluation of Prevent on a modified version of randomized dining philosopher and on the QNX Neutrino kernel traces collected from the autopilot software of a hexacopter.

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.