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 Vrevent, 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 lookup table 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 that gives the most probable state. We show an empirical evaluation of Vrevent on a version of randomized dining philosopher and on the QNX Neutrino kernel traces collected from an autopilot software of a hexacopter.