A survey of statistical model checking

Gul A Agha, Karl Palmskog

Research output: Contribution to journalReview article

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 languageEnglish (US)
Article number6
JournalACM Transactions on Modeling and Computer Simulation
Volume28
Issue number1
DOIs
StatePublished - Jan 2018

Fingerprint

Model checking
Model Checking
Statistical Model
Stochastic systems
Stochastic Systems
Symbolic Methods
Temporal logic
Interactive Systems
Formal Specification
Systems Biology
Temporal Logic
Statistical Inference
Networking
Embedded systems
Embedded Systems
Probability distributions
Communication Systems
Confidence
Queue
Scalability

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 journalReview article

@article{add13b6f58ae4170a7eb05df4ade9485,
title = "A survey of statistical model checking",
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.",
keywords = "Estimation, Hypothesis testing, Simulation, Statistical model checking, Temporal logic",
author = "Agha, {Gul A} and Karl Palmskog",
year = "2018",
month = "1",
doi = "10.1145/3158668",
language = "English (US)",
volume = "28",
journal = "ACM Transactions on Modeling and Computer Simulation",
issn = "1049-3301",
publisher = "Association for Computing Machinery (ACM)",
number = "1",

}

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 -