第３６卷第１２期计算机科学Ｖ０１．３６Ｎｏ．１２２００９年１２月ＣｏｍｐｕｔｅｒＳｃｉｅｎｃｅＤｅｃ２００９网络协议一致性测试研究综述朱雪峰１’２许建军３邹彪１张哲１孙雷１’２（中国石油大学（北京）计算机科学与技术系北京１０２２４９）１（地球探测与信息技术北京市重点实验室北京１０２２４９）２（中国标准化研究院北京１０００８８）３摘要一致性测试是网络协议验证中最为基本的部分。虽然大量的研究与实践对此问题做过深入的探讨，但是到目前为止，仍然缺乏系统、有效而实用的协ｉＫ－－致性测试方法。从协议一致性描述方法入手，分别从一致性测试的体系结构、方法以及测试生成技术等方面对协４Ｋ－－致性测试技术进行了综合研究，最后对其中存在的问题给出了基本解决思路。关键词网络协议，一致性测试，形式化方法中图法分类号ＴＰ３９３文献标识码ＡＮｅｔｗｏｒｋＰｒｏｔｏｃｏｌＣｏｎｆｏｒｍａｎｃｅＴｅｓｔｉｎｇ：ＡｎＯｖｅｒｖｉｅｗＺＨＵＸｕｅ－ｆｅｎ９１’２ＸＵＪｉａ州Ｌｌｎ３ＺＯＵＢｉａ０１ＺＨＡＮＧＺｈｅｌＳＵＮＬｅｉｌ・２（ＤｅｐａｒｔｍｅｎｔｏｆＣｏｍｐｕｔｅｒＳｃｉｅｎｃｅａｎｄＴｅｃｈｎｏｌｏｇｙ，ＣｈｉｎａＵｎｉｖｅｒｓｉｔｙｏｆＰｅｔｒｏｌｅｕｍ，Ｂｅｉｊｉｎｇ１０２２４９，Ｃｈｉｎａ）１（ＫｅｙＬａｂｏｒａｔｏｒｙｏｆＥａｒｔｈＰｒｏｓｐｅｃｔｉｎｇａｎｄＩｎｆｏｒｍａｔｉｏｎＴｅｃｈｎｏｌｏｇｙ，Ｂｅｉｊｉｎｇ１０２２４９，Ｃｈｉｎａ）２（ＣｈｉｎａＮａｔｉｏｎａｌＩｎｓｔｉｔｕｔｅｏｆＳｔａｎｄａｒｄｉｚａｔｉｏｎ，Ｂｅｉｊｉｎｇ１０００８８，Ｃｈｉｎａ）３ＡｂｓｔｒａｃｔＣｏｎｆｏｒｍａｎｃｅｔｅｓｔｉｎｇｉＳｆｕｎｄａｍｅｎｔａｌｔＯｔｈｅａｎａｌｙｓｉｓｏｆｎｅｔｗｏｒｋｐｒｏｔｏｃｏｌ，ｗｈｉｌｅｔｈｅｒｅａｒｅｌｏｔｓｏｆｗｏｒｋｏｎｒｅ－ｓｅａｒｃｈａｎｄｐｒａｃｔｉｃｅａｓｐｅｃｔｏｆｔｈｉｓｐｒｏｂｌｅｍ，ｗｅｓｔｉｌｌｌａｃｋａｓｙｓｔｅｍａｔｉｃａｌｌｙ，ｅｆｆｉｃｉｅｎｔｌｙａｎｄｕｓａｂｌｅｍｅｔｈｏｄｆｏｒｃｏｎｆｏｒｍａｎｃｅｔｅｓｔｉｎｇＯｆｎｅｔｗｏｒｋｐｒｏｔｏｃｏｌＢｅｇｉｎｉｎｇｗｉｔｈｔｈｅｆｏｒｍａｌｄｅｓｃｒｉｐｔｉｏｎｍｅｔｈｏｄｆｏｒｄｅｓｃｒｉｂｅｎｅｔｗｏｒｋｐｒｏｔｏｃｏｌ，ｗｅｓｕｒｖｅｉｅｄｎｍ—ｊｏｒｔｅｃｈｎｉｑｕｅｓｏｎｔｅｓｔｉｎｇａｒｃｈｉｔｅｃｔｕｒｅ，ｔｅｓｔｉｎｇｍｅｔｈｏｄａｎｄｔｅｓｔｉｎｇｓｅｑｕｅｎｃｅｇｅｎｅｒａｔｉｎｇｉｎｃｏｎｆｏｒｍａｎｃｅｔｅｓｔｉｎｇ．Ａｎｄｆｉｎａｌ—ｌＹ．ｇａｖｅｏｕｒｍｅｔｈｏｄｏｎｒｅｍａｉｎｉｎｇｐｒｏｂｌｅｍ．ＫｅｙｗｏｒｄｓＮｅｔｗｏｒｋｐｒｏｔｏｃｏｌ，Ｃｏｎｆｏｆｉｎａｎｃｅｔｅｓｔｉｎｇ，Ｆｏｒｍａｌｍｅｔｈｏｄ网络协议的一致性测试是一种功能性的黑盒测试，它根方法和形式化描述语言。据协议的描述对协议的某个实现进行测试，以判别此实现与１．１形式化描述方法所对应的协议标准是否一致。一致性测试包括静态测试和动目前，大量的形式化描述方法已不断提出并应用到实际态测试两类。静态一致性测试是将协议实现者向测试方提供的协议开发中。常用的形式化描述技术包括有限状态机、Ｐｅ－的“协议实现一致性声明”与协议中的静态一致性要求相比ｔ一网、进程代数、时序逻辑和构造类别代数等。较；动态一致性测试就是运行测试集对ＩＵＴ进行测试。有限状态机（ＦＳＭ）是一种最常见的模型，它具有直观、易协议一致性测试包括３个阶段：第一阶段是测试生成，为于实现的特点，能够很方便地与其它形式化方法进行组合。特定协议产生于所有协议实现的抽象测试集；第二阶段随着ＦＳＭ的广泛应用和发展，出现了很多扩展模型，主要包是测试实现，把抽象测试集中的测试例转换成在实际系统上括扩展有限状态机、确定有限自动机、通信层次化状态机、通可执行的测试例；第三阶段为测试执行，在特定的ＩＵＴ上执信有限状态机等。有限状态机模型存在的问题是：无法描述行测试用例，并且观察ＩＵＴ的外部行为结果，最后对ＩＵＴ与并发行为，不利于协议验证的实现；难以描述复杂的系统，在协议说明是否一致给出判定结果。进行大规模复杂协议的描述时，ＦＳＭ模型会面ｆ临状态爆炸的难题。１一致性测试的形式化描述技术Ｐｅｔｒｉ网是一种建立在并发概念基础上的、特殊的自动机形式化描述是一致性测试的基础。形式化方法建立在严模型，可以清楚地表达两个进程之间的通信，能够直观地表示格的数学基础上，可以精确而完整地表达协议的功能、性能及非确定性，可用于描述通信系统中异步成分之间的关系。Ｐｃ－行为等，它为协议的分析、验证、实现、测试等活动的系统化、ｔｒｉ具有一套成熟的数学理论工具，在通信领域特别是通信协自动化提供了良好的基础。形式化描述技术包括形式化描述议验证方面得到了广泛的应用。Ｐｅｔｒｉ网有多种扩展模型，包到稿日期：２００９－０１—２０返修日期：２００９－０３—２５本文受国家自然科学基金重大项目（６０４９６３２４）ｇ＇ｆｌ中国标准化研究院基本科研业务费支持项目（５６０７６Ｓ１５２４）资助。朱冒峰（１９７３一）。男，博士，讲师，ＣＣＦ会员，主要研究方向为形式化验证．Ｅ－ｍａｉｌ：ｘｕｅｆｅｎｇ．ｚｈｕ＠ｃｕｐ．ｅｄＬＬｃｎ！许建军（１９７４～），男，博士，副研究员；孙雷（１９７０一），女，副教授。万方数据・５・括数字Ｐｅｔｒｉ网和时间Ｐｅｔｒｉ网等。Ｐｅｔｒｉ网以其清晰直观的图形表示、坚实的数学基础和分析技术得到了广泛的应用，但是在描述大型复杂协议时，同样存在状态爆炸的问题。进程代数将协议描述成进程的集合，通过进程事件的集合和进程的迹来描述进程的行为，通过并发、选择、递归等来描述进程之间的关系。进程代数能够严密地表述协议的逻辑结构以及协议的时序性，而且有助于协议验证。ＲＭｉｌｎｅｒ提出的通讯进程演算（ＣＣＳ）和Ｃ八Ｈｏａｒｅ提出的通信顺序进程（ｃｓＰ）均基于进程代数理论。时序逻辑是模态逻辑的扩展，以状态为可能世界，以状态的演变次序关系为可能世界问的可达性关系。在时序逻辑描述中，使用辅助的时序算子定义时序逻辑公式，每个公式都是关于状态序列的一个断言；一个时序逻辑描述由一组时序公理组成，这些公理描述了从系统执行开始产生的所有状态序列都为真的性质；时序逻辑通过状态关联进行推理，它附加有与时间相关的操作属性。时序逻辑应用较为成熟，并且数学抽象能力很强，它侧重于通过定义系统外部可见的行为事件来描述系统，即直接描述系统的输入／输出行为，不关心协议实体的内部变化，比ＦＳＭ，Ｐｅｔｒｉ网更易于刻画协议的活动性，因而有利于对协议的各种性质进行分析验证；其缺点是协议描述的可读性差，协议描述复杂。构造类别代数是一种基于代数规范的形式化描述技术，通过定义构造函数或延拓函数来定义其可观察和可控制的行为，并通过定义公理集合来构造函数和延拓函数，即公理集合构成了协议行为的规范。构造类别函数的这种特性使得它非常适合于描述协议数据部分及其处理过程。这种类别代数的方法与基于有限状态机的方法类似，但是当状态机状态较多时，它比基于有限状态机的方法更容易描述协议并生成测试用例。１．２形式化描述语言国际标准化组织根据形式化描述方法提出了３种通信协议的形式化描述语言，分别是ＩＳ（）的ＥＳＴＥＬＩ。Ｅ，Ｌ０，ｒ０Ｓ和ＣＣＩＴＴ的ＳＤＩ．。ＥＳＴＥＬＬＥ是由ＩＳＯ组织专门为协议描述而设计开发的一种基于扩展有限状态机的形式化描述语言。它是ＰＡＳ—ＣＡＬ语言的扩充，其描述的协议很容易转换成ＰＡＳＣＡＬ或Ｃ代码，是一种面向协议实现的ＦＤＬ：模块实例可通过初始化语句动态产生，如果协议实现后模块实例对应于一个进程或任务，那么网络进程或任务也是动态产生的；模块之间的通信为异步通信。ＥＳＴＥＬＬＥ对并发、不确定性、超时、异步通信状态转移具有较强的表达能力，但是对于递规、共享通道、同步通信、协议性质的表示缺乏有力的手段。用ＥＳＴＥＬＬＥ描述的协议易于提取ＦＳＭ模型和Ｐｅｔｒｉ网模型，但不容易转变成时态逻辑模型和ＣＣＳ模型。ＬＯＴＯＳ是由ＩＳＯ组织开发的一种形式化描述语言。在基于ＬＯＴＯＳ的描述中，一个通信系统可以描述成一系列有时间顺序的、可由外部观察的事件。ＬＯＴＯＳ使用ＣＣＳ来描述进程的行为和交互，并且使用ＡＣＴＯＮＥ语言来描述数据结构和表达式。ＡＣＴＯＮＥ是一个抽象数据类型语言，它的数学模型是代数规范。ＬＯＴＯＳ语言存在一些扩展，如Ｄ－１２３－ＴＯＳ，Ｇ－ＬＯＴ（）Ｓ等。ＳＤＬ是由ＣＣＩＴＴ组织开发的基于ＥＦＳＭ的电信领域的・万方数据６・国际标准。ＳＤＬ存在两种表示方法：图形表示和语句表示。ＳＤＬ语言主要由以下几个部分组成：结构、行为和通信。ＳＤＬ是基于扩展有限状态机的形式化描述语言，可用于从需求分析到具体实现的整个开发过程，适用于具有实时反应的系统；用图形的形式表示，可视性好；具有面向对象的特征。基于ＳＤＬ的上述优点，ＳＤＬ主要用于实时交互分布式系统的形式化描述。２一致性测试体系结构抽象测试方法描述由下测试器、上测试器和测试协调过程组成的抽象测试结构以及它们与测试系统和ＳＵＴ的关系组成。一致性测试的抽象测试方法分为两大类：端系统的抽象测试方法和中继系统的抽象测试方法。２．１端系统ＩＵＴ的抽象测试方法根据不同的控制观察点，现有的端系统抽象测试方法可以分为４类，即本地测试法、协调测试法、分布测试法和远程测试法，如图１所示。二卜—哑引＾Ｓ９芒御匿器Ｉｌ●Ｎ－Ｉ，层服务提供者（Ｂ）本地测试法（ｃ）分布剥试法习…；型而刍ＩＴＭｐｊ上测试器十ＡｓＰＩ议实现Ｎ一１层服务提供者（ｂ）协调测试法（ｄ）远程测试法图ｌ端系统抽象测试方法本地测试方法是下测试器和上测试器都在测试系统中且在砌Ｔ的上层服务边界上有一个ＰＣＯ的抽象测试方法。协调测试方法是上测试器在ＳＵＴ中且为测试协调过程定义了标准化的ＴＭＰ，使得控制和观察（包括测试管理ＰＤＵ的控制和观察）仅用下测试器活动的术语说明的抽象测试方法。分布测试方法是上测试器在ＳＵＴ中且在ＩＵＴ的上层服务边界上有一个ＰＣＯ的抽象测试方法。远程测试方法是测试事件的控制和观察仅用下测试器活动的术语说明，且对测试协调过程的一些要求可能在ＡＴＳ中暗示或非正式地表达，但没有做关于这些要求的可行性或实现的假定的抽象测试方法。２．２中继系统１１５１＂的抽象测试方法开放中继系统的抽象测试方法包括两类：回环测试方法和穿越测试方法，如图２所示。驯意！二！星曼墨篓垡！（ａ）回环舅试方ｊ圭（ｂ）穿越测试方法图２中继系统抽象测试方法回环测试方法只需要一个测试器，但要求在被测实现或系统内部或外部链路上实现回环，而且其测试能力过于简单，因而不够实用。另外，被测中继系统只有一端的行为被直接观察到，而另一端的行为不能被正确地评价。穿越测试方法能够测试中继系统的全部中继功能，但需要至少两个测试系统。各测试系统之间的协调是实现穿越测试方法的困难所在，穿越测试方法则使被测中继系统在平常的操作模式下得到测试，在两端的行为都能够观察到。３测试生成方法协议测试方法中最主要的工作就是生成测试序列。目前，绝大多数一致性测试序列的生成算法都是基于ＦＳＭ模型的。基于有限状态机的测试方法基本过程如下：测试系统向ＩＵＴ施加输入事件序列，接收校验输出事件序列，检查状态转移；根据输出事件和状态的转移，判定ＩＵＴ的行为是否符合协议规范的描述。测试生成方法包括可达性分析与测试序列两种。３．１可达性分析可达性分析从一个初始状态出发，生成并检查系统能够到达的所有状态，以实现协议验证的自动化。可达性分析包括３种：全局搜索、控制下的部分搜索、随机仿真。３．１．１全局搜索全局搜索算法的主要思想是：首先从初始状态集Ｓｏ中取出一个状态ｓ，从初始状态集ｌｓｏ中删去ｓ并将ｓ加入到已分析状态集Ｓ７中；如果ｓ是一个错误状态，则报告出错；否则对于ｓ的每一个后继状态５７，如果５７不在初始状态集Ｓ。或已分析状态集Ｓ７中，则将ｓ７不放人初始状态集Ｓ。中，并递规地执行以上过程，最后从Ｓ中删除ｓ７。重复执行上述过程，直到初始状态集为空。算法中工作集Ｓ０控制系统状态空间树的搜索顺序。如果工作集Ｓ０中的状态以先进先出的顺序取出，那么算法执行的是状态空问树的宽度优先搜索；如果是以后进先出的顺序取出，则是深度优先搜索。全局搜索算法可以证明协议中没有错误，但是其应用范围有限，能够分析的最大状态数目依赖于协议、描述方法和可用的计算资源。当系统状态的数目非常大时，会发生状态空间爆炸。３．１．２局部搜索局部搜索与全局搜索基本类似，只是在后继状态的处理上选择的是某些后继状态，而不是像全局搜索那样选择每一个后继状态，这就是部分搜索最主要的特征。局部搜索只能用来证明错误的存在，无法证明不存在错误。与全局搜索算法相比，可以有效地解决状态爆炸的问题，这样就能利用有限的资源来验证协议中最重要的部分，从而最大限度地发现错误。缺点是必须能够预先判断出协议中错误的位置，然而这是无法预先做到的；另外，虽然这些方法能够减少状态空间的大小，但是它们都没有提供任何工具将状态空间的大小与可用内存相匹配。３．１．３分支搜索分支搜索的基本思想是：从一个初始状态出发进行判定；如果此状态为一错误状态，则报告出错，再从初始状态集中选择一个初始状态；否则选取此状态的一个后继状态，重复执行以上过程。分支搜索中，只选取当前状态下状态转换中的一条分支，因而算法相当简单。万方数据分支搜索算法与协议系统的大小和复杂性无关。对于复杂的验证问题，分支搜索是实际中唯一可用的方法。不足之处在于：首先，分支搜索没有明确的终止，无法判断是否已经访问过系统的所有可达状态；其次，由于没有算法的终止，也就无法判断是否已经发现了系统的所有错误。这种算法也只能发现错误，不能证明协议中没有错误。３．２测试序列方法目前协议测试方法都是在转移级别来做的，即针对ＦＳＭ中的单个转移生成相应的测试子序列，再将这些测试子序列连接起来作为完整的测试序列。设Ｍ是有限状态机，Ｍ一＜ｆ，Ｏ，Ｓ，Ｓｏ，丁）。吖是Ｍ的一个实现，则针对转移ｔ一（跏ｓｊ，ｉ／ｏ）的测试通常包括以下３步：（１）将ＩＵＴ从初始状态置成状态￥；（２）向ＩＵＴ输入激励ｉ，接收并核对ＩＵＴ的输出事件ｏ；（３）验证ＩＵＴ所到达的新状态是否为ｓｉ。通过以上３步得到转移ｔ的测试子序列，它由３部分组成。第一部分将ＩＵＴ从初始状态置成状态盅，称为路径序列ＰＳ（ｓｉ），该序列可以通过宽度优先搜索得到；第二部分就是待测转移ｔ的输入输出ｉ／ｏ；第三部分验证ＩＵＴ所到达的新状态是否为ｓｉ所采用的特征序列ＣＳ（目），该特征序列可以唯一地确定有限状态机的当前状态，后两部分合起来称为测试段。针对如何生成测试序列，主要的方法有以下几种。３．２．１Ｔ方法在一个有限状态机中，最直观的一种测试方法就是从初始状态出发，将其中所有的转移至少遍历一次，最终回到初始状态。转移回路方法相对于其它基于有限状态机的测试序列生成方法，具有简单、生成序列长度短的优点，并且这种方法仅要求有限状态机是强连通的，不必完全定义；但是这种方法在测试过程中只检查了转移的输出情况，没有对转移到达的状态进行检查，因而错误检测能力较低。３．２．２Ｄ方法对于一个输入序列，如果它分别作用于ＦＳＭ的每一个状态，从这些状态分别开始的输出均不相同，则称此输入序列为该ＦＳＭ的区分序列。Ｄ方法的基本思想就是利用区分序列来生成测试子序列的第三步。区分序列在状态确认上是一种非常有效的方法，但是这种方法不具有普适性：一方面，大多数有限状态机中不存在ＤＳ序列；另一方面，即使存在ＤＳ序列，其长度也可能太大而无法使用。３．２．３Ｗ方法针对Ｄ方法的缺陷，ｗ方法采用多个输人事件来确定状态。ｗ方法基于ｗ集和Ｐ集来构造测试序列，其中ｗ集是ＦＳＭ的输入序列的集合，其输出能够唯一标识状态；Ｐ集是使ＦＳＭ从初始状态到任意状态的输入序列的集合。ＩＵＴ的ｗ集合是一个包含ｋ个输人事件序列的集合。对于ＩＵＴ的各个状态来说，Ｗ集合是相同的，但是各个输入事件序列所产生的最后输出事件所组成的输出模式不同。如果Ⅳ集合包含ｋ个输人事件序列，那么需要对ＩＵＴ施加ｋ次测试，才能判定ＴＬＪＴ是否处于状态而，这样就大大加长了测试序列。但是相对于区分序列而言，Ｗ集合一般是存在的。（下转第３６页）・７・［７］ＦｒａｕｅｎｔｈａｌＪｃＭａｔｈｅｍａｔｉｃａｌＭｏｄｅｌｉｎｇｉｎＥｐｉｄｅｍｉｏｌｏｇｙ［Ｍ］．ＮｅｗＹｏｒｋ：Ｓｐｒｉｎｇｅｒ－Ｖｅｒｌａｇ，１９８０［８３ＺｏｕＣｃ。ＧｏｎｇＷＢ，ＴｏｗｓｌｅｙＤ．ＣｏｄｅＲｅｄＷＯＩＴｌｌｐｒｏｐａｇａｔｉｏｎｍｏｄｅｌｉｎｇａｎｄａｎａｌｙｓｉｓ［Ｃ］／／Ｐｒｏｃｅｅｄｉｎｇｓｏｆｔｈｅ９ｔｈＡＣＭＳｙｍ—ｐｏｓｉｕｍｏｎＣｏｍｐｕｔｅｒａｎｄＣｏｍｍｕｎｉｃａｔｉｏｎＳｅｃｕｒｉｔｙ．Ｗａｓｈｉｎｇｔｏｎ，２００２：１３８—１４７（上接第７页）３．２．４Ｕ方法区分序列和ｗ集合都是在有限状态机所处的状态完全未知的情况下对状态进行确定的一种方法，但是实际上，在测试子序列生成过程的第三步，对ｎＪＴ所处的状态有一个期望值町，在测试中只需要确定砌Ｔ的实际状态是否为ｓｉ。由此来看，区分序列和ｗ集合的状态确认能力相对于测试要求来说太强了，这就是Ｕ方法的基本出发点。ＩＵＴ状态而的Ｕ１０序列是ＴＵＴ所有其它状态不能表现的Ｉ／０行为，它唯一地标识状态￥。为了找出各个状态的ＵＩＯ序列，必须罗列出ｍＴ各个状态的Ｉ／０序列（一棵Ｉ／０序列树），从树的根部开始比较各个状态的Ｉ／０序列，直至为每个状态找到唯一的Ｉ／０序列为止。相对于Ｄ方法和Ｗ方法，Ｕ方法能够生成更短的测试序列，并且Ｌ兀０在大部分的有限状态机中是存在的，因而其３．３测试序列到抽象测试集的转换测试集可分为通用测试集ＧＴＳ、抽象测试集ＡＴＳ和可执行测试集ＥＴＳ。测试生成阶段得到的测试序列属于通用测试集的初级阶段，需要经过规范化转换到通用测试集。采用适当的测试描述法描述通用测试集就能够得到抽象测试集；输人到特定的测试系统并结合被测协议实现信息就能够得到针对该实现的可执行测试集。实际测试时，把自动生成的测试序列按照相当确定的测试目标进行分解，得到针对每一个测试目标的测试子序列，在测试子序列的基础上构造每一个测试例。分析每一个测试子序列，找到其明确的测试点（比如测试一个状态、一个变迁等），对子测试序列进行分割，把从子序列起始位置到测试点的初始位置作为前测试步序列，完成测试驱动和状态验证的剩下部分作为测试体序列。根据子序列执行后的最终状态，添加能够使被测协议转换到初始状态的后测试步序列。三部分序列组合起来，得到针对特定测试点的完整的测试序列。采用适当的测试描述法对上述得到的测试序列进行描述，就的测试例，就能够组合成抽象测试集。４测试实现和测试执行在测试实现阶段，根据协议实现的ＰＩＣＡＳ和ＰＩＸＩＴ从一致性测试集中选取适当的测试例，去除没有意义的测试，并使用ＰＩＸＩＴ提供的信息来量化这些测试例。从抽象测试集生成可在一实际的测试系统上执行的参数化的可执行测试集，即可在特定测试设备上对某个ｍＴ进行测试运行的测试集。４．２测试执行在测试执行阶段．一个特定的ⅢＴ被实际测试，并得出・３６・万方数据［９］ＹｏｕＣＣ，ＴｏｗｓｌｅｙＤ，ＧｏｎｇＷ．ＯｎｔｈｅｐｅｒｆｏｒｍａｎｃｅｏｆＩｎｔｅｒｎｅｔＷＯｒｍｓｃａｎｎｉｎｇｓｔｒａｔｅｇｉｅｓ［Ｊ］．ＰｅｒｆｏｒｍａｎｃｅＥｖａｌｕａｔｉｏｎ，２００６，６３：７００－７２３［１０］ＺｏｕＣＣ，ｅｔａ１．ＴｈｅｍｏｎｉｔｏｒｉｎｇａｎｄｅａｒｌｙｄｅｔｅｃｔｉｏｎｏｆＩｎｔｅｒｎｅｔｗｏｒｍｓ［Ｊ］．１ＥＥＥ／ＡＣＭＴｒａｎｓａｃｔｉｏｎｓｏｎＮｅｔｗｏｒｋｉｎｇ，２００５，１３（５）：９６１—９７４砌Ｔ一致性判定结果。测试执行过程分为两步：第一步是静态一致性需求检查，根据协议标准的静态一致性需求对ⅣＴ的ＰＩＣＳ进行检查；第二步为在测试器上执行测试例来检查ＩＵＴ对动态一致性要求的满足程度，对每个测试例做出测试判断：通过、失败或不确定。最后，静态一致性检查的结果和所有的测试例的执行判定结果组合在一起，形成一个有关ＩＵＴ的一致性判决。当且仅当所有的测试都未失败时，最终的判决才会是通过。现有的测试执行方法可划分为两类：基于编译的测试执行（ＣＴＥ）和基于解释的测试执行（ＩＴＥ）。基于编译的测试执行，是指在测试执行之前，由抽象测试集ＡＴＳ到可执行测试集ＥＴＳ的转换已经由转换器或编译器完成，这一过程非常耗时，但是提高了测试执行的效率。在基于解释的测试执行中，从ＡＴＳ到ＥＴＳ的转换是在测试执行过程中完成的，这种方法使得用户可以对测试过程进行动态观察和控制，但测试执行的效率较低。结束语协议一致性测试所面临的挑战是双重的。一方面，随着协议的全方位发展，协议的功能越来越强，协议的复杂性也越来越高，使得协议的一致性测试变得越来越困难；另一方面，随着形式化验证技术的发展，对于协议一致性的验证必然会面临如何提高形式化验证的效率的问题。目前一致性测试的研究和实践中需要解决的几个关键问题包括测试理论的形式化、高速计算机网络协议和路由协议的测试、通用测试平台的研制。所有这些都需要新的、高效可行的形式化验证技术的支持。我们认为，面对协议一致性测试领域的困境，形式化的领域本体可能会对协议的形式化验证起到关键的作用，我们未来的工作将主要沿着这条路径展开。参考文献［１３ＺｈａｎｇＹ．ＬｉｚＡＮｅｗＦｏｒｍａｌＴｅｓｔＳｕｉｔｅＳｐｅｃｉｆｉｃａｔｉｏｎＬａｎｇｕａｇｅｆｏｒＩＰｖ６ＣｏｎｆｏｒｍａｎｃｅＴｅｓｔｉｎｇｌ－Ｃ］ｆｆＰｒｏｃｅｅｄｉｎｇｓｏｆＩＣＣＴ２００３．２００３：１７４－１７７［２３ＷｕＪ，ＳａｍｕｅｌＴ，ＧａｏＱＦｏｒｍａｌＭｅｔｈｏｄｓｆｏｒＰｒｏｔｏｃｏｌＥｎｇｉｎｅｅｒ—ｉｎｇａｎｄＤｉｓｔｒｉｂｕｔｅｄＳｙｓｔｅｍｓ［Ｍ］．ＫｌｕｗｅｒＡｃａｄｅｍｉｃＰｕｂｌｉｓｈｅｒｓ，２００１［３３ＴｉａｎＪ，Ｌｉ乙ＴｈｅＮｅｘｔＧｅｎｅｒａｔｉｏｎＩｎｔｅｒｎｅｔＰｒｏｔｏｃｏｌａｎｄｉｔｓＴｅｓｔ［ｃ］／／ＰｒｏｃｅｅｄｉｎｇｓｏｆＩＥＥＥＩｎｔｅｒｎａｔｉｏｎａｌＣｏｎｆｅｒｅｎｃｅｏｎＣｏｍｍｕ—ｎｉｃａｔｉｏｎ．２００１：２１０－２１５［４］ＺｈａｎｇＦ，ＣｈｅｕｎｇＴ．ＯｐｔｉｍａｌＴｒａｎｓｆｅｒＴｒｅｅｓａｎｄＤｉｓｔｉｎｇｕｉｓｈｉｎｇＴｒｅｅｓｆｏｒＴｅｓｔｉｎｇＯｂｓｅｒｖａｂｌｅＮｏｎｄｅｔｅｒｍｉｎｉｓｔｉｃＦｉｎｉｔｅＳｔａｔｅＭａ—ｃｈｉｎｅｓ［Ｊ］．ＩＥＥＥＴｒａｎｓａｃｔｉｏｎｓｏｎＳｏｆｔｗａｒｅＥｎｇｉｎｅｅｒｉｎｇ。２００３，２９（１）１１－１４［５］朱雪峰，金芝．关于软件需求中的不一致性［Ｊ］．软件学报．２００５，１６（７）：１２２１—１２３２适用范围更广。得到一个完整的测试例。如此构造出针对每一个特定测试点４．１测试实现
