TY - JOUR
T1 - A survey of statistical model checking
AU - Agha, Gul
AU - Palmskog, Karl
N1 - Funding Information:
This work is supported by the National Science Foundation, under Grants No. NSF CCF 14-38982 and No. NSF CCF 16-17401, and by AFOSR/AFRL Air Force Research Laboratory and the Air Force Office of Scientific Research under Agreement No. FA8750-11-2-0084 for the Assured Cloud Computing at the University of Illinois at Urbana-Champaign. Authors’ addresses: G. Agha and K. Palmskog, University of Illinois at Urbana-Champaign, Department of Computer Science, Urbana, IL, 61801; emails: {agha, palmskog}@illinois.edu. Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from permissions@acm.org. © 2018 ACM 1049-3301/2018/01-ART6 $15.00 https://doi.org/10.1145/3158668
Funding Information:
This work is supported by the National Science Foundation, under Grants No. NSF CCF 14-38982 and No. NSF CCF 16-17401, and by AFOSR/AFRL Air Force Research Laboratory and the Air Force Office of Scientific Research under Agreement No. FA8750-11-2-0084 for the Assured Cloud Computing at the University of Illinois at Urbana-Champaign.
Publisher Copyright:
© 2018 ACM.
PY - 2018/1
Y1 - 2018/1
N2 - Interactive, distributed, and embedded systems often behave stochastically, for example, when inputs, message delays, or failures conform to a probability distribution. However, reasoning analytically about the behavior of complex stochastic systems is generally infeasible. While simulations of systems are commonly used in engineering practice, they have not traditionally been used to reason about formal specifications. Statistical model checking (SMC) addresses this weakness by using a simulation-based approach to reason about precise properties specified in a stochastic temporal logic. A specification for a communication system May state that within some time bound, the probability that the number of messages in a queue will be greater than 5 must be less than 0.01. Using SMC, executions of a stochastic system are first sampled, after which statistical techniques are applied to determine whether such a property holds. While the output of sample-based methods are not always correct, statistical inference can quantify the confidence in the result produced. In effect, SMC provides a more widely applicable and scalable alternative to analysis of properties of stochastic systems using numerical and symbolic methods. SMC techniques have been successfully applied to analyze systems with large state spaces in areas such as computer networking, security, and systems biology. In this article, we survey SMC algorithms, techniques, and tools, while emphasizing current limitations and tradeoffs between precision and scalability.
AB - Interactive, distributed, and embedded systems often behave stochastically, for example, when inputs, message delays, or failures conform to a probability distribution. However, reasoning analytically about the behavior of complex stochastic systems is generally infeasible. While simulations of systems are commonly used in engineering practice, they have not traditionally been used to reason about formal specifications. Statistical model checking (SMC) addresses this weakness by using a simulation-based approach to reason about precise properties specified in a stochastic temporal logic. A specification for a communication system May state that within some time bound, the probability that the number of messages in a queue will be greater than 5 must be less than 0.01. Using SMC, executions of a stochastic system are first sampled, after which statistical techniques are applied to determine whether such a property holds. While the output of sample-based methods are not always correct, statistical inference can quantify the confidence in the result produced. In effect, SMC provides a more widely applicable and scalable alternative to analysis of properties of stochastic systems using numerical and symbolic methods. SMC techniques have been successfully applied to analyze systems with large state spaces in areas such as computer networking, security, and systems biology. In this article, we survey SMC algorithms, techniques, and tools, while emphasizing current limitations and tradeoffs between precision and scalability.
KW - Estimation
KW - Hypothesis testing
KW - Simulation
KW - Statistical model checking
KW - Temporal logic
UR - http://www.scopus.com/inward/record.url?scp=85042465606&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85042465606&partnerID=8YFLogxK
U2 - 10.1145/3158668
DO - 10.1145/3158668
M3 - Review article
AN - SCOPUS:85042465606
VL - 28
JO - ACM Transactions on Modeling and Computer Simulation
JF - ACM Transactions on Modeling and Computer Simulation
SN - 1049-3301
IS - 1
M1 - 6
ER -