Bayesian statistical model checking with application to Simulink/Stateflow verification

@INPROCEEDINGS{DBLP:conf/hybrid/ZulianiPC10,
	pdf = {pub/bayesmcest.pdf},
	slides = {pub/bayesmcest-slides.pdf},
	TR = {DBLP:conf/hybrid/ZulianiPC10:TR},

  author    = {Paolo Zuliani and
               Andr{\'e} Platzer and
               Edmund M. Clarke},
  title     = {Bayesian Statistical Model Checking with
               Application to {Simulink/Stateflow}
               Verification},
  booktitle = {HSCC},
  year      = {2010},
  pages     = {243-252},
  doi       = {10.1145/1755952.1755987},
  editor    = {Karl Henrik Johansson and
               Wang Yi},
  longbooktitle = {Proceedings of the 13th ACM
               International Conference on
               Hybrid Systems: Computation and Control,
               HSCC 2010, Stockholm,
               Sweden, April 12-15, 2010},
  publisher = {ACM},
  isbn      = {978-1-60558-955-8},
  abstract  = {
    We address the problem of model checking stochastic
    systems, i.e. checking whether a stochastic system
    satisfies a certain temporal property with a
    probability greater (or smaller) than a fixed
    threshold. In particular, we present a novel
    Statistical Model Checking (SMC) approach based on
    Bayesian statistics. We show that our approach is
    feasible for hybrid systems with stochastic
    transitions, a generalization of Simulink/Stateflow
    models. Standard approaches to stochastic (discrete)
    systems require numerical solutions for large
    optimization problems and quickly become infeasible
    with larger state spaces. Generalizations of these
    techniques to hybrid systems with stochastic effects
    are even more challenging. The SMC approach was
    pioneered by Younes and Simmons in the discrete and
    non-Bayesian case. It solves the verification problem
    by combining randomized sampling of system traces
    (which is very efficient for Simulink/Stateflow) with
    hypothesis testing or estimation. We believe SMC is
    essential for scaling up to large Stateflow/Simulink
    models. While the answer to the verification problem is
    not guaranteed to be correct, we prove that Bayesian
    SMC can make the probability of giving a wrong answer
    arbitrarily small. The advantage is that answers can
    usually be obtained much faster than with standard,
    exhaustive model checking techniques. We apply our
    Bayesian SMC approach to a representative example of
    stochastic discrete-time hybrid system models in
    Stateflow/Simulink: a fuel control system featuring
    hybrid behavior and fault tolerance. We show that our
    technique enables faster verification than
    state-of-the-art statistical techniques, while
    retaining the same error bounds. We emphasize that
    Bayesian SMC is by no means restricted to
    Stateflow/Simulink models: we have in fact successfully
    applied it to very large stochastic models from Systems
    Biology.}
}```