Bounded model checking using satisfiability solving
Bounded model checking using satisfiability solving
复制标题
DOI：
10.1023/a:1011276507260
复制
发表时间：
2001-07-01
影响因子：
0.8
通讯作者：
Zhu, Y
中科院分区：
文献类型：
--
作者：
Clarke, E;Biere, A;Zhu, Y
短语模型检查是指用于探索转换系统的状态空间以确定其是否遵守其预期行为的规范的算法。这些算法可以以高度自动化的方式执行穷举验证，因此在工业上引起了很大的兴趣。模型检验程序现在已经商业化了。然而，模型检测一直阻碍了状态爆炸问题，这是一个问题，在一个系统中的状态的数量呈指数增长的系统组件的数量。在本教程中，我们首先简要回顾了模型检测的历史，然后重点介绍了将联合收割机模型检测与可满足性求解相结合的最新技术。这些技术被称为有界模型检查，对状态空间进行了非常快速的探索，对于某些类型的问题，似乎比以前的方法提供了很大的性能改进。我们回顾了公共领域和工业设计上的有界模型检查实验，并提出了一种方法，将该技术应用于工业中进行不变性检查。然后，我们总结了这种新技术的优点和缺点，并讨论了未来的研究工作，以扩大其功能。
The phrase model checking refers to algorithms for exploring the state space of a transition system to determine if it obeys a specification of its intended behavior. These algorithms can perform exhaustive verification in a highly automatic manner, and, thus, have attracted much interest in industry. Model checking programs are now being commercially marketed. However, model checking has been held back by the state explosion problem, which is the problem that the number of states in a system grows exponentially in the number of system components. Much research has been devoted to ameliorating this problem.In this tutorial, we first give a brief overview of the history of model checking to date, and then focus on recent techniques that combine model checking with satisfiability solving. These techniques, known as bounded model checking, do a very fast exploration of the state space, and for some types of problems seem to offer large performance improvements over previous approaches. We review experiments with bounded model checking on both public domain and industrial designs, and propose a methodology for applying the technique in industry for invariance checking. We then summarize the pros and cons of this new technology and discuss future research efforts to extend its capabilities.