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

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.