一种基于编码的OBDD模型检测的算法实现＊

马晓龙 顾滨兵 刘鑫淼

（91404部队 秦皇岛 066000）

1 引言

模型检测是一种被广泛使用的验证有限状态系统满足规范的自动化技术，它将形式化规范描述成命题时态逻辑包括LTL（线性时态逻辑）和CTL（分支时态逻辑）等，将系统（如电路设计、协议）模型化为状态转换系统，使用高效的搜索算法来判定规范是否在系统中成立［1～4］。

随着被验证系统规模的不断增大，状态爆炸的问题在一定程度上制约时态逻辑模型检测的进一步发展，而有序二值判定图（Ordered Binary Decision Diagrams）OBDD的使用，使基于 CTL及LTL的符号化模型检测方法得到了极大突破，使验证规模有了明显提高。虽然关于OBDD模型检测方法的资料很多，但是国内很少有关于OBDD模型检测具体实现算法的介绍，本文将在由作者自行开发的 MC＿OBDD v1.0的基础上介绍OBDD模型检测工具的具体实现。

2 模型检测与OBDD

模型检测的基本思想是用状态迁移系统（S）如Kripke结构表示系统的行为，用模态／时序逻辑公式（F）如时序逻辑表达式CTL［1］描述系统的性质。这样“系统是否具有所期望的性质”就转化为数学问题“状态迁移系统S是否是公式F的一个模型”，用公式表示为S｜＝F［4～5］。模型检测的一般流程如图1所示。

BDD［1，6～7］是 Bryant在1986年提出的一种基于图形的二叉判定图，是表示和操作布尔函数的有力工具。OBDD是化简后的BDD。用OBDD验证分为三步：首先用表示状态集合，然后用OBDD表示转移关系，最后计算可达状态。随着基于OBDD表示的高效查找技术的发展，OBDD被应用到知识表达和推理领域特别是符号化模型检测领域中取得了很好的效果。

图1 模型检测的一般流程

3 微波炉验证实例

下面介绍一个常用的模型检测实例，运用这个实例介绍OBDD模型检测的基本思路和方法，并使用自己开发的模型检测器MC＿OBDD对其进行了验证。

对一个微波炉工作的控制软件，从系统建模开始说明它的验证过程。

微波炉的模型如图2所示。

图2 微波炉状态转换模型

上面的模型我们可以表示为M＝（S，S0，R，L，F）。要验证属性用CTL公式表示，本例验证：公式AG（start→AFheat）是否满足M。

4 OBDD模型检测的关键技术

4.1 二叉判定图BDD的编码和生成

OBDD的模型检测，首先要生成二叉判定图BDD，本文使用二叉树来表示BDD［8，10］。由图2该微波炉用BDD的二叉判定子树表示，如图3所示。

图3的左分支表示联接变量节点的肯定命题、右分支表示联接变量节点的否定命题。这种表示的好处是直接在子树图中可以直接找到各变量的取值，缺点是在很多情况下，该二叉子树为稀疏二叉树，节点数目过于庞大，为2m（m为变量数目），。本文采用对状态编码的方法，将状态按照顺序依次编为自然数1～n，并将其转换成二进制数，这样就可以只使用k个布尔变量，其中k为不小于log2（n）的自然数，来生成二叉判定树，生成的子树为满二叉树或接近满二叉树，如图4所示，大大压缩了使用的空间。

图3 微波炉状态的BDD子树

图4 微波炉状态编码后的二叉判定子树

关于转换动作也可以用类似方法生成子二叉树。基于编码的BDD二叉判定树的生成算法如下：

1）读取状态转换模型，得到控制流图Control-Graph；

2）读取状态个数；读取转换动作个数；

3）GetBitLength（）；／／计算状态和动作的二进制编码所需布尔变量个数，生成状态和动作的二进制数组；

4）计算转换边个数，m＿TranNum；

5）for（i＝0；i＜m＿TranNum；i＋＋）

｛根据控制流图，得到转换边；

（1）转换前状态的二叉子树生成；

（2）转换动作的二叉子树生成，并联接到步骤（2）生成的子树上；

（3）转换后状态的二叉子树生成，并联接到步骤（3）生成的子树上｝

图5 微波炉模型生成的二叉判定树

微波炉模型的控制流图ControlGraph生成的BDD二叉树如图5所示。

4.2 从BDD到OBDD的化简算法

一般由二叉判定树形成OBDD，必须做以下工作进行化简：

1）保证所有路径上变量出现的顺序必须一致；

2）合并同构的子树；

3）删除多余的节点：

（1）删除重复的终止节点；

（2）删除重复的非终止节点；

（3）删除没必要存在的节点。

对于（1），可以从4.1节看到，路径上变量出现的顺序是一致的，而对于3）-（1），4.1节的生成过程以连接到true和false为结束，所以也不存在重复的终止节点。所以化简过程重点在于删除重复的非终止节点和冗余节点，以及合并同构子树，化简算法描述如下：

1）获取最下一层的节点加入队列vBreadNodeList；

2）while（vBreadNodeList［i］的左儿子或右儿子不为空）

DelRepeatNode（）；／／／／／／删除重复非终止结点及冗余结点；

3）执行函数DelRepeatNode（）

／／／两两查找重复非终止结点及冗余结点｝

①判断是否是重复非终止结点

②结点的重新定向

③删除重复结点｝

将当前层的上一层加入到临时队列m＿vTempOBDDList中

将当前层的上一层加入到临时队列vBread-NodeList中

