Bayesian statistical model checking with application to Simulink/Stateflow verification

DOI10.1145/1755952.1755987MaRDI QIDQ2985888zbMATH OpenOpenAlexFDO

Authors Paolo Zuliani, André Platzer, Edmund Clarke

Publication date 10 May 2017

Published in Proceedings of the 13th ACM international conference on Hybrid systems: computation and control (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/1755952.1755987

zbMATH Keywords

Bayesian statisticshybrid systemsprobabilistic model checkingstatistical model checkingstochastic systems

Mathematics Subject Classification ID

Bayesian problems; characterization of Bayes procedures (62C10) Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Recommendations

• Bayesian statistical model checking with application to Stateflow/Simulink verification
• Statistical probabilistic model checking with a focus on time-bounded properties
• Computer Aided Verification
• Statistical model checking for cyber-physical systems
• Coupling and importance sampling for statistical model checking

Cites work

• Decentralized Control of Discrete-Event Systems With Bounded or Unbounded Delay Communication
• Discrete-time control for rectangular hybrid automata
• scientific article; zbMATH DE number 1507210 (Why is no real title available?)
• scientific article; zbMATH DE number 1444339 (Why is no real title available?)
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control
• Marked directed graphs
• Partial-order methods for the verification of concurrent systems. An approach to the state-explosion problem
• Stability Analysis of Networked Control Systems Using a Switched Linear Systems Approach
• Unfoldings: A partial-order approach to model checking.
• What's decidable about hybrid automata?

Cited in

(18)

• Statistical model checking
• Bayesian statistical model checking with application to Stateflow/Simulink verification
• Terminal satisfiability in GSTE
• Quantitative verification of implantable cardiac pacemakers over hybrid heart models
• Smoothed model checking for uncertain continuous-time Markov chains
• Self-adaptive statistical model checking approach for CPS
• Statistical Model Checking for Networks of Priced Timed Automata
• Confidence bounds for statistical model checking of probabilistic hybrid systems
• Simulator semantics for system level formal verification
• Sequential schemes for frequentist estimation of properties in statistical model checking
• Multilevel Monte Carlo method for statistical model checking of hybrid systems
• Stochastic differential dynamic logic for stochastic hybrid programs
• Dynamic Bayesian networks for formal verification of structured stochastic processes
• Probabilistic Model Checking for Continuous-Time Markov Chains via Sequential Bayesian Inference
• Statistical model checking of complex robotic systems
• A survey of statistical model checking
• Scalable and reliable stochastic parametric verification with stochastic variational smoothed model checking
• Active and sparse methods in smoothed model checking

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2985888)