Bayesian statistical model checking with application to Simulink/Stateflow verification

@article{DBLP:journals/fmsd/ZulianiPC13,
	pdf = {pub/bayesmcest-FMSD.pdf},
	author = {['Paolo Zuliani', 'André Platzer', 'Edmund M. Clarke']},
	title = {Bayesian Statistical Model Checking with
               Application to Simulink/Stateflow
               Verification},
	journal = {Formal Methods in System Design},
	volume = {43},
	number = {2},
	year = {2013},
	pages = {338-367},
	doi = {10.1007/s10703-013-0195-3},
	issn = {0925-9856},
	keywords = {Probabilistic verification, Hybrid systems,
               Stochastic systems, Statistical model
               checking, Hypothesis testing, Estimation},
	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 Statistical Model Checking (SMC) approach based
        on Bayesian statistics. We show that our approach
        is feasible for a certain class of 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 (i.e.,
        testing against a probability threshold) or
        estimation (i.e., computing with high probability
        a value close to the true probability). 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. We emphasize that Bayesian SMC is by
        no means restricted to Stateflow/Simulink models.
        It is in principle applicable to a variety of
        stochastic models from other domains, e.g.,
        systems biology.
  }
}