被动测试在BGP/OSPF协议上的实现

摘要

协议测试是提高协议实现正确性的重要保证。被动测试是一种比较新的协议测试概念，本文的主要工作是将被动测试方法应用于协议测试中。

本文介绍了协议的形式化描述工具：FSM/NFSM/EFSM/CFSM模型，总结了在以上几个模型上做被动测试的现状和遇到的难点问题。

本文重点讨论了EFSM模型上被动测试的变量管理问题，总体思路是要将尽可能多的协议信息记录下来，以发现被测系统中的错误，同时尽量降低算法复杂度。在此基础上，提出了多个变量管理方法，并对各个方法进行了综合，设计了变量管理的综合算法。

在实践方面，设计了与协议无关的被动测试系统的总体框架，该系统具有良好的通用性和可扩展性。介绍了各个模块的实现，其中重点介绍了变量管理器。介绍了采用被动测试对BGP和OSPF协议实现的测试情况。对于OSPF中协议参数的测试体现了变量管理系统的能力，测试结果验证了算法的正确性和有效性。

最后，本文总结了变量管理问题在被动测试中的意义，提出了被动测试研究的进一步工作方向。

Protocol testing is very important to guarantee the correctness of protocol implementations. Passive Testing is a new concept of protocol testing in recent years. In this paper, we try to apply passive testing method to routing protocol testing.

We show several formal models for protocol specifications: Finite State Machine, Non-deterministic Finite State Machine, Extended Finite State Machine and Communicating Finite State Machine. The former works on passive testing on these models are reviewed. Problems are also raised.

Our work concentrates in the problem of variable management for passive testing EFSM model. Several solutions in different views are suggested and analyzed. An integrated algorithm is suggested.

We also show the implementation of passive testing on FSM/NFSM/EFSM models with the examples of testing BGP/OSPF protocols. A protocol-independent passive testing architecture is introduced. Each part of the system is described. The parts for variable management are explained in detail. The experimental results of the passive testing on BGP/OSPF are also shown and analyzed.

Finally, the importance of the variable management in passive testing is suggested. And the future work is also described.

Keyword

Protocol Testing

Passive Testing

Extended Finite State Machine (EFSM)

Constraints Satisfaction Problem (CSP)

第一章引言

1.1. 背景

Text Box:
图1-1 网络技术在近二三十年来飞速发展。随着Internet的迅速普及，网络规模的不断扩大，网络出现错误的可能性也在增加。其中，协议是网络的灵魂，对网络产品进行协议测试，可以发现协议实现中的错误，提高协议实现的可靠性，从而保证网络尤其是Internet的高效运行。目前，协议测试仍远远不能满足网络技术发展的需求。大量未经充分测试（尤其是第三方测试）的网络产品（包括协议实现的硬件与软件）已经被广泛使用，这给网络的运行质量带来潜在的威胁。

在协议工程学中，为了检验实现是否符合协议规范，可以使用一致性测试和监控诊断的方法来实现（见图1-1）。作为一种辅助的测试手段，监控诊断通过观察协议实现的运行情况来检测协议是否运作正常。“被动测试” (Passive Testing)是一种监控诊断的方法，其概念最早在70年代初被提出。为了区分，称传统的测试为主动测试(Active Testing)。

一致性测试是主动测试领域的重点。形式化技术是协议测试中的重要手段和工具，从协议的描述，到生成、评价测试集，形式化技术都发挥了重要的作用。主要的形式化描述模型是有限状态机（包括扩展有限状态机等）。协议状态机模型是协议测试方法、测试结构、测试集的设计和组织及测试集覆盖率的评价等的依据。近20年来研究人员在主动测试领域做了大量的研究，取得了丰硕的成果。但是主动测试对于复杂协议存在局限性，在路由协议测试中，我们就发现对路由表进行测试时，需要辅助的测试部件。

被动测试是另一种测试思想：通过监听来采集数据，通过分析数据来发现协议实现中存在的错误。监听是从底层收集数据的方法，收到的数据用于验证系统的特性，所以称为被动测试。从目前的研究来看，被动测试比较适用于测试网络动态行为，如路由器中路由信息的测试，TCP协议中的拥塞控制等。相关的研究包括：

