Bayesian statistical model checking with application to Simulink/Stateflow verification

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.

@inproceedings{DBLP:conf/hybrid/ZulianiPC10,
	pdf = {pub/bayesmcest.pdf},
	slides = {pub/bayesmcest-slides.pdf},
	TR = {DBLP:conf/hybrid/ZulianiPC10:TR},
	author = {['Paolo Zuliani', 'André Platzer', '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', '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.}
}