TY - GEN
T1 - Feedback control for statistical model checking of cyber-physical systems
AU - Kalajdzic, K.
AU - Jegourel, C.
AU - Lukina, A.
AU - Bartocci, E.
AU - Legay, A.
AU - Smolka, S. A.
AU - Grosu, R.
N1 - Publisher Copyright:
© Springer International Publishing AG 2016.
PY - 2016
Y1 - 2016
N2 - We introduce feedback-control statistical system checking (FC-SSC), a new approach to statistical model checking that exploits principles of feedback-control for the analysis of cyber-physical systems (CPS). FC-SSC uses stochastic system identification to learn a CPS model, importance 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 applications or in any complex probabilistic program whose model is either not available, or is infeasible to derive through static-analysis techniques.
AB - We introduce feedback-control statistical system checking (FC-SSC), a new approach to statistical model checking that exploits principles of feedback-control for the analysis of cyber-physical systems (CPS). FC-SSC uses stochastic system identification to learn a CPS model, importance 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 applications or in any complex probabilistic program whose model is either not available, or is infeasible to derive through static-analysis techniques.
UR - https://www.scopus.com/pages/publications/84994019270
U2 - 10.1007/978-3-319-47166-2_4
DO - 10.1007/978-3-319-47166-2_4
M3 - Conference contribution
AN - SCOPUS:84994019270
SN - 9783319471655
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 46
EP - 61
BT - Leveraging Applications of Formal Methods, Verification and Validation
A2 - Margaria, Tiziana
A2 - Steffen, Bernhard
PB - Springer Verlag
T2 - 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2016
Y2 - 10 October 2016 through 14 October 2016
ER -