[8]提出了在网络中设置观察点(observer)，收集网络信息，进行网络故障检测。 [4]将这个概念应用于网络故障管理上，提出了基于FSM模型的有效的算法。由于它不影响网络设备的正常工作，特别适用于发现正在运行的网络上的故障。 [5][6]设想将被动测试的方法应用于网络故障的发现和定位，这些工作集中在理论方面。从现有的文献和研究成果看来，被动测试比较适合于下面几方面的应用：

l 测试正在运行的实际网络设备。正在运行的设备不能将其取出，被动测试能够保证在不干扰网络正常运行的情况下对设备进行测试。

l 测试系统的动态行为，比如路由器的路由表。路由信息的交互具有随机性，不容易通过模拟生成主动测试例（ [10]的Socrates系统只能在概率上给出错误的覆盖范围，并不能保证全部）。

l 测试复杂的系统，例如带诸多协议变量的系统、实时系统。现有的测试方法要测试系统行为，复杂度很高而且往往不实用（测试序列长度常常是状态数的指数，而复杂系统的状态数目很大）；而被动测试比较适合这种情形。

l 帮助生成主动测试的测试例。被动测试有较为通用的测试方法，是一种易于实现的测试手段。被动测试能够提供一定的错误覆盖，可以帮助生成主动测试的测试例。

笔者认为，被动测试是主动测试的有益的补充，虽然它在理论和实践上都还存在着很多没有解决的问题，但它在网络管理等领域有良好的应用前景。

在基于自动机模型的被动测试方面， [4]提出了FSM/NFSM的被动测试算法。然而，很多协议包含了变量系统，用FSM/NFSM描述是不够的，而扩展有限状态自动机（EFSM）模型能比较好的描述这类协议。基于EFSM模型的被动测试问题，公开的研究还不算多。[4]提到在EFSM模型测试上，被动测试能避免主动测试面临的状态爆炸问题。但具体的算法如何，算法的实现如何，都没有讨论。

我选择了这个题目，希望能在EFSM模型的被动测试问题上有所创造，为被动测试应用于路由协议测试方面做一些有用的探索。

1.2. 论文章节安排

论文分成九章。

第一章概述工作背景，第二章介绍协议测试的基本概念和被动测试的研究进展和遇到的问题。第三章介绍了我们用FSM模型描述BGP协议、用NFSM模型描述OSPF协议的实验和结果分析，提出了采用EFSM描述OSPF进行被动测试。

第四章针对EFSM被动测试中遇到的变量管理问题进行了分析，从不同角度提出了多个解决方案，并提出了综合的算法。第五章介绍了采用EFSM描述OSPF协议进行被动测试的实验和结果分析。

第六章介绍被动测试数据获取模块的设计。

第七章给出了的总结和展望。

第二章协议的形式化描述和被动测试的理论概述

2.1. 协议的形式化描述方法

所谓“协议”，在这里指的是计算机网络和分布式系统中各种通信实体或进程间相互交换信息时必须遵守的一组规则，协议是计算机网络的核心。

协议自动机是网络协议的形式化描述的重要工具。在本文中，我们主要用了三种自动机对协议进行形式化描述。它们是：确定有限状态机（Finite State Machine, FSM，或者称为Deterministic Finite Automata, DFA）、非确定有限状态机（Non-deterministic Finite State Machine或者称为Non-deterministic Finite Automata, NFA）和扩展有限状态机（Extended Finite State Machine）。此外，被动测试常用于网络监控，在考虑多台网络设备以及设备之间通道的时候，往往使用通信有限状态自动机（Communicating Finite State Machine）来描述。下面分别对这几种自动机进行介绍。

2.1.1. 确定有限状态机FSM

FSM的定义见[17]。

FSM可以直接描述简单的状态变迁情况。在我们的实验中，BGP的协议状态机比较简单，在不考虑时钟因素的时候，可以用FSM描述。

2.1.2. 非确定有限状态机NFSM

NFSM的定义见[17]。

可以证明，NFSM的描述能力与FSM相同。我们可以对NFSM进行状态扩展，转化成FSM。但在被动协议测试中，除了考虑描述能力以外，还要考虑被测自动机的状态数目及其对测试算法的复杂度的影响。到目前为止，尚未找到一种扩展状态数目为多项式级的FSM-NFSM转化算法。所以，在被动测试的时候，不能简单的把NFSM转换成FSM再用FSM被动测试算法，而需要重新设计一套算法测试NFSM。

在我们的实验中，NFSM主要作为OSPF协议状态机的简化模型（不考虑时钟问题和协议变量问题）。

