如何把网站建设成营销型网站,网站建设基本流程是什么,做外贸网站好还是内贸网站好,海沧区建设局网站作者 | 李建文 华东师范大学软件工程学院博导
版块 | 鉴源论坛 观模 01 模型检查的历史
模型检查是一种起源于20世纪70年代末的形式化验证技术。该技术最初由Edmund M. Clarke、E. Allen Emerson和Joseph Sifakis提出#xff0c;他们因在模型检查领域的贡献而获得了2007年的…作者 | 李建文 华东师范大学软件工程学院博导
版块 | 鉴源论坛 · 观模 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只适用于反例的寻找而不适合证明模型满足安全性质。 图2BMC算法示例图
3.2 Interpolation Model Checking (IMC)
IMC是在BMC的基础上改进来的模型检查算法它不仅可以查找反例也可以证明模型是满足安全性质P的弥补了BMC算法的缺陷。
简要地说在查找反例上IMC和BMC一样都是靠确定从初始状态出发┐P代表的非安全状态是否是k步可达的如果是则找到了反例若不是则继续增大k的值。和BMC不同的是对于每一个步数kIMC都维持了一个初始状态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(i1)中状态S4可以一步转移到非安全状态S6但是集合F(i1)中的其他集合不能转移到S4因此我们把S4从Fi1及其之前的集合中删除删除S4后我们发现集合F(i1)和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(i1)。
若存在某个B(i)其是所有B(j) (j i) 的并集的子集那么模型是安全的。安全性条件生效表明B序列不会再扩大即使继续扩展B序列新的B(i1)中的元素只会是下标更小的B(i)中出现过的元素这意味着初始状态I不可能到达B(0)因此模型是安全的。此时从B0至B(i)的并集构成了一个不变式。如果某一个状态空间F(i)中存在一个状态s此状态属于非安全状态!P则得到一条以I为起点状态s为终点路径这条路径是待验证性质的反例将被返回。
如下图所示我们发现集合B(i1)包含在所有B(j) (j i1) 的并集中因此安全性条件生效B(j) (j i1) 的并集就是我们要找的不变式(安全性证明)。 图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.
