Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

Model Checking as Control: Feedback Control for Statistical Model Checking of Cyber-Physical Systems

Abstract : We introduce feedback-control statistical system checking (FC-SSC), a new approach to statistical model checking that exploits princi-ples of feedback-control for the analysis of cyber-physical systems (CPS). FC-SSC uses stochastic system identification to learn a CPS model, im-portance sampling to estimate the CPS state, and importance splitting to control the CPS so that the probability that the CPS satisfies a given property can be efficiently inferred. We illustrate the utility of FC-SSC on two example applications, each of which is simple enough to be easily understood, yet complex enough to exhibit all of FC-SCC's features. To the best of our knowledge, FC-SSC is the first statistical system checker to efficiently estimate the probability of rare events in realistic CPS ap-plications or in any complex probabilistic program whose model is either not available, or is infeasible to derive through static-analysis techniques.
Document type :
Preprints, Working Papers, ...
Complete list of metadatas

Cited literature [20 references]  Display  Hide  Download

https://hal.inria.fr/hal-01087977
Contributor : Cyrille Jegourel <>
Submitted on : Thursday, November 27, 2014 - 11:40:08 AM
Last modification on : Friday, July 10, 2020 - 4:26:20 PM
Document(s) archivé(s) le : Monday, March 2, 2015 - 9:20:11 AM

File

tacas2015_submission_145.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01087977, version 1

Citation

K Kalajdzic, Cyrille Jegourel, E Bartocci, Axel Legay, Scott Smolka, et al.. Model Checking as Control: Feedback Control for Statistical Model Checking of Cyber-Physical Systems. 2014. ⟨hal-01087977⟩

Share

Metrics

Record views

540

Files downloads

268