2.1.3. 扩展有限状态机EFSM

定义：

一个扩展有限状态机M是一个五元组<S,s0,Σ,Χ,T>。其中：

l S是状态的有限集合；

l s₀∈S是初始状态；

l Σ是有限的字符表；

l X=(x1,x2,…,xk)是一个向量，表示一个变量的有限集合；

l T：对于T中任意一个元素t，t=<s,i,P,A,s’>。其中 s是变迁的起始状态，I是输入，P是变迁的条件(它是由X中的变量或者常数参与的逻辑表达式)，A是变迁的动作（它是X中的变量或者常数参与的，对X中的变量的赋值语句集合），s’是变迁的到达状态。

当M处于某一个状态s的时候，收到一个输入i，如果存在一个t∈T与s、I对应，并且使P的值为真，则M执行A中的动作并移到状态s’。

同样可以证明，EFSM的描述能力与FSM相同。但这个过程同样碰到状态爆炸的问题。因此，我们也需要另外设计算法，在不产生状态爆炸的情况下测试协议状态机。

在我们的实验中，在不考虑时钟的前提下，EFSM可以直接描述OSPF协议状态机。

2.1.4. 通信有限状态自动机CFSM

定义:

一个通信有限状态自动机由一组有限状态自动机的集合M和一组通道C组成。约定：网络N=(M,C)；|M|=r

且N满足：

l M={m₁,m₂,……m_r}是一个有r个有限状态机的有限集合；

l C={C_ij：i,j≤r而且i≠j}是一个通道的有限集合；

l 对M中的每个自动机m_i，是确定有限状态机，其描述与FSM定义相同；

l C中的每个通道C_ij表示m_i到m_j的通信通道。它是一个先进先出的队列，m_j从队列的头读出数据作为输入，m_i把要向m_j输出数据送到队列的尾部。

CFSM是描述互相通信的多台网络设备工作情况的常用方法。

2.2. 协议测试的基本概念

从自动机的角度，协议测试本质可以描述如下：

给定一个状态机（specification），同时给定一个该状态机的被测实现（Implementation Under Testing，IUT），测试IUT的工作是否符合状态机的描述。

在主动测试中，IUT仅与测试设备连接，测试设备根据状态机描述中所要求的功能，与IUT通信，同时检查IUT的输入和输出情况，确定IUT所在的状态，并且根据状态的变迁检查IUT的工作是否与协议自动机的描述一致。

主动测试是离线测试，一般在设备投入使用之前进行。

在被动测试中，IUT在线工作，测试设备不与IUT直接通信，只是被动地监听IUT与其他网络设备的通信，观察IUT的输入与输出，以此推测IUT的状态转换，判断IUT的工作是否与协议自动机的描述一致。由于不影响IUT的正常工作，也不给网络造成额外的信息流，被动测试可以用作在线测试，监控设备的运转是否正常。

下一节将对被动测试做比较详细的介绍。

2.3. 被动测试

2.3.1. 历史、现状和展望

早在七十年代，就有人提出了被动测试这个概念，用于测试集成电路。而近年来，随着计算机网络的普及，各种网络协议的测试成了热点。传统的协议测试以主动测试为主，日趋成熟，但是主动测试不能在产品运行阶段发现错误，不能适应复杂的动态行为。而被动测试较好的适应了这些情况，并且在近年来得到了一些应用。

[4]中提出了对FSM和NFSM进行被动测试的算法，并分析了算法复杂性；同时提出，采用被动测试手段可以避免主动测试遇到的一些困难，比如可达性问题，状态机状态爆炸问题等。

[5][6]中提出对CFSM模型进行被动测试，并根据测试结果进行错误定位(Fault Location)的理论算法。

这些研究的成果表明，被动测试在网络管理方面是很有前途的。

本文作者认为，被动测试和主动测试是互补的。主动测试主要用于网络产品开发和生产阶段，而被动测试用于网络产品使用过程中的监控和管理。随着网络设备复杂度的增大，单纯靠开发和生产阶段的质量控制是不够的，引入网络实时监控是必要的，在这个过程中，被动测试将大有作为。

值得强调的是，被动测试属于监测手段，不能保证覆盖所有的可能错误。在被动测试的研究中，我们追求的是尽量多的发现潜在错误，同时保证不误判。即：被测实现发生错误是被动测试报错的必要而非充分条件。这是我们设计被动设计算法的原则，称之为：“被动测试的报错条件”。

