### 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

*ACM Transactions on Modeling and Computer Simulation*,

*28*(1), [6]. https://doi.org/10.1145/3158668

**A survey of statistical model checking.** / Agha, Gul A; Palmskog, Karl.

Research output: Contribution to journal › Review article

*ACM Transactions on Modeling and Computer Simulation*, vol. 28, no. 1, 6. https://doi.org/10.1145/3158668

}

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 -