Bayesian statistical model checking with application to Stateflow/Simulink verification

DOI10.1007/s10703-013-0195-3zbMath1291.68273OpenAlexW2168798915MaRDI QIDQ2248081

André Platzer, Paolo Zuliani, Edmund M. Clarke

Publication date: 30 June 2014

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-013-0195-3

zbMATH Keywords

estimationhybrid systemshypothesis testingstochastic systemsprobabilistic verificationstatistical model checking

Mathematics Subject Classification ID

Parametric hypothesis testing (62F03) Point estimation (62F10) Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Related Items (8)

Statistically Sound Verification and Optimization for Complex Systems ⋮ A compositional modelling and verification framework for stochastic hybrid systems ⋮ Data-driven and model-based verification via Bayesian identification and reachability analysis ⋮ On minimising the maximum expected verification time ⋮ Unnamed Item ⋮ Preface to the special issue on probabilistic model checking ⋮ On checking equivalence of simulation scripts ⋮ Monitoring bounded LTL properties using interval analysis

Uses Software

• PRISM
• StateFlow
• BayesDA
• APMC
• INFAMY

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A logic for reasoning about time and reliability
• Abstractions for hybrid systems
• Stochastic hybrid systems. Theory and safety critical applications.
• Statistical probabilistic model checking with a focus on time-bounded properties
• A counterexample-guided abstraction-refinement framework for markov decision processes
• Bayesian statistical model checking with application to Simulink/Stateflow verification
• A Note on the Limiting Relative Efficiency of the Wald Sequential Probability Ratio Test
• Optimal Statistical Decisions
• Some Recent Results in Metric Temporal Logic
• The complexity of probabilistic verification
• Ergodic Control of Switching Diffusions
• Symbolic model checking for probabilistic processes
• Computer Aided Verification
• Validation of Stochastic Systems
• Probability Inequalities for Sums of Bounded Random Variables
• Simulation and the Monte Carlo Method
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• On the Asymptotic Theory of Fixed-Width Sequential Confidence Intervals for the Mean
• Tools and Algorithms for the Construction and Analysis of Systems
• Computer Aided Verification
• Symmetry Reduction for Probabilistic Model Checking
• Sequential Tests of Statistical Hypotheses
• Hybrid Systems: Computation and Control
• Verification, Model Checking, and Abstract Interpretation

This page was built for publication: Bayesian statistical model checking with application to Stateflow/Simulink verification