2.3.2. 被动测试原理和基本算法

被动测试根据被测实现与其它设备的通信过程的输入输出序列，判断被测实现运行是否正常，如果发现不可能的输入输出序列，即认为被测实现的运行有错误。

下面介绍FSM和NFSM被动测试的基本算法。

FSM被动测试的算法：

FSM的被动测试算法分为两步：Homing过程和监测过程。

1、Homing过程

被动测试算法开始的时候，认为被测实现可能处于FSM所有的状态中的任意一个。通过不断监听被测实现的输入输出，排除一些被测实现目前不可能处在的状态，从而使被测实现可能处在的状态的集合(Possible State Set)的规模逐步变小。当Possible State Set里面只有一个状态的时候，被测实现所处的状态被确定，此时Homing过程完成。

Text Box:
图2-1 FSM的被动测试算法——Homing部分（摘自[4]） Homing过程的伪代码如图2-1所示。

2、监测过程

在确定被测实现所处的状态之后，被动测试算法继续监听被测实现的输入和输出。跟踪检查被测实现所处状态上，是否允许这样的输入输出。如果监听到了不可能的输入输出，即认为被测实现出现错误。如果没有发现错误，监测过程将无限期的进行下去。

监测过程的伪代码如图2-2所示：

图2-2 FSM的被动测试算法——监测部分（摘自[4]）

NFSM被动测试的算法：

Homing和监测过程两部分实际上是可以合二为一的。Homing过程可以在发现Possible State Set仅有一个状态的时候，继续监听，直到Possible State Set为空，即认为被测实现发生错误，否则无限期跟踪下去。FSM的分步算法只是为了易于理解。

在NFSM中，一个状态对一个输入可能有多种输出。Homing结束之后，被测实现的可能状态集合仍可能变大。所以，Homing和监测过程并不能明显区分。因此，NFSM的被动测试算法，需要把FSM的Homing和监测合二为一。

图2-3 NFSM的被动测试算法（摘自[4]）

NFSM被动测试的伪代码如图2-3所示：

FSM和NFSM在被动测试中的最大区别是：FSM的Possible State Set规模非严格递减，而NFSM模型的Possible State Set规模可能变大。

[4]中还提到当观察的数据缺少n步输入输出的时候的算法，与NFSM的算法类似，在此不再累赘。

EFSM被动测试算法的讨论

在[4]文中提到，被动测试在测试EFSM的时候不会遇到主动测试时候遇到的一些困难。比如：带变量的测试例的生成问题、可达性问题等，但没有提出具体的测试算法，也没有实用的测试例子。目前为止，EFSM被动测试问题也没有得到很好的解决。主要原因是：

1、虽然被动测试可以忽略EFSM中的变量，从而把EFSM模型简化成NFSM模型，但这样做，所有的变迁（包括从变量角度上看可能是互斥的变迁）均被认为是可能的变迁，查错能力有限。

2、如果考虑变量，变量值的获得是一个很大的问题。在被动测试里面，虽然不需要编写覆盖所有情况的测试集；但需要获得变量当前的值，从而判断某条变迁是否可能发生。测试是在线的，不一定能在协议建立连接之初开始监测。所以，如何根据EFSM的某一段输入输出，获得变量的值，是一个很大的问题。

本文作者的毕业设计课题是FSM/EFSM的被动测试算法及其在BGP和OSPF协议上的实现。这包括了FSM/NFSM模型的算法的实现和EFSM算法的设计与实现。其中主要难点在于EFSM被动测试中变量的处理。在论文工作过程中，我们用FSM描述BGP协议、用NFSM模型描述OSPF并进行了测试，发现NFSM对OSPF的描述过于简化，测试能力不强。提出采用EFSM模型描述OSPF，并提出了多种EFSM变量管理方法和变量管理的综合算法。

第三章 FSM/NFSM被动测试的实验系统及实验结果

被动测试实现的总体思路是：监听被测实现在数据链路层的通信，获得数据包，经过多次的解析和过滤，获得测试所关心的输入输出流，送到测试模块。测试模块从配置文件读取协议自动机的描述，通过计算和比较，判断输入输出流是否合法。

在测试系统的实现中，我们采用了面向对象技术，同时使系统尽可能与具体协议无关。以下介绍的实验系统框架，除了注明与协议相关的模块之外，其他模块均与协议无关。

