ABSTRACT

In Symbolic Model checking, as a comparatively efficient method of representing transition relation with OBDD, we need firstly represent it as a boolean function with the aid of SMV language, and then synthesize the OBDD using relevant algorithms. However, during the course of representation from transition relation to the boolean function, we often encounter two problems: first, the assignment of next state is non-deterministic; second, the number of non-input variables with certain variation regularity is more. In this paper, through the concept of equivalent-input variables, we impose restriction on the assignment of the boolean function formula used to represent transition relation, and give definite solutions to these two problems, enabling the boolean function representation of transition relation is further accurate and efficient.

Keywords:Symbolic Model Checking, OBDD, Transition Relation, Boolean Function, Equivalent-Input Variables

迁移关系的布尔函数表示的优化

张小珍，江建国

辽宁师范大学数学学院，辽宁 大连

收稿日期：2016年12月1日；录用日期：2016年12月18日；发布日期：2016年12月21日

摘 要

符号模型检测中，将迁移关系表示为OBDD的一种较为高效的方法是先借助SMV语言将迁移关系表示为布尔函数，再利用相关算法综合得其OBDD。但在将迁移关系表示为布尔函数时常会遇到两个问题：第一，下一状态取值不确定；第二，具有一定变化规律的非输入变量较多。本文提出等效输入变量的概念，对迁移关系的布尔函数公式的取值条件加以限制，给出了这两个问题的具体解决办法，进而使得迁移关系的布尔函数表示更加准确、高效。

关键词 :符号模型检测，OBDD，迁移关系，布尔函数，等效输入变量

1. 引言

随着计算机科学技术的迅速发展，关于计算机硬件和软件系统的正确性验证也越来越重要，而关于其功能的验证主要采用模拟法和形式化验证法。相对于模拟法来说，形式化验证法更能保证验证的完备性，所以其在工业上的应用更为广泛。此外，形式化验证法大体上可分为等价性检测、模型检测和定理证明三类。

模型检测 [1] [2] 是一种自动的、基于模型的形式化验证技术，它通过遍历状态空间来对系统某方面的性质作出验证。然而，随着系统规模的不断扩大，状态空间的大小呈指数级增长，于是就引起了状态空间爆炸问题。为了克服显式模型检测在解决此问题上的局限性，符号模型检测应运而生。

符号模型检测是由J. R. Burch，E. M. Clarke和K. L. McMillan等人于20世纪90年代初提出的 [3] [4] [5] ，它通过布尔函数来表示状态集、迁移关系，而布尔函数则以有序二叉判定图(Ordered Binary Decision Diagrams，简称OBDD) [6] [7] [8] 来呈现。符号模型检测的提出使得状态数超过10²⁰的实际系统得到了验证，在很大程度上缓解了状态空间爆炸问题，进而促进了验证技术的重大突破。而近几年关于OBDD变量序的研究 [9] [10] 及符号模型检测在应用中的研究 [11] [12] [13] [14] 使得形式化验证技术得到了重大发展。

符号模型检测中，在将迁移关系表示为数据结构OBDD时常会遇到两个问题：第一，状态变量在下一状态的取值不确定；第二，具有一定变化规律的非输入变量较多时，它们之间关系的处理。对于这两个问题，文献 [15] 中给出了一些相应的的解决办法，但其较为抽象，而且形式化过程、结果都存在有一些赘余表示。

本文通过提出等效输入变量的概念，给出了借助SMV (Symbolic Model Verifier)语言描述迁移系统并由此得出迁移关系的布尔函数时，对于这两个问题具体明确的解决办法，此外对文献 [15] 中所提关于的公式进行了改进，使得形式化过程更加高效，形式化结果更加简洁，进而直接或者间接地提高了符号模型检测中某些具体问题的验证效率。

2. 基本概念

模型检测中，对系统某方面的性质作出验证时，首先要对实际系统建模得出一个迁移系统。

