期刊
ACM TRANSACTIONS ON MODELING AND COMPUTER SIMULATION
卷 28, 期 1, 页码 -出版社
ASSOC COMPUTING MACHINERY
DOI: 10.1145/3158668
关键词
Statistical model checking; hypothesis testing; temporal logic; simulation; estimation
资金
- National Science Foundation [NSF CCF 14-38982, NSF CCF 16-17401]
- AFOSR/AFRL Air Force Research Laboratory and the Air Force Office of Scientific Research for the Assured Cloud Computing at the University of Illinois at Urbana-Champaign [FA8750-11-2-0084]
- Direct For Computer & Info Scie & Enginr [1617401, 1438982] Funding Source: National Science Foundation
- Division of Computing and Communication Foundations [1438969] Funding Source: National Science Foundation
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.
作者
我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。
推荐
暂无数据