FSM和NFSM的被动测试算法可以通用，其测试系统结构也相同。

3.1. FSM/NFSM被动测试系统的结构

FSM/NFSM被动测试系统的框架如图3-1所示。

图3-1 FSM/NFSM被动测试系统结构

从功能上分析，整个系统可以分成两部分，在图中以虚线分开。

第一部分是底层的数据获取部分，功能是从以太网上获取被测实现的数据包，在MAC/IP/TCP层做解析、过滤，生成被测协议对应的数据包流和目录文件。这部分在Linux/Unix系统上实现，在第七章详细介绍。

第一部分输出的数据分成两个文件，一个是二进制文件，顺序记录监听所得的包。另一个是索引文件，记录每一个包的源/目的地址、包类型、在二进制文件中的起始地址和长度。

第二部分是上层的测试部分，这部分在PC上实现。协议包解析器把底层的数据流转换成被测协议数据包的类实例；测试控制器从协议包解析器生成的协议包类实例中读取所需的通信信息，并计算每一步变迁之后的可能状态集。

在系统中，尽量做到了与具体协议无关的要求。只要在底层采用不同的过滤器，在上层采用不同的协议包解析器即可满足不同被测协议的需要。

3.2. 协议数据包的表示和协议包解析

Text Box:
图3-2 OSPF协议数据包的类继承关系这部分与协议相关。

在实验系统里，协议的数据包用类表示。对于协议中的多种数据包，可以用类继承的方法很好的表示出来。以OSPF协议为例，类继承关系如图3-2所示。

OSPF_Packet是所有OSPF数据包的公共父类，描述OSPF数据包的公共数据。OSPF_Hello_Packet、OSPF_DD_Packet、OSPF_LSR_Packet、OSPF_LSU_Packet、OSPF_LSA_Packet五个子类五种包分别表示OSPF的五种数据包类型。

五个子类的结构相同，具体如图3-3。

class OSPF_包类型_Packet: public OSPF_Packet

{

       public:

       <OSPF数据包公用包头> *hdr; //在OSPF_Packet中定义;

       <特殊包头r> *subhdr;                     //在子类中定义

       int <多元素项的数目>             //子类中定义（比如：Hello中的Neighbor数目）

<多元素项> *…                            //子类中定义（比如：Hello中的Neighbor域）

void print();          // OSPF_Packet定义, 打印数据包的基本信息

int fromMem();      // OSPF_Packet定义, 把存储在内存里的二进制代码转换成OSPF包.

Virtual private:

Void printInside(); //子类中定义，print()调用，打印子类相关的信息

Int analyze();        //子类中定义，fromMem()调用，解析子类特有的域

}

图3-3 OSPF的数据包类

外部通过调用一个实例的fromMem()，可以完成任意一个类型的协议数据包的从二进制代码到高级数据结构的解析工作。

从底层输出文件（索引文件+二进制文件）到内存是由OSPF_Loader的类实现的。OSPF_Loader读取索引文件、在二进制文件定位并且把所以文件指定长度的数据从二进制文件读入内存。

3.3. 测试控制器

测试控制器是被动测试实验系统的控制部分。负责事件的读取和可能状态集合的维护，实现了FSM/NFSM被动测试算法。这部分由陈东洛完成，算法见图2-3。

3.4. 采用FSM描述BGP的被动测试实验

BGP协议可以用FSM描述。具体的FSM状态变迁图见附录A。

3.4.1. 用Socrates模拟多个路由器

Socrates是Bell Lab Research China授权清华计算机系协议测试组做科研使用的一套模拟测试软件[10]。它可以在Linux下通过3到4个网卡与路由器通信，模拟最多255台路由器的工作。我们采用它作为实际网络的一个模拟。

Text Box: 图3-4 实验连接图

3.4.2. 实验连接图

实验连接如图3-4。

实验中，被动测试器监听路由器A——网络模拟器（多路由器）的之间通信。

目的：测试路由器A在相当规模的网络里面的表现。

3.4.3. BGP实验结果和分析

实验结果是：对各组数据，被动测试算法都能在第一步完成Homing过程。

分析其原因是：

BGP协议的自动机是确定有限自动机，而且每一个输入输出几乎都是只有一个后继状态。所以，Homing过程很短。OSPF的协议自动机比较复杂，采用OSPF作为测试对象，能得到更多有用的信息。

3.5. 采用NFSM描述OSPF的被动测试实验

