Predictive Runtime Verification of Stochastic Systems

runtime verification;predictive runtime verification;black box system;abstraction;importance sampling;stochastic system;prediction model

Babaee Cheshmeahmadrezaee, Rezaaffiliation1:Faculty of Engineering ; advisor:Rayside, Derek ; advisor:Ganesh, Vijay ; Rayside, Derek ; Ganesh, Vijay ;

University of Waterloo

关键词: stochastic system;    predictive runtime verification;    prediction model;    abstraction;    black box system;    importance sampling;    runtime verification;    Doctoral Thesis;   

Others  :  https://uwspace.uwaterloo.ca/bitstream/10012/14876/5/Babaee_Reza.pdf

瑞士|英语

来源: UWSPACE Waterloo Institutional Repository

【 摘 要 】

Runtime Verification (RV) is the formal analysis of the execution of a system against someproperties at runtime. RV is particularly useful for stochastic systems that have a non-zeroprobability of failure at runtime. The standard RV assumes constructing a monitor thatchecks only the currently observed execution of the system against the given properties.This dissertation proposes a framework for predictive RV, where the monitor insteadchecks the current execution with its finite extensions against some property. The extensions are generated using a prediction model, that is built based on execution samplesrandomly generated from the system. The thesis statement is that predictive RV forstochastic systems is feasible, effective, and useful.The feasibility is demonstrated by providing a framework, called Prevent, that builds apredictive monitor by using trained prediction models to finitely extend an execution path,and computing the probabilities of the extensions that satisfy or violate the given property.The prediction model is trained using statistical learning techniques from independent andidentically distributed samples of system executions. The prediction is the result of aquantitative bounded reachability analysis on the product of the prediction model and theautomaton specifying the property. The analysis results are computed offline and stored ina lookup table. At runtime the monitor obtains the state of the system on the predictionmodel based on the observed execution, directly or by approximation, and uses the lookuptable to retrieve the computed probability that the system at the current state will satisfyor violate the given property within some finite number of steps.The effectiveness of Prevent is shown by applying abstraction when constructing theprediction model. The abstraction is on the observation space based on extracting thesymmetry relation between symbols that have similar probabilities to satisfy a property.The abstraction may introduce nondeterminism in the final model, which is handled byusing a hidden state variable when building the prediction model. We also demonstratethat, under the convergence conditions of the learning algorithms, the prediction resultsfrom the abstract models are the same as the concrete models.Finally, the usefulness of Prevent is indicated in real-world applications by showinghow it can be applied for predicting rare properties, properties with very low but non-zeroprobability of satisfaction. More specifically, we adjust the training algorithm that usesthe samples generated by importance sampling to generate the prediction models for rareproperties without increasing the number of samples and without having a negative impacton the prediction accuracy.