NDLI: Bayesian statistical model checking with application to Stateflow/Simulink verification

Content Provider	Springer Nature Link
Author	Zuliani, Paolo Platzer, André Clarke, Edmund M.
Copyright Year	2013
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.
Starting Page	338
Ending Page	367
Page Count	30
File Format	PDF
ISSN	09259856
Journal	Formal Methods in System Design
Volume Number	43
Issue Number	2
e-ISSN	15728102
Language	English
Publisher	Springer US
Publisher Date	2013-08-27
Publisher Place	Boston
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Probabilistic verification Hybrid systems Stochastic systems Statistical model checking Hypothesis testing Estimation Circuits and Systems Electrical Engineering Computer-Aided Engineering (CAD, CAE) and Design Software Engineering/Programming and Operating Systems
Content Type	Text
Resource Type	Article
Subject	Theoretical Computer Science Software Hardware and Architecture

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Automatic verification of competitive stochastic systems

Software Model Checking: The VeriSoft Approach

On simulation-based probabilistic model checking of mixed-analog circuits

Model checking for probabilistic timed automata

HySAT: An efficient proof engine for bounded model checking of hybrid systems

Memory model sensitive bytecode verification

Model checking parameterized asynchronous shared-memory systems

Bisimulation conversion and verification procedure for goal-based control systems

Model checking approach to automated planning

Bayesian statistical model checking with application to Stateflow/Simulink verification

Similar Documents

Automatic verification of competitive stochastic systems

Software Model Checking: The VeriSoft Approach

On simulation-based probabilistic model checking of mixed-analog circuits

Model checking for probabilistic timed automata

HySAT: An efficient proof engine for bounded model checking of hybrid systems

Memory model sensitive bytecode verification

Model checking parameterized asynchronous shared-memory systems

Bisimulation conversion and verification procedure for goal-based control systems

Model checking approach to automated planning

Bayesian statistical model checking with application to Stateflow/Simulink verification