01 模型检查的历史

模型检查是一种起源于20世纪70年代末的形式化验证技术。该技术最初由Edmund M. Clarke、E. Allen Emerson和Joseph Sifakis提出，他们因在模型检查领域的贡献而获得了2007年的图灵奖。模型检查的提出最初是为了对并发和分布式系统做自动化验证，这些系统越来越复杂，手动验证则变得越来越困难。模型检查涉及系统地探索系统的所有可能状态，并检查每个状态是否满足某些属性。

在早期阶段，模型检查可以通过显示地计算Kripke结构上的不动点(针对CTL描述的性质) [1]或者是在由模型和LTL性质构造的乘积自动机上做状态搜索 [2]来完成。尽管这些技术非常直观且易于理解，但它们处理大型系统的能力非常有限，现在它们已经被以BDD [3]和SAT求解器 [4]为计算核心的符号模型检查技术所取代。事实上，基于SAT求解器的模型检查技术是目前最有前景的自动化验证技术。目前最先进的基于SAT求解器的模型检查技术包括BMC [5]，IMC [6]，IC3/PDR [7]，和CAR [8]。

模型检查已被应用于各种系统，包括硬件电路、通信协议、操作系统和软件程序。它已被用于在部署之前检测系统中的错误和缺陷，这可以在开发过程中节省时间和金钱。今天，模型检查是一个活跃的研究和开发领域，研究人员正在不断努力，以提高其拓展性、准确性和可用性。

02 模型检查问题描述

模型检查问题是说：给定一个模型M，或者说一个状态迁移系统，如何判断M是否满足安全性质P。在具体算法实现中，我们往往是从初始状态I出发，判断┐P代表的状态是否可达，即是否所有I可达的状态都是满足安全性质P的。如果我们在算法中找到了反例，即从I出发，经过一系列状态，可以到达┐P，则我们返回反例，用以说明安全性质P不成立；如果我们找到了一个不变式，即证明了从I出发，所有可达的范围都在一个满足P的状态集合中，则我们返回验证通过，安全性质P成立。下面我们先简要介绍几个常见的模型检查算法。

图1 模型检查问题示例图

03 模型检查算法介绍

3.1 Bounded Model Checking (BMC)

BMC是一个简单但是高效的模型检查算法，类似于图搜索中的广度优先搜索。BMC从初始状态出发，先判断是否可以直接一步转移到┐P，也就是不安全的状态中，若可以，则找出了一个长度为1的反例；若不行，则说明在初始状态一步的范围内，安全性质成立，接着，BMC增大步数，判定从初始状态出发，是否可以两步转移到┐P，同样地，若可达则返回反例，若不可达，则继续增大步数，直到找到反例或者达到限定的时间为止。

如下图所示，从S0出发，先确定一步可达的S1和S2满足性质，接着增大步数，确定两步可达的S3满足性质，再确定三步可达的S4和S5满足性质，最终步数为4时，检查出四步可达的S6不满足性质，从而得到反例。

使用BMC算法可以很快地找到长度最短的反例，但是它的局限性也很大，假设BMC在k步之内找不到反例，这只能说明初始状态k步可达的状态满足安全性质，而不能证明初始状态可达的状态都是满足安全性质的，也就是说，BMC只适用于反例的寻找，而不适合证明模型满足安全性质。

图2：BMC算法示例图

3.2 Interpolation Model Checking (IMC)

IMC是在BMC的基础上改进来的模型检查算法，它不仅可以查找反例，也可以证明模型是满足安全性质P的，弥补了BMC算法的缺陷。

简要地说，在查找反例上，IMC和BMC一样，都是靠确定从初始状态出发，┐P代表的非安全状态是否是k步可达的，如果是，则找到了反例，若不是，则继续增大k的值。和BMC不同的是，对于每一个步数k，IMC都维持了一个初始状态k步之内可达的状态的超集R，即R里面也包含了一些其他的状态，且R里面的元素都满足安全性质，在寻找反例的过程中，IMC不断扩大集合R，若在某个时刻，R不能被扩大，即R里面的元素只能转移到R里面，则我们找到了一个不变式，即证明了从初始状态出发，可达的所有状态都是满足安全性质的，从而证明了模型是满足安全性质P的。

如下图所示，从初始状态S0出发，我们找到了一个状态集合R，使得S0可达的状态S1、S2和S3都在集合R中，且R中的元素都满足安全性质，因此我们证明了模型是满足安全性质的，集合R就是证据。

图3 IMC算法示例图

3.3 Property Directed Reachability (PDR)