OSPF协议可以用NFSM简化描述，具体的状态变迁图见附录B。在OSPF测试中，除了继续使用用BGP的那套实验环境之外，还另外增加了两套实验环境，分别作简单测试和复杂测试。

3.5.1. 简单测试的实验环境

实验连接如图3-5。

监听路由器A——路由器B的之间通信。

目的：用最简单的通信测试被动测试系统。

图3-5 简单实验的连接图

Text Box: 图3-6 复杂实验的连接图 3.5.2. 复杂的测试环境

实验连接如图3-6。

让路由器A同时与网络模拟器（多路由器）和路由器B通信，监听路由器A与路由器B之间的部分。

目的：测试路由器A的消息传播，同时避免因为模拟器的错误而造成的通信问题。

需要指出的是，三个实验方法使用的IUT都是很成熟的CISCO设备。所以，是否找到错误并不是我们的主要评价标准（虽然我们也发现了Socrates系统里面一些没有严格执行RFC的地方），我们主要的评价标准是被动测试的Homing过程的情况：对于BGP，主要考察其Homing过程的长度；对于OSPF，考虑它的状态被确定的时间和变量的确定情况。

3.5.3. NFSM描述的OSPF被动测试实验结果和分析

对三个环境下面获得的数据，NFSM描述的OSPF协议的被动测试都不能到达状态Homing。

NFSM本身是不保证状态收敛的，所以，对OSPF的测试，采用NFSM是不足够的。最好采用EFSM模型。

后面，我们将讨论EFSM模型被动测试的算法和实现。

第四章 EFSM被动测试中变量管理问题的算法研究

如第二章所叙述，EFSM被动测试中，变量是一个难点。在论文中，我们考虑了多种解决方案。下面分别介绍这些方案。

需要声明的是：在讨论中，我们假设变量的取值均为非负整数。在网络协议中，这个假设是合理的。

4.1. 区域状态机的思路

在EFSM测试中，经常采用的是区域状态机的思想：找出变量值的等价类。对于两组变量值，如果它们对EFSM中任何条件判断是等价，则认为这两组变量值是等价的。这样，可以把整个变量取值空间划分为若干个等价类（区域）。找出所有的等价类（区域），可以把EFSM的每个状态S分裂成A个子状态S₁、S₂、……S_A（A是区域的数目），子状态S_i对应于EFSM处于状态S、并且其变量的值属于第i个等价类的情况。可以构造出一个FSM，它的状态是EFSM状态扩展的子状态，变迁不需要条件和动作。

假设EFSM中每个变量的取值范围被EFSM中所有条件分成了n个区间，EFSM一共有v个变量，s个状态，则子状态的总数为s*n^v个。一般情况下，n很大，所以，直接构造FSM有状态爆炸的问题。

被动测试不需要编写测试例，只需要记录当前被测实现所处在的状态和该状态可能变迁即可。而记录状态的可能变迁，一般不需要把整个扩展后的FSM构造出来。所以，被动测试的跟踪过程不受状态爆炸的问题困扰。

但是，在被动测试完成Homing之前，Possible State Set有多个可能的状态，此时如何表示这些可能状态的集合是一个很困难的问题。

如果记录被测实现可能处在的EFSM状态和每个变量可能的取值区间的集合，则变量值的取值区间很可能有多个，最坏的时候是所有状态和所有取值区间都是可能的，此时，状态数是s，每个状态下面的可能取值区间有n^v个，同样碰到指数级复杂度的问题。

4.2. 可能变量值的存储

4.2.1.放弃不确定的变量值

另一个直观的想法是，尽量保存变量的值，但如果不能保存，则放弃。在这种思路下，每个变量要么有确定的一个值，要么被设置为VALUE_VAGUE，表示它的值还不能确定。

在这种情况下，当生成的一个状态对应的变量可能有多个不同的值的时候，变量被标记成VALUE_VAGUE，这样，每次的可能状态最多为N（N是状态数目），每个可能状态只对应一组变量值，不存在指数级复杂度问题。

此时，尽管有一些变量的值可能是未知的（被标记成VALUE_VAGUE的变量），但也很可能有一些变量的值是被确定了。我们可以用已经确定的变量帮助判断变迁的合法性。表4-1是VALUE_VAGUE变量和确定值变量的算术运算关系和逻辑运算关系。

