Abstract
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.
| Original language | English (US) |
|---|---|
| Article number | 6 |
| Journal | ACM Transactions on Modeling and Computer Simulation |
| Volume | 28 |
| Issue number | 1 |
| DOIs | |
| State | Published - Jan 2018 |
Fingerprint
Keywords
- Estimation
- Hypothesis testing
- Simulation
- Statistical model checking
- Temporal logic
ASJC Scopus subject areas
- Modeling and Simulation
- Computer Science Applications
Cite this
A survey of statistical model checking. / Agha, Gul A; Palmskog, Karl.
In: ACM Transactions on Modeling and Computer Simulation, Vol. 28, No. 1, 6, 01.2018.Research output: Contribution to journal › Review article
}
TY - JOUR
T1 - A survey of statistical model checking
AU - Agha, Gul A
AU - Palmskog, Karl
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 -