4）for（i＝0；i＜层数；i＋＋）／／合并同构子树｛

①对每一层节点，查找当层的其它节点

②对同层节点两两比较后继节点，判断是否是同构子树

③对同构子树的父节点重新定向｝

4.3 CTL公式的描述及模型检测

CTL可以描述状态的前后关系和分枝情况，描述一个状态的基本元素是原子命题符号。公式由原子命题，逻辑连接符和模态算子组成。CTL的逻辑连接符包括：﹁（非），∨（或），∧（与），它的模态算子包括：E（Exists），A（Always），X（Nexttime），U（Until），F（Future），G（Global）。可以证明所有CTL公式都可用﹁、∨、EX、EG、EU来表示。

本质上，本模型检测方法进行验证的过程是按照CTL公式用旧OBDD计算新OBDD的过程。验证时，我们从被验证公式的最深层的子公式开始验证，一级一级逐步扩展到验证整个公式。

5 OBDD模型检测的计算过程及算法实现

5.1 利用CTL公式进行OBDD模型检测的计算过程

1）对于﹁f运算，我们只需复制f的OBDD并将其中终止节点的值交换即可；

2）对于f∨g运算，如果f、g是用二叉判定树表示的，我们要找到满足f∨g的状态，只需按先根次序同时遍历f、g的二叉判定树，一边遍历一边生成一个新的二叉判定树，然后对同一个状态在两个二叉判定树的终止节点的值进行析取运算，把所得值标在新二叉判定树中，就可以判断哪些状态满足f∨g，OBDD是化简后的二叉判定树；

3）对于EX的计算，EXf表示一个状态的下一个状态满足f。我们可以遍历S的OBDD，遍历到状态s的终止节点时，通过查找R的OBDD可以找到s的所有后继状态，然后根据f的OBDD就能得知这些后继状态中是否有满足f的状态，若有，则s满足EXf，这样当遍历完整个S的OBDD时，就能得知哪些状态满足EXf，得到所求的OBDD；

4）对于EG的计算，EGf＝f∧EX（EGf），我们可以遍历S的OBDD，找出所有满足f的状态，构成集合S′，如果一个状态满足EGf，那么它的某个后继也一定满足f并在S′中，如果它的所有后继都不在S′中，那么它一定不满足EGf，应该从S′中删除它，反复删除这样的状态，直到S′不再发生变化；

5）对于EU的计算，E［f1∪f2］＝f2∨（f1∧EX（E［f1∪f2］）），我们可以遍历S的OBDD，找出所有满足f2的状态，构成集合S′，然后再找出这些状态的前驱状态，把其中满足f1的添加到S′中，然后再找新添加的状态的前驱状态，把其中满足f1的状态添加到S′中，如此反复，直到S′不再变化为止。

5.2 计算过程的具体实现

由于篇幅所限，我们只给出f∨g的OBDD计算如下：

6 计算结果

对第4节给出的例子，我们来验证公式AG（start→AFheat）是否满足M。

首先利用5.1给出公式的转换公式：﹁E（trueUstart∧EG（﹁heat））

我们逐步给出公式各部分的验证结果，最后给出最终结果如图6所示。

终止节点为＊的表示能够到达的状态（该二叉树可以表示4个状态1、2、3、4），而终止节点为自然数的表示状态集合为φ，因此可以看到S（EG（﹁heat））＝｛1，2，3｝，S（S∧EG（﹁heat））＝｛2｝，S（E（trueUstart∧EG（﹁heat）））＝｛1，2，3，4｝，S（﹁E（trueUstart∧EG（﹁heat）））＝φ。因此公式AG（start→AFheat）不满足M。

图6 AG（start→AFheat）的逐步及最终验证结果

7 结语

虽然近些年来，模型检测是人工智能方面的一个研究热点，对模型检测和OBDD技术的介绍也很多，但是很少有关于OBDD模型检测实现算法的相关介绍，作者通过介绍自行开发的OBDD模型检测器，给出了基于编码的OBDD模型检测的具体实现算法，并利用该模型检测器验证了一个例子，填补了这一空白，并在今后的工作中逐步完善。

［1］BRYANT R E.Graph based algorithms for Boolean function manipulation［J］.IEEE Transactions on Computers，1986（8）：677～691

［2］林惠民，张文辉.模型检测：理论、方法与应用［J］，电子学报，2002，12（30）：1907～1910

［3］苏开乐，骆翔宇，吕关锋.符号化模型检测CTL［J］.计算机学报，2005，11（28）：1978～1979

［4］徐畅，刘吉锋，孙吉贵.基于经典逻辑的安全协议模型检测算法［J］.计算机科学，2008，6（35）：20

［5］赵辉，李彤.基于模型的验证及其方法［J］.计算机工程，2001，8（27）：45～56

［6］吕关锋，苏开乐，等.基于BDD的图表示及其算法［J］.中山大学学报（自然科学版），2006，1（45）：20

［7］郭建，杜建敏，等.基于时态逻辑的硬件设计形式化验证技术－模型检验［J］.小型微型计算机系统，2001，5（22）：521～523

［8］王飞明，胡元闯，董荣胜.模型检测研究进展［J］.广西科学院学报，2008，24（4）：320～321

［9］刘林霞，张自强，何安平.基于模型检测的半结构化数据查询［J］.计算机与数字工程，2009，37（8）

［10］贺亚博，郝克刚，葛玮.模型检测在软件需求分析及设计中的应用［J］.计算机应用与软件，2009，4（26）：129