有界模型检验综述

于露

摘要：无论是计算机系统硬件设计还是软件设计，随着设计规模越来越复杂和庞大，会产生越来越多的设计缺陷。传统检测方法代价高，并且难以检测这些设计缺陷。有界模型检验是一种重要的形式化验证方法，可以大大提高检测、验证的效率。作为一种形式化方法构造系统的模拟运行过程，有界模型检验通过把有限状态机和线性时序逻辑验证规范否定形式编码成布尔可满足性实例，再由各种布尔可满足性工具来求解，以获得反例。由于有界模型检验使用深度优先搜索，它可以很快找到路径最短的反例。

关键词：有界模型检验；模型检验；SAT

中图分类号：TP311 文献标识码：A 文章编号：1009-3044（2017）35-0070-02

1 有界模型检验的概念

模型检测（model checking）是形式化验证方法的一种，它可以自动检测系统的模拟运行是否满足某些期望的规范。随着计算机系统越来越复杂，网络应用越来越普及和重要，通过模型检测技术来验证系统和网络的安全性和正确性的应用也逐渐增多。针对前期的OBDD（ordered binary decision diagram）技术的模型检测的不足，有界模型检测（bounded model checking，简称BMC）使用SAT（satisfiability）求解器来求解

需要验证的问题。BMC通过设置界限阈值k，可以有效地克服状态爆炸问题，并可以解决逻辑公式相对应的BDD（binary decision diagram）结构的存储空间、检测变量少等问题[1]。BMC有两个主要的优势：其优势之一是充分利用SAT（satisfiability）求解工具的特征，把BMC 问题编码成SAT实例，有效地使模型检验的变量数提升一个数量级以上；另一优势是BMC的求解过程向着不满足命题的方向发展，有利于得到长度最短、最简明的反例，方便设计者理解问题，找出原因。实验验证，当边界阈值的上界k小于60时，BMC优于传统的模型检测[2]。

2 有界模型检验的过程

有界模型检测的主要过程是：使用有限状态自动机（finite state machine，FSM）来表示要验证的模型或系统，通过FSM状态间的转移来模拟系统或模型运行；用线性时序逻辑（linear-time temporal logic，LTL）来描述有限状态自动机；设定边界阈值k；FSM 状态间的转移关系和LTL逻辑规范使用逻辑与来构成BMC转换公式；把BMC转换公式编码成SAT实例，借助SAT工具求解。若有解，则产生反例反之，若无解，则系统一直运行到阈值k阶段后停止，说明系统或模型是安全且没有错误的。

2.1 Kripke结构

有限状态机可以被表示成kripke结构。

Kripke结构由状态集、状态之间的转移关系、每个状态上使一组原子命题为真的集合组成[3]。它的定义为：

定义一：设AP是一组原子命题，AP上的一个Kripke结构M定义为四元组M=（S，S0，R，L），其中：

1） S是一个有限状态集合；

2） S0 ? S 是初始状态集合；

3） R ? S×S 是转移关系，要求是完全的，即对?s∈S都存在一个状态?s‘∈S，使得（s，s）∈R成立；

4） L：S→2AP是一个函数，标记每个状态使某些原子命题为真的函数。

在Kripke结构中，从一个状态s开始的一条路径是一个无限状态序列，π=s0s1…，其中s0=s且R（si，si+1）对所有i≥0成立。

Kripke结构是一种数学结构，目前在模型检验上是用比较多，可以表示为状态图。它可以用命题语句来表示状态之间的转移关系。使用Kripke结构来进行证明的优势是：

1） 可以反映程序执行的状态；

2） 程序的执行过程可以由状态图来表示。

2.2 线性时序逻辑

线性时序逻辑是经典逻辑的延伸，它继承了布尔变量和布尔操作，类如﹁非运算、∧与运算、→条件运算等。除了布尔连接符，LTL还有如下时序修饰符：

1） X（next）：下一个；

2） G（globally）：总是；

3） F（future）：未来；

4） U（until）：直到；

5） R（release）：释放。

线性时序逻辑将有限状态机各个状态之间的逻辑用符号表示出来。BMC通过对各个状态的布尔值进行對比，来判断是否满足属性。

2.3 属性的分类

BMC的属性分为两种：安全属性和活力属性[4]。前者声明什么状态不应该发生，换句话说也就是什么状态应该发生；后者声明什么状态最终应该发生。安全属性的反例为一个状态踪迹，这个踪迹的最后一个状态不满足于属性。活力属性的反例为一个指向循环的路径，这个无限循环不包含应有的状态，它永远无法到达特定的状态。

3 有界模型检验的应用

近年来，作为国内外研究的热点，BMC虽然发展迅速，但由于发展时间短，目前尚有很多不完善之处。对于BMC的不足之处，学术界主要从三个方面提高它的性能[5]。一、优化BMC的转换公式；二、在编码时，优化SAT实例变量的字句；三、将BMC问题转化为SAT实例后，根据SAT子句的特点，优化SAT工具，从而提高SAT求解效率。

BMC不仅广泛应用于系统安全、硬件设计、系统性能分析等领域，还被应用于Web服务、实时调度和构建技术等方面。其中，黄蔚等人将其用于C/C++程序内存泄漏检测方案[6]。骆翔宇等人利用有界模型检验对多智体系统的时态认知的逻辑进行同步[7]。郝身刚等人使用有界模型检验对大规模服务进行建模，来解决传统的服务组合技术灵活性差并且服务规模有限的问题[8]。

4 结束语

作为一种形式化的模型检验方法，BMC可以提高验证的效率，同时也存在着很多问题。未来在软件和硬件的形式化验证领域，BMC仍然是一个热点。

参考文献：

[1] 侯刚， 周宽久， 勇嘉伟， 等. 模型检测中状态爆炸问题研究综述[J]. 计算机科学， 2013， 40（6a）：77-86.

[2] 杨晋吉. 基于SAT的有界模型检测及其应用研究[D]. 广州： 中山大学， 2008.

[3] 郭建， 韩俊刚. 基于不完全Kripke结构三值逻辑的模型检验[J]. 计算机科学， 2006， 33（3）：263-266.

[4] Biere A， Cimatti A， Clarke E M， et al. Bounded Model Checking[C]// Advances in Computers. DBLP， 2003：117-148.

[5] 杨晋吉， 苏开乐， 骆翔宇， 等. 有界模型检测的优化[J]. 软件学报， 2009， 20（8）：2005-2014.

[6] 黄蔚， 洪玫， 杨秋辉， 等. 基于有界模型检测的C/C++程序内存泄露检测[J]. 计算机应用研究， 2016， 33（6）：1762-1766.

[7] 骆翔宇， 苏开乐， 杨晋吉， 等. 有界模型检测同步多智体系统的时态认知逻辑[J]. 软件学报， 2006， 17（12）：2485-2498.

[8] 郝身刚， 张丽. 有界模型检测在服务组合中的应用研究[J]. 计算机工程与应用， 2012， 48（10）：111-114.