定义1：迁移系统是一个多元组，其中S表示系统的状态集合，表示系统的初始状态集合且满足，表示迁移关系，它是状态集上的二元关系：对于，都满足，是用于描述状态的原子命题集，是从状态集到原子命题集的幂集上的函数，称为标记函数。

一个迁移系统可以通过一个有向图来表示，如图1所示。

对于图1所示迁移系统有：

符号模型检测中，需首先将迁移系统中的状态集和迁移关系表示为布尔函数的形式，而且在此表示过程中会涉及到一些变量。

定义2：若一个变量的定义域是，则称此变量为布尔变量。令为布尔变量，若集合上的函数满足布尔运算、、、，则称此函数为从到上的元布尔函数。

用来描述系统各状态的自变量，称为状态变量。系统模型的任意一个状态可以认为是对状态变量集中各元素的一个赋值。状态变量的取值可能会随着状态的迁移而变化。而由外界环境所决定的变量，称为输入变量。在有限状态的迁移系统中，不可以指定输入变量的初值，而且它的取值变化完全取决于模拟环境，而与状态迁移毫无关系。

布尔函数的表示方法有很多种，在诸多表示中，OBDD是布尔函数较为紧凑且较为规范的表示形式。

定义3：二叉判定图(Binary Decision Diagrams，简称BDD)是一个有限有向无环图，满足条件：

1) 具有唯一初始结点；

2) 所有非终止结点用布尔变量标记，且都恰好有两条边指向其它结点：一个用虚线表示，一个用实线表示，其中虚线表示布尔变量取值为0，实线表示取值为1；

3) 所有终止结点标记为0或1。

有序二叉判定图(Ordered Binary Decision Diagrams，简称OBDD)是带有某些有序变量表的BDD。

如图2是无变量序的BDD，而图3是带有序的OBDD。

3. 迁移关系的布尔函数表示

符号模型检测中，需要将迁移系统中的迁移关系表示为OBDD，而当系统较大较为复杂时，则需借助SMV语言描述迁移系统，并依据此得出表示迁移关系的布尔函数，进而通过相关算法综合求得其OBDD。而用SMV语言描述迁移系统以及由此得出迁移关系的布尔函数时，通常会遇到两个问题的处理：第一个问题是，状态变量在下一状态的取值不确定；第二个问题是：具有一定变化规律的非输入变量较多时，它们之间关系的处理。

为有效解决这两个问题，我们引入了一种叫做等效输入变量的状态变量：在任意下一状态取值都不确定的状态变量，称为等效输入变量。很明显，等效输入变量不是输入变量，但其取值不会随着状态的迁移呈现一定的变化规律。

本节工作前提是状态集已被表示为布尔值和布尔函数。符号说明：表示状态变量，表示状态变量在下一状态的取值所满足的关系表达式，而则表示状态变量在下一状态的取值。

3.1. 非确定的下一状态

迁移关系表示为布尔函数过程中，为解决下一状态为非确定赋值的问题，我们对所研究的状态变量

图1. 迁移系统的有向图

图2. 无变量序的BDD

进行考究，看状态变量是否为等效输入变量，进而给出不同的解决办法，使得形式化结果更加简明。

若状态变量为非等效输入变量，即只在某些条件下，其下一状态取值不确定：

1) 用SMV语言描述迁移关系时，需将该条件下的赋值为所有可能的取值组成的集合；

2) 由SMV语言求得迁移关系的布尔函数时，只需将该条件的取值为来表示，而无需再引入其它输入变量，因为输入变量的引入表示系统状态的增多。

若状态变量为等效输入变量，即其在任意下一状态的赋值都不确定：

1) 用SMV语言进行描述时，不需要对其下一状态取值进行描述；

2) 由SMV语言求得迁移关系的布尔函数时，即依据求取时，我们对的条件进行修改，要求其不仅不可以是输入变量，而且不可以是等效输入变量。假设是等效输入变量，则无论任何时候都满足，而，于是通过这样的限制，可