带有VAGUE值的算术运算与逻辑运算定义
*操作符*	*操作数*	值
缺省	任意一个值为VAGUE	VAGUE
缺省	所有值不为VAGUE	正常计算结果
*	任意一个为0	0
/	被除数为0	0
/	除数为0	Error
^	任意一个值为False	False
V	任意一个值为True	True

表4-1

在这套带有VALUE_VAGUE的运算规则中，每个变迁条件可能有三个取值：True、False或者Vague。当变迁条件为True或者Vague的时候，我们认为变迁由可能发生。

4.2.2.记录变量可能的取值区间

4.2.1的方法虽然解决了指数级复杂度问题，但把所有不确定的取值标记成VALUE_VAGUE，损失了很多信息。

其实，4.2.1的方法与4.1的方法是两个极端，4.2.1放弃了所有未确定变量的可能取值区间，而4.1的方法保留了所有未确定变量的可能取值区间。在这两个极端之间，是保留未确定变量的部分取值信息。

其中最简单的方法是：对4.2.1的方法进行改进，对所有标记为VALUE_VAGUE的变量，改用一个区间R=[a,b]记录该变量的取值范围，称R为“可能值区间”。R的定义：

对一个变量v，它的可能值区间R(v)是包含v的所有可能取值的长度最小的区间。即：

为了保持一致性，已经被确定的变量的值也可以用可能值区间表示：

对于值为a的变量v，R(v)=[a,a]。

实际上，“放弃不确定值”的方法是“可能值区间”方法的一个特例：

规定R(v)只有两类取值：

把整数算术运算和逻辑运算移到可能值区间上来。表4-2是可能值区间的基本算术运算，表4-3是可能值区间的基本逻辑运算。

算术运算的定义注： UA、UB、U分别为A、B和结果的上界 LA、LB、L分别为A、B和结果的下界
操作	取值
A+B	U=UA+UB L=LA+LB
A-B	U=UA-LB L=max{LA-UB,0}
A*B	U=UAUB L=LALB
A/B	Error: Divided by zero (UB==0) U=UA/LB (LB>0) \| INFINIT (LB==0) L=LA/UB (UB>0)

表4-2

逻辑操作的定义
操作	取值	*取值条件*
A==B	True	UA=LA=UB=LB
A==B	False	A*B==Null
A>=B	True	LA>=UB
A>=B	False	UA<LB
A>B	True	LA>UB
A>B	False	UA<=LB
A<=B	True	UA<=LB
A<=B	False	LA>UB
A<B	True	UA<LB
A<B	False	LA>=UB
A<>B	True	A*B==Null
A<>B	False	UA=LA=UB=LB
A<<B (Set)	True	A is a subset of B
A<<B (Set)	False	A*B==Null
A\|<B (Set)	True	A*B==Null
A\|<B (Set)	False	A is a subset of B

表4-3

可能值区间是部分保留变量信息的最简单方法之一。进一步扩展可以有：k-可能值区间方法。即，把变量v的可能值用k个区间表示。这样，避免一些不可能的取值进入算法记录的可能值集合里面。但k个区间有如何选取的问题，这涉及到最优求解等方法，可能会使问题复杂化。在实验中，我们只采用了可能值区间的方法，不再讨论k-可能值区间的方法。

值得指出的是：“放弃不确定值”和“可能值区间”都可能包含了一些实际上不可能出现的变量值，从而允许了一些不能发生的变迁。但根据被动测试的报错条件：被测实现工作出错是被动测试报错的必要而非充分条件，这是允许的。

4.3. 利用条件的“暗示信息”

4.3.1.“暗示信息”的利用

在被动测试中，测试器一开始并不一定能够知道被测实现对应的EFSM各个变量的值。被动测试算法需要在跟踪过程中不断发现变量的值。这主要有两条途径：一条是变迁动作，如果一个变量在某个变迁的变迁动作中被赋以一个确定的值，则该变量的值已知。另一条途径是变迁条件，如果某条变迁一定发生了，则该变迁上的变迁条件必须满足。比如，若变迁上有（v==c）的条件而且这条变迁被确定已经发生了，则变量v的值必然为c。本文称这种从变迁条件获取的信息为“暗示信息”。

4.3.2.基本运算提供的暗示信息

基本运算所能够提供的暗示信息如表4-4所示。