PDR是一个较为复杂的模型检查算法，简要地说，它维持了一个满足安全性质P的状态集合的序列F，其中F(0)是初始状态I，而F(1)则是初始状态一步之内可达的集合的超集，即它里面除了有初始状态一步之内可达的状态，也包含了一些其他的状态，以此类推，后面每一个F(i)集合都是前一个F(i-1)集合的一步之内可达的集合的超集，PDR算法不断地在F(i)集合中寻找那些可以一步转移到┐P的元素S，若F(i)中的其他元素可以一步转移到S，则PDR接着判断F(i-1)中的元素可不可以两步转移到S，以此类推，若在F(0)，即初始状态中，有元素可以多步转移到S，则找到了一个反例，即性质P不成立，如果在这个过程中，我们找到一个F(i)集合，使得它里面的元素都不能转移到S，则我们可以把S从这个集合及它之前的集合中删除，我们不断重复这个过程，如果在某一步，存在某个F(i)使得F(i)=F(i-1)，即F(i-1)里面的状态只能转移到F(i-1)里面时，我们就找到了一个不变式，即所有初始状态可达的状态都满足了性质P，证明了性质P成立。

如下图所示，在集合F(i+1)中，状态S4可以一步转移到非安全状态S6，但是集合F(i+1)中的其他集合不能转移到S4，因此我们把S4从Fi+1及其之前的集合中删除，删除S4后，我们发现集合F(i+1)和F(i)相等，即此时F(i)里面的状态只能转移到F(i)里面，因为F(i)是初始状态可达的状态的超集，从而初始状态可达的元素都在F(i)中，因此模型的安全性质就得到了满足，F(i)就是证据。

图4 PDR算法示例图

3.4 Complementary Approximate Reachability (CAR)

CAR算法也是一个较为复杂的模型检查算法，可以有两个搜索方向（Forward CAR和Backward CAR），后续我们以Backward CAR为例。CAR维护了两个序列，B序列和F序列，F序列是从初始状态I出发可达的状态的子集的集合，B序列则是可以到达非安全状态的!P的状态的超集的集合，且F(0)= I , B(0)= !P。维护子集与超集的原因是F序列和B序列都是动态的，Fi的元素会随着算法运行不断增多，子集会越来越接近原集。而B(i)的元素则会不断减少，超集也会越来越接近原集。CAR算法就是不断地去做类似的SAT调用，然后根据结果去更新F和B序列。例如CAR算法会不断地通过SAT来判断某个状态s能否一步转移到B(i)，若成立，则可以拿到s的一个后继状态s'并把其加入到F序列，随后CAR则递归询问s'是否可以转移到B(i-1)；若不成立，CAR则会拿到一个uc(最小不满足核)，并把这个uc来更新B(i+1)。

若存在某个B(i)，其是所有B(j) (j < i) 的并集的子集，那么模型是安全的。安全性条件生效表明B序列不会再扩大，即使继续扩展B序列，新的B(i+1)中的元素，只会是下标更小的B(i)中出现过的元素，这意味着初始状态I不可能到达B(0)，因此模型是安全的。此时从B0至B(i)的并集构成了一个不变式。如果某一个状态空间F(i)中，存在一个状态s，此状态属于非安全状态!P，则得到一条以I为起点，状态s为终点路径，这条路径是待验证性质的反例，将被返回。

如下图所示，我们发现集合B(i+1)包含在所有B(j) (j < i+1) 的并集中，因此安全性条件生效，B(j) (j < i+1) 的并集就是我们要找的不变式(安全性证明)。

图5 CAR算法示例图

参考文献：

[1] E. Clarke and H. Schlingloff, “Model checking,” in Handbook of Automated Reasoning, A. Robinson and A. Voronkov, Eds. MIT Press, 2001, pp. 1635–1790.

[2] O. Kupferman, N. Piterman, and M. Y. Vardi, “An automata-theoretic approach to infinite-state systems,” in Time for Verification: Essays in Memory of Amir Pnueli, Z. Manna and D. A. Peled, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2010, pp. 202–259.

[3] K. L. McMillan, Symbolic Model Checking. Boston, MA: Springer US, 1993.

[4] Y. Vizel, G. Weissenbacher, and S. Malik, “Boolean satisfiability solvers and their applications in model checking,” Proceedings of the IEEE, vol.103, no. 11, pp. 2021–2035, 2015.

[5] A. Biere, A. Cimatti, E. Clarke, and Y. Zhu, “Symbolic model checking without BDDs,” in Tools and Algorithms for the Construction and Analysis of Systems (TACAS), W. R. Cleaveland, Ed. Berlin, Heidelberg: Springer Berlin Heidelberg, 1999, pp. 193–207.

[6] K. L. McMillan, “Interpolation and SAT-based model checking,” in Computer Aided Verification, W. A. Hunt and F. Somenzi, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2003, pp. 1–13.

[7] A. R. Bradley, “SAT-based model checking without unrolling,” in Verification, Model Checking, and Abstract Interpretation, R. Jhala and D. Schmidt, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2011, pp. 70–87.

[8] J. Li, R. Dureja, G. Pu, K. Y. Rozier, and M. Y. Vardi, “Simplecar: An efficient bug-finding tool based on approximate reachability,” in Computer Aided Verification, H. Chockler and G. Weissenbacher, Eds. Cham: Springer International Publishing, 2018, pp. 37–44.