Model Checking as Control: Feedback Control for Statistical Model Checking of Cyber-Physical Systems
(2014)
Files
No attached file found for this publication.
Details
- Authors
- 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.
Citations
Kalajdzic, K., Jegourel, C., Bartocci, E., Legay, A., Smolka, S., & Grosu, R. (2014). Model Checking as Control: Feedback Control for Statistical Model Checking of Cyber-Physical Systems. https://hdl.handle.net/2078.5/172999