*单个逻辑运算符的暗示信息* 注： UA、UB分别为A、B的上界 LA、LB分别为A、B的下界
*逻辑运算*	*暗示信息*
A==B	UA=UB=min{UA,UB}; LA=LB=max{LA,LB}; e.c. A=B=A*B
A<>B	Null
A>B	UB=min{UB,UA-1} LA=max{LA,LB+1}
A>=B	UB=min{UB,UA} LA=max{LA,LB}
A<B	UA=min{UA,UB-1} LB=max{LB,LA+1}
A<=B	UA=min{UA,UB} LB=max{LA,LB}
A<<S	A=A[s.getSmallest..s.getLargest] e.c. A=AS
A-B	UB<=UA LA>=LB
A/B	UB>=LB>=1

表4-4

4.3.3. 暗示信息在算术运算中的传播

假设有一个条件：A+B==C。

现在A确定，B未知，C确定。此时， B=C-A也是已经确定的。由此可见，暗示信息可以在算术运算中传播。下面讨论一般的情况：

clearTraverse(ParseTreeNode* r)

{

    if （（r被暗示信息改变了）&&(r不是叶子节点)）

{

    if ((r的左子树确定)&&(r的右子树不确定))

{

    右子树的值=Rev(r的值，r的左子树的值，r的运算类型)

     clearTravers(右子树)

}；

}；

//类似的这里写一个修改左子树的

……

}

图4-1 暗示信息传播算法

不失一般性，假设一个算术运算表达式对应于一棵表达式树，树的叶子节点为常数或者变量值，树的非叶子节点为某个运算生成的临时结果（本文中，这棵树叫做表达式求值树）。则暗示信息可以沿着二叉树向叶子节点传播，当采用放弃不确定值描述变量值的时候，传播可以递归进行，直到叶子节点或者某个节点的两个子节点都是不确定的或者都是确定的为止。递归算法伪代码如图4-1所示。

Res=A <运算符> B

运算符

计算方法（求A）

计算方法（求B）

+

A=Res-B

B=Res-A

-

A=Res+B

B=A-Res

*

A=Res/B

B=Res/A

/

A=Res*B

B=A/Res

表4-5 Rev的计算方法

Rev的计算方法如表4-5所示。

当采用可能值区间描述变量值的时候，传播的规则与上表类似，只是对应的算术运算要用表4-2定义的那套运算规则。而且，A和B的新值应该是老值的子集（即，新值应该比老值获得更确定的信息）。

4.3.4. 复合逻辑运算中暗示信息的处理

不失一般性，假设逻辑表达式为析取范式(Disjunctive Normal Form)。根据被动测试的报错条件，分别对非、与、或三种关系运算讨论。

“非”(NOT)：从单个逻辑运算符的暗示信息可以看到，每个逻辑运算符都有对应的相反逻辑运算符。对于关系运算符NOT，只要把它修饰的逻辑式的逻辑运算符改成相反的逻辑运算符，并且去掉NOT符号即可。

“与”（AND）：AND两边的逻辑表达式都必须满足，所以，AND连接而成的合取项的暗示信息是每个基本逻辑表达式暗示信息的并集。因此，经过AND两边的暗示信息提示所生成两个新的变量可能值集合应该取交集。

“或”（OR）：OR两边的逻辑表达式满足一个即可，所以，OR连接而成的析取项的暗示信息是每个基本逻辑表达式暗示信息的交集。经过OR两边的暗示信息提示所生成两个新的变量可能值集合应该取并集。

综合上述三种情况，可以得到在复合逻辑运算中利用条件暗示信息的算法：

假设：变量组为VarSystem，记录各个变量的值。

1、把条件转换成析取范式

2、对NOT修饰的条件因子，把NOT去掉，并把因子中的逻辑判断符号取逻辑相反符号。

3、对每个析取项D_i，做：

A、复制varSystem到VarSystem_i

B、在VarSystem_i上面对D_i中的每一个条件因子进行检查，看是否能找到有用的暗示信息并改变变量的值

C、如果在B过程中由变量的值被修改，则转B

4、把每个析取项D_i生成的变量组VarSystem_i的每个变量做并操作，生成一个新的变量组

5、varSystem=新的变量组

6、算法结束。

最后生成的varSystem中，每个变量的可能取值范围是新输入的varSystem的子集。因为步骤3中每次对变量的改变，都只能使变量的可能取值区间变小。对于每个V_i有：。所以，。因此，通过利用暗示信息，变量的值只能是更加确定了。

摘要

关键字

Abstract