以避免形式化过程中的冗余表示。

例1：已知迁移系统的有向图如图4所示，试用SMV语言对该系统进行描述，并由此给出其迁移关系的布尔函数。

首先，分析非输入变量的变化规律可知：变量在任意一个下一状态的取值是不确定的，既有TRUE，也有FALSE，因此为等效输入变量，所以在SMV语言描绘中不对进行说明。而变量则遵循一定的变化规率：当为TRUE时，在下一状态的取值为FALSE；而为FALSE时，在下一状态的取值是不确定的，既有TRUE也有FALSE。

由此得出该迁移系统的SMV语言描绘如下所示：

图3. 带有序[x,y]的OBDD

图4. 迁移系统TS₁的有向图

其次，由SMV语言描绘求得迁移关系的布尔函数时，关于下一状态是不确定值的处理：首先分析是等效输入变量，所以不需要求。而是非等效输入变量的状态变量，当时，的取值是不确定的，此时需使取值为即可；而且写表达式时，没有必要列真值表，只需将时的各种情况用布尔表达式表示然后再相加即可。

由SMV语言中的next表达式分析：时的条件是且，故。

最后，得出图4所示系统的迁移关系的布尔函数是：

3.2. 多个非等效输入

当迁移系统中有具有一定变化规律的非输入变量较多，即有多个非等效输入变量的状态变量时，处理好各之间的关系，方可得到原迁移系统的正确描述。因为用SMV语言描述迁移系统时，需分析各的变化规律，而当非等效输入变量的状态变量较多时，分析某个变量的变化规律可能会引入一些原迁移系统中不存在的迁移，此时在分析其他变量的变化规律时需避免这些赘余迁移，也就是说，依据每个都会得到一个迁移图，而它们的公共部分才为已知迁移系统的有向图。

例2：已知迁移系统的有向图如图5所示，试用SMV语言对该系统进行描述，并由此给出其迁移关系的布尔函数。

图5. 迁移系统TS₂的有向图

首先，分析可知，状态变量和都不是等效输入变量，而变量的变化规律是：只有当和均为FALSE时，下一状态的真值不确定，既有TRUE，也有FALSE；而其它情况下，下一状态的取值一定为FALSE；但殊不知，这个变化规律增加了迁移，如图6中的左图虚线箭头所示，因此在分析的变化规律时，必须避免这些迁移的出现。对于，要求当且时，在下一状态的取值为TRUE，这样避免了迁移；而其他情况下，在下一状态的取值一定为FALSE，这样的赋值避免了其他的赘余迁移。虽然又引入了额外的迁移，但也不影响最后结果，如图6中的右图说明了变量的变化规律，其中虚线部分为所引入的无关迁移。图6中左图和右图的公共部分即为图5中的迁移。

该迁移系统的SMV语言描绘如下所示：

由迁移系统的SMV语言描述求时，利用同例1的方法，只需将各时的条件转化为对应的布尔表达式再相加即可。所以可求得，，于是可得图5中所示迁移系统的迁移关系的布尔函数是：

4. 结语

本文给出了符号模型检测中将迁移关系表示为布尔函数时，关于下一状态取值不确定以及非等效输

图6. x₁和x₂的变化规律各自所对应的迁移图

入变量较多时的处理方法，从而使得迁移关系的布尔函数表示更加高效、准确。但对于该表示过程中所遇到的其它问题，比如用当前值无法表示下一状态取值而需要引入其它输入变量等问题的处理，还有待于进一步研究。

文章引用

张小珍,江建国. 迁移关系的布尔函数表示的优化
Optimization of the Boolean Function Representing Transition Relation[J]. 软件工程与应用, 2016, 05(06): 319-326. http://dx.doi.org/10.12677/SEA.2016.56037

参考文献 (References)