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.
Type de document :
Pré-publication, Document de travail
2014
Liste complète des métadonnées

Littérature citée [20 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01087977
Contributeur : Cyrille Jegourel <>
Soumis le : jeudi 27 novembre 2014 - 11:40:08
Dernière modification le : mardi 16 janvier 2018 - 15:54:23
Document(s) archivé(s) le : lundi 2 mars 2015 - 09:20:11

Fichier

tacas2015_submission_145.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

420

Téléchargements de fichiers

143