A Survey of Statistical Model Checking
A Survey of Statistical Model Checking
复制标题
DOI：
10.1145/3158668
复制
发表时间：
2018-01-01
影响因子：
0.9
通讯作者：
Palmskog, Karl
中科院分区：
文献类型：
--
作者：
Agha, Gul;Palmskog, Karl
交互式、分布式和嵌入式系统的行为通常是随机的，例如，当输入、消息延迟或故障符合概率分布时。然而，对复杂随机系统的行为进行解析推理通常是不可行的。虽然系统仿真在工程实践中经常使用，但它们传统上并没有被用来推理形式规范。统计模型检测(SMC)通过使用基于模拟的方法来对随机时序逻辑中指定的精确属性进行推理来解决这一弱点。通信系统的规范可以规定，在某个时间范围内，队列中的消息数量将大于5的概率必须小于0.01。使用SMC，首先对随机系统的执行进行抽样，然后应用统计技术来确定这种性质是否成立。虽然基于样本的方法的输出并不总是正确的，但统计推断可以量化对所产生结果的置信度。实际上，SMC为使用数值和符号方法分析随机系统的性质提供了一种更广泛的适用性和可扩展性的替代方案。SMC技术已经成功地应用于计算机网络、安全和系统生物学等领域中具有大状态空间的系统分析。在本文中，我们概述了SMC算法、技术和工具，同时强调了当前的限制和精度与可伸缩性之间的权衡。
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.