Sign in
Author

Conference

Journal

Organization

Year

DOI
Look for results that meet for the following criteria:
since
equal to
before
between
and
Search in all fields of study
Limit my searches in the following fields of study
Agriculture Science
Arts & Humanities
Biology
Chemistry
Computer Science
Economics & Business
Engineering
Environmental Sciences
Geosciences
Material Science
Mathematics
Medicine
Physics
Social Science
Multidisciplinary
Keywords
(22)
bayesian statistics
Control System
Discrete System
Discrete Time
Error Bound
Fault Tolerant
Hybrid System
Hypothesis Test
Model Checking
Numerical Solution
Optimization Problem
Probabilistic Model Checking
Random Sampling
Satisfiability
Scaling Up
State Space
Statistical Techniques
Statistical Model
Stochastic Model
Stochastic System
System Biology
Temporal Properties
Subscribe
Academic
Publications
Bayesian statistical model checking with application to Simulink/Stateflow verification
Bayesian statistical model checking with application to Simulink/Stateflow verification,10.1145/1755952.1755987,Paolo Zuliani,André Platzer,Edmund M.
Edit
Bayesian statistical model checking with application to Simulink/Stateflow verification
(
Citations: 6
)
BibTex

RIS

RefWorks
Download
Paolo Zuliani
,
André Platzer
,
Edmund M. Clarke
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 nonBayesian 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 discretetime
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 stateoftheart 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.
Conference:
Hybrid Systems
, pp. 243252, 2010
DOI:
10.1145/1755952.1755987
Cumulative
Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
(
portal.acm.org
)
(
portal.acm.org
)
(
www.informatik.unitrier.de
)
(
doi.acm.org
)
More »
Citation Context
(5)
...Thorough static analysis like model checking is expensive and inaccurate [
21
]...
Ruoyu Zhang
,
et al.
Combining Static and Dynamic Analysis to Discover Software Vulnerabili...
...The semantics of BLTL are defined over infinite traces, but it can be shown that traces of an appropriate (finite) length are sufficient to decide BLTL properties [
49
]...
...We have introduced a Bayesian sequential hypothesis testing approach and applied it to the verification of rulebased models of signaling pathways and other stochastic systems [23,
49
]...
...Theorem. [
49
] The error probability for the sequential...
Haijun Gong
,
et al.
Analysis and verification of the HMGB1 signaling pathway
...Clarke et al. [
27
] are using ideas and proposing new algorithms in the SMC area...
Cristiano Bertolini
,
et al.
Calibrating Probabilistic GUI Testing Models Based on Experiments and ...
...Several different forms of combinations of probabilities with hybrid systems and continuous systems have been considered, both for model checking [7,12,3] and for simulationbased validation [18,
28
]...
...Statistical model checking has been suggested for validating stochastic hybrid systems [18] and later refined for discretetime hybrid systems with a probabilistic simulation function [
28
] based on corresponding discrete probabilistic techniques [27]...
...They did not show measurability and do not support stochastic differential equations [
28
]...
...Validation by simulation is generally unsound, but the probability of giving a wrong answer can sometimes be bounded [27,
28
]...
André Platzer
.
Stochastic Differential Dynamic Logic for Stochastic Hybrid Programs
...In the probabilistic verification world, discreteevent simulation is more and more applied as a vehicle in statistical model checking [5,24,
25
]...
Jonathan Bogdoll
,
et al.
Partial Order Methods for Statistical Model Checking and Simulation
References
(23)
Modelchecking for Probabilistic Realtime Systems
(
Citations: 112
)
Rajeev Alur
,
Costas Courcoubetis
,
David L. Dill
Conference:
International Colloquium on Automata, Languages and Programming  ICALP
, 1991
Symbolic Model Checking for Probabilistic Processes
(
Citations: 97
)
Christel Baier
,
Edmund M. Clarke
,
Vasiliki HartonasGarmhausen
,
Mark Ryan
Conference:
International Colloquium on Automata, Languages and Programming  ICALP
, pp. 430440, 1997
ModelChecking Algorithms for ContinuousTime Markov Chains
(
Citations: 253
)
Christel Baier
,
Boudewijn R. Haverkort
,
Holger Hermanns
,
Joostpieter Katoen
Journal:
IEEE Transactions on Software Engineering  TSE
, vol. 29, no. 6, pp. 524541, 2003
On Probabilistic Computation Tree Logic
(
Citations: 27
)
Frank Ciesinskiand
,
Marcus Größer
Conference:
Validation of Stochastic Systems  VOSS
, pp. 147188, 2004
The complexity of probabilistic verification
(
Citations: 247
)
Costas Courcoubetis
,
Mihalis Yannakakis
Journal:
Journal of The ACM  JACM
, vol. 42, no. 4, pp. 857907, 1995
Sort by:
Citations
(6)
Combining Static and Dynamic Analysis to Discover Software Vulnerabilities
Ruoyu Zhang
,
Shiqiu Huang
,
Zhengwei Qi
,
Haibin Guan
Conference:
International Conference on Innovative Mobile and Internet Services in Ubiquitous Computing  IMIS
, 2011
Ant colonies for Temporal Logic falsification of hybrid systems
(
Citations: 1
)
Y. S. R. Annapureddy
,
G. E. Fainekos
Published in 2010.
Analysis and verification of the HMGB1 signaling pathway
(
Citations: 1
)
Haijun Gong
,
Paolo Zuliani
,
Anvesh Komuravelli
,
James R Faeder
,
Edmund M Clarke
Journal:
BMC Bioinformatics
, vol. 11, no. Suppl 7, pp. S1013, 2010
Calibrating Probabilistic GUI Testing Models Based on Experiments and Survival Analysis
Cristiano Bertolini
,
Alexandre Motaand
,
Eduardo Aranha
,
Alexandre Cabral Mota
Conference:
International Symposium on Software Reliability Engineering  ISSRE
, pp. 319328, 2010
Stochastic Differential Dynamic Logic for Stochastic Hybrid Programs
(
Citations: 1
)
André Platzer