（计算机软件与理论专业论文）协议的动态测试.pdf

摘要网络技术在近二三十年来飞速发展，随着i n t e m e t 的迅速普及，网络规模不断扩大，不幸的是，随着网络规模的增加，出现问题的可能性也在增加，这就对通信协议测试技术提出了巨大的挑战。传统的通信协议测试方法是根据一定的测试序列生成算法生成测试集，按照静态的固定的顺序对协议实现进行测试，一般称这种测试方法为“静态测试”。但是这种测试方法忽略了测试过程之中的反馈，存在测试效率和测试覆盖率相对较低的问题。“动态测试”是另一种测试思想：在已生成测试集的基础之上，在测试过程之中根据测试的阶段性结果对测试顺序进行重组，并进一步重新生成有效的测试序列，以期提高测试效率和测试覆盖率。本文研究了有限状态机模型上动态测试的一些理论和方法，本论文的主要工作包括：1 、测试序列动态排序的问题：在某些情况之下，测试并不需要运行所有的测试序列：测试目的为检测出第一个错误。此时测试代价只是检测出第一个错误之前执行的澳0 试序列代价。明显的，对于每一种特定的错误，都存在一种最优的排序，使第一个错误晟早的出现。但是这样将导致不同的错误对应不同的排序，而实际测试中不可能事先知道是什么错误，所以从平均效果来看，任何一种静态排序方法都不会导致最小的测试代价。因此提出动态排序方法，即在测试中不事先指定测试顺序，而是根据已经测试过的试结果来动态安排剩余的测试子序列的测试顺序。本文给出了三种动态重排序算法，分别针对多错误情况、单错误情况和对测试效率要求高并且测试机计算能力较强的情况。2 、测试序列动态生成的问题：引导序列和验证序列与待测转换存在依赖关系，e i i ji 导序列和验证序列会对待测转换的测试子序列产生影响。为了解决这个问题，本文提出两种方案，来避免错误的转换对待测转换测试序列的影响。关键词：协议一致性测试：静态测试；动态测试；有限状态机a b s t r a c tr e c e n ta d v a n c e si nc o m m u n i c a t i o n ss o f t w a r eh a v ee n l a r g e da n dc o m p l i c a t e dc o m m u n i c a t i o np r o t o c o l s t oi n c r e a s et h er e l i a b i l i t yo fs u c hp r o t o c o l s t e s t i n gt e c h n i q u e se n s u d n gt h a tap r o t o c o li m p l e m e n t a t i o nc o n f o r m st oi t ss p e c 蹰c a f i o na r en e c e s s a r y 1 1 1 et r a d i t i o n a lt e s t i n gm e t h o di sf i r s t i yg e n e m t e st e s t i n gs e q u e n c e sb ys o m eg e n e r a t i o na l g o r i t h m t h e na p p l yt h e s et e s t i n gs e q u e n c e st oi u to n eb yo n ea s as t a t i co r d e r t h i sm e t h o di sc a l l e d ”s t a t i ct e s t i n g ”b u tt h i sm e t h o di g n o r et h ef e e d b a c ki nt h ep r o c e s so fa p p l y i n gt e s t i n gs e q u e n c e st oi u t a n dh a st h ed i s a d v a n t a g eo fl o wt e s t i n ge 俪c e n c ea n df a u l tc o v e r a g e 。d y n a m i ct e s t i n g ”i sad i f f e r e n tt e s t i n gm e t h o d ：b a s e do nt h et e s t i n gs e q u e n c e sa l r e a d yg e n e m t e d ，t h em e t h o do r d e r st h e s et e s t i n gs e q u e n c e sd y n a m i c a l l yb yt h el o c a lv e r d i c t so ft h ep r o c e s so ft e s t i n g ，f u r t h e rm o r e t h em e t h o dg e n e r a t e sn e wa v a i l a b l et e s t i n gs e q u e n c e s i nt h i p a p e r s o m er e s e a r c ho nt h e o r ya n dm e t h o d so fd y n a m i ct e s t i n ge a s e do nf s m ( f i n i t es t a t em a c h i n e ) m o d e li sd o n e t h ec e n t d b u t i o n so ft h i sp a p e r , i n c l u d et h r e em a i np a r t s ：1 t e s ts e q u e n c er e o r d e r i n g ：t e s t e rd o e s n tn e e da l lo ft h er e s u l t so ft e s t i n gs e q u e n c e su n d e rs o m es i t u a t i o n t h ep u r p o s eo ft e s t i n gi sm e e tt h ef i r s tt e s tf a u l ta ss o o na sp o s s i b l e s ot h et e s tc o s ti st h ec o s to fa l lt h et e s t i n gs e q u e n c eb e f o r ef i r s tt e s tf a u l ti sm e t a p p a r e n t l ye a c hf a u l tc o n d i t i o nh a si t so w no p t i m a lt e s t i n go r d e r b u ti np r a c t i c a lt e s t i n g ，t h ef a u l tc o n d i t i o nw i l ln e v e rb ek n o w nb e f o r et e s t i n g s oe a c hs t a t i ct e s t i n go r d e rc a nn o tr e s u l t st h em i n i m a lt e s t i n gc o s ta v e r a g e l y an o v e lm e t h o dw h i c hr e o r d e r st h et e s ts e q u e n c ed y n a m i c a l l yi sp r o p o s e d t h r e ed y n a m i c a l l yr e o r d e n n ga l g o r i t h m sw e r ep r o p o s e dd e p e n d i n go nd i f f e r e n tf a u l tc o n d i t i o n s 2 t e s ts e q u e n c ed y n a m i c a l l yg e n e r a t i o n ：t r a n s t i o n si np r e a m b l ea n dp o s t h l es u b - s e q u e n c eh a se f f e c tt ot h et r a n s i t i o nt ob et e s t e d s ot e s ts e q u e n c ew i l lg i v eu n a v a i l a b l ea n dw r o n gr e s u l tb e c a u s eo ft h i s i td e d u c e st h et e s te f f i c i e n c ea n df a u l tc o v e r a g e t os o l v et h i sp r o b l e m t h i sp a p e rp r o p o s et w om e t h o d st oa v o i dt h ee f f e c tf r o mp r e a m b l ea n dp o s t b l es u b - s e q u e n c et ot h et r a n s i t i o nt ob et e s t e d k e y w o r d s ：p r o t o c o lc o n f o r m a n c et e s t i n g ；s t a t i ct e s t i n g ；d y n a m i ct e s t i n g ；f i n j t es t a t em a c h i n e ；第一章绪论1 1 研究背景近年来，随着计算机通信与网络技术的飞速发展，特别是开放型异构的互连，分布式系统的功能越来越多，所提供的服务越来越丰富，不同系统的互通能力和互操作能力也越来越强，这一切都使得通信协议的种类和数量越来越多，其规模和复杂性也越来越大。通信协议是计算机网络和通信网络中各种通信实体或进程之间相互交换信息所遵守的一组规则，它是计算机网络、多机系统的灵魂。同时，协议的开发也变得越来越困难，其复杂性主要表现在：网络软件规模不断扩大，开发周期不断延长：潜在错误增多，排除困难：协议标准化难以保障；软件移植性较差；软件可维护性降低等等。研究表明，数据通信领域目前正在发生两个转变，一个是通信协议日趋复杂，其二是网络环境中，数据通信涉及到越来越多的设备供应商和服务提供商。因此，协议开发过程中的任何一点缺陷都会给通信系统的稳定性、可靠性、安全性，容错性以及系统之间的互联互通带来巨大的危害。为了设计出功能上正确可靠、逻辑上一致完整的通信协议，并且将其有效地实现，在协议的开发过程中，需要采用一体化、形式化的方法，这种开发过程称为协议工程【1 】【2 】【3 1 。- 协议工程是以通信协议为研究对象的软件工程，但是它具有一套比现有软件工程一般的方法更加严格的协议设计方法，是一个一体化、系统化和形式化的协议开发过程。协议工程包括：协议设计、协议描述、协议验证、协议实现、协议测试和协议维护【4 】【5 卜协议描述阶段是对自然语言表达的协议进行形式化描述，研究如何用数学模型来精确描述协议，主要解决用自然语言描述协议的不精确和二义性问题；协议验证技术是采用数学方法来证明协议的形式化描述中不存在逻辑错误，如死锁，活锁，不可达等等；协议的实现则是将协议文本或者协议的形式化描述变换成计算机可执行代码的过程；协议测试包括一致性测试、性能测试、互操作性测试和坚固性测试，一致性测试是所有测试的基础；协议的一致性钡试是检查协议实现与协议规范是否一致的过程，是保证协议实现能够按照协议规范准确工作的重要步骤。针对一致性测试的测试策路一般分为两种，静态策略和动态策略。传统的测试都使用静态策略，即使用一定的测试序列生成算法得出测试套之后，按照一种事先规定好的顺序静态的执行。而动态策略早在1 9 9 2 年就被c h a n s o n 提出来【3 1 ，在测试执行中测试例的执行顺序并不是一开始就定义好的，而是根据不同的需求和情况进行动态的调整，在很多的情况之下都具有很好的测试效果，但是直没有得到足够的重视。本文正是从这个角度出发，对一致性测试中的动态测试进行一些理论研究。结果表明较之传统的静态测试具有较大的改进。1 2 研究现状1 2 1 一致性测试协议一致性测试的研究最早于1 9 7 9 年由英国国家物理实验室( n a t i o n a lp h y s i c a ll a b o m t o r y ：n p l ) 展开。1 9 8 3 年，n p l 开始了基于o s i 模型的协议形式化和一致性测试的标准化工作。协议一致性测试经过2 0 来年的发展取得了很大的进展。国际标准化组织i s 0 也专门制定了一个国际标准o s l 的i、一一致性测试方法与框架，这个标准由1 9 8 7 年的5 部分【2 4 】，已经扩展为1 9 9 4 年的7 部分【2 5 1 。协议一致性测试的过程参见1 1 。其中形式化描述和测试序列生成已经具有很成熟的理论。协议形式化描述方面，常用的形式化模型有有限状态机( f i n i t es t a t em a c h i n e ：f s m ) 及其扩展模型1 6 】、p e t r i 网( p e t r in e t ：p n ) 网、时序逻辑( t e m p o r a ll o g i c ：t l ) 【8 1 【9 1 【1o 】、通讯进程演算( c a l c u l u so fc o m m u n i c a t i n gs y s t e m ：c c s ) 【1 1 1 2 等；常用的形式化描述语言有l o t o s 2 0 2 1 2 2 、e s t e l i e 1 9 、s d l 2 3 和m s c 等。在测试序列生成方面，主要有t 方法【2 7 1 、d方法【2 8 1 、u i o 方法1 2 9 】和w 方法【3 0 】。它们都是基于有限状态机模型的。1 2 _ 1 1 测试框架i s o ，i e c9 6 4 6 国际标准的诞生是协议一致性测试领域的重要里程碑，它为协议的一致性测试提供了基本框架。如下图所示：图1 1 一致性钡4 试基础框架其中i u t ( i m p l e m e n t a t i o nu n d e rt e s t ) 为待测协议实体，它通过观察控制点p c o ( p o i n t so fc o n t r o la n do b s e r v a t i o n ) 与外部环境交互：u t 为l u t的服务使用者，与i u t 交换( n ) a s p ( a b s t r a c t s e r v i c ep r i m i t i v e s ) ；l t 为l u t的对等实体，与i u t 交换c n ) p d u 。实际通信中( n ) p u d 最终编码为( n 一1 )a s p ，然后与i u t 进行交互，不过i s o i e c9 6 4 6 中允许在抽象测试例中直接定义p u d 的内容格式，因此，我们可以认为l t 是直接与i u t 通过( n ) p d u 进行交互的。l t 与u t 之间通过测试协调进程t c p c t e s tc o o r d i n a t i o np r o c e d u r e )来协调测试中两者的同步问题和控制问题。测试的控制者可以是u t ，也可以是l t 。1 2 1 2 测试方法根据控制观察点( p c o ) 放置的不同，一致性测试可以分为四种方法。如图1 2 所示：a 本地测试法b 分布测试法pc 协调测试法d 远程测试法图1 2 协议一致性测试的四种方法本地测试：u t 位于测试系统内部，它与i u t 间的p c o 为标准的硬件接口。t c p 在测试系统内部实现。分布式测试：u t 位于被测试系统内部，它与i u t 间的p c o 为用户界面或编程语言接口。协调测试：u t 位于被测试系统内部，但u t 与i u t 问没有p c o 。u t 执行有关的测试管理协议( t e s tm a n a g e m e n tp r o t o c o l ：t m p ) ，与l t 交换 im p协议数据单元来实现t c p 。远程测试：没有u t ，需要通过设置被测系统( s u t ) 来实现简单的u t 功能。远程测试是实际测试中最常使用的一种测试方法。1 2 1 3 测试过程致性测试过程是评估待测实现或待测系统与一个或者多个i u l - _ t 建议或者国际标准相一致的所有一致性测试活动的全过程，如图1 3 所示，整个测试过程可以分为三个阶段：1 、测试准备包括：a ) 根据待测实现或者待测系统产生系统一致性声明( s c s ) ，协议实现一致性声明( p i c s ) 和协议实现附加信息( p i x i t ) ：b ) 根据协议文档选择抽象测试方法，并产生抽象测试集( a t s ) 。待测集是否完备决定了测试质量：c ) 选择测试方法。2 、测试操作由四个步骤组成，是协议一致性测试过程的核心部分：a ) 静态一致性检查。分析i u t 的p i c s 与有关标准指定的静态一致性要求是否相一致：b ) 测试例选择和参数化。测试集中的测试例不一定都适合所有的i u t ，应该根据协议实现一致性说明( p i c s ) 和协议实现附加信息( p i x i t )选择适当的测试例，并使用p i x i t 提供的信息来量化这些测试例，从a i t s 生成可执行测试集( e t s ) ，最终产生参数化的可执行测试集；c ) 动态测试。执行e t s ，并记录有关的测试信息。动态测试包括三种类型：基本互连测试、能力测试和行为测试；d ) 结果分析。测试结果是在测试过程中发生的系列可观察的事件，包括对i u t 的所有输入输出。测试结果分为两类：可预见的和不可预见的。可预见的测试结果是在抽象测试用例中定义过的，也就是说，观察到的事件符合抽象测试用例中的测试序列。一个可预见的测试结果对测试用例做出的判定有三种：通过、失败、无法判定。不可预见的测试结果在抽象测试用例中没有定义过，也就是说，观察到的事件不符合抽象测试用例中的事件序列。它意味着一个测试用例的错误或者是非正常的测试用例终止。3 、测试报告生成。根据分析结果产生系统一致性测试报告( s c t r ) 和协议一致性测试报告( p c t r ) 。图1 3致性测试过程1 2 1 4 测试集合如图1 _ 4 所示，一致性测试集合具有一定的层次结构：测试组、测试例、测试步和测试事件。测试事件是测试集中的晟小单位，它描述测试系统与i u t 交互的单个事件，如从i u t 接收p d u 或a s p 。多个测试事件按照一定的次序组合在一起可以组成测试步。测试步相当于编程语言中的子程序，用于提高代码的利用率。测试例是整个测试集中比较重要的一层。每个测试例都具有专门的测试目的，用于验证i u t 是否具有某种要求的能力，如支持某种大小的数据包，或是否表现了某种要求的行为，如在特定状态下发生特定事件时做出期待的响应。一般，测试例有当前测试步、测试体和后测试步三部分组成。前测试步将i u t 从一个稳定状态引导至该测试例所需的初始状态：测试体组织相关测试事件或( 和)测试步完成要求的测试验证；然后由后测试步将i u t 引导至另一个稳定的测试状态，为下一个测试例的执行做准备。为了方便阅读和管理，可以根据测试目的的不同，把测试例划分到不同的测试组中。原则上一个测试组可以具有任意的深度，即包含任意层测试组。测试套的描需要特定的语言。i s o ，i e c9 6 4 6 国际标准制定t t c n 语言用于描述测试套，并在i s o ，| e c9 6 4 6 - 3 中进行了详细的描述。除t t c n 外还有其他不同种类的测试套描述语言，如t c l 等。详细请参见1 2 5 。图1 4 一致性测试集结构1 2 2 形式化描述为了解说的方便，几乎所有的协议规范都是采用自然语言来描述，有时考虑到直观性，也会借助图表。但是采用非形式化( 自然语言) 和半形式化( 图表)方法描述协议存在不精确、有歧义和不易验证等缺陷。而采用形式化描述技术f d t ( f o r m a ld e s c r i p t i o nt e c h n i q u e ) 则能比较好的克服这些不足，充分表述协议的各种特性和体系结构，为协议的验证、实现以及一致性测试提供良好的基础。形式化描述方法不仅可以用来描述和定义一个系统的行为和动作，而且可以用来验证和测试一个系统设计和实现是否满足一个系统功能的要求。形式化方法以严格的数学为基础，使人们能够以精确的方式表示概念，证明规范和设计的性质，并且在开发出软件产品之前就能对产品的行为进行推理，因而形式化方法对保证软件产品的正确可靠性有重要的作用。采用形式化描述描述协议可以带来以下好处：1 、使用形式化技术所描述的协议规范是精确的：2 、可以通过严格的分析来确定给定规范的完整性和一致性；3 、可以编写一个合适的编译器处理形式化规范生成一个协议的部分协议实现：4 、协议形式化规范可以作为自动验证和自动一致性测试的基础；5 、形式化描述可以作为一个协议的形式化文档；6 、协议设计者可以使用形式化描述技术来描述协议，这样就可以和协议实现者建立一个精确的联系；一般来说协议的形式化特性应该包含以下五个方面的内容：1 、活动性( a c t i v i t y ) ：协议的活动性是指协议运行时一些好事情会发生。这些好事情包括：预定的事件会发生，制定的协议状态会到达，应该进行的协议行动会进行等。协议的活动性体现在终止性和进展性两个方面，或者说，如果协议有终止性和进展性，它就具有活动性i 终止性是指协议从任何二- 个状态开始运行，总能正确的到达指定状态，如果协议的某个状态不可达，则表明协议有错误。2 、安全性( s a f e t y ) ：协议的安全性是指协议运行时没有坏事情出现。这些坏事情包括：不可接收的事件，不可进一步向前的状态，错误的行为，错误的条件，变量越界等。坏事情一般导致死锁( d e a d l o c k )或活锁( 1 i v el o c k ) 。死锁是指协议阻塞在某个状态而无法前进，活锁是指协议作没有意义的循环。3 、有界性：检验协议的某些属性或参数的值是否有界。4 、完整性：检验协议是否缺少应有的处理，是否有不期待的接收等。5 、可恢复性或自同步性：当出现差错后，协议是否能在有限步骤内返回正常状态( 包括初始状态) 下执行。正是由于协议形式化描述是协议工程的核心内容，国内外已经有许多学者对这一课题进行了研究，大量的形式化描述方法不断被提出并应用到实际的协议开发中。常用的形式化描述技术包括：有限状态机( f s m ) 及其扩展模型、p e t r i网模型、时序逻辑( t l ) 、通信进程演算( c c s ) 、通信顺序进程( c s p ) 及构造类别代数等。下面讨论几种最常用最重要的模型。1 2 2 基本有限状态机有限状态机( f i n i t es t a t em a c h i n e ：f s m ) 无疑是最为重要的一种形式描述技术，它是其它很多形式化方法的基础。这主要是由于它直观性强，可以实现与其它形式方法的组合和转换，而且它易于自动实现。一个有限状态机可以采用状态转移图、状态转移矩阵或状态转移表等多种方法来表示，其中最常用的是状态转移图，它的顶点代表状态，有向边代表状态转移，每一条有向边上都标记了输入和输出。f s m 模型包括基本f s m 、通信有限状态机( c o m m u n i c a t i n gf i n i t es t a t em a c h i n e ：c f s m ) 和扩展有限状态机( e x t e n d e df i n i t es t a t em a c h i n e ：e f s m ) 等等。f s m 由于简单直观而得到广泛应用，但它也有诸多缺点：不利于协议验证的实现，难于描述复杂的系统，当进行大规模复杂协议的描述时，f s m 模型将会面临状态爆炸的难题。有限状态机( f i n 舱s t a t em a c h i n e ：f s m ) ：一个有限状态机 彳是一个六元组：m = ( j ，d ，s ，s o ，j ，五) ，其中j ：为有限的输入集合 ，之， ，允许包含空事件，以“- ”表示；o ：为有限的输出集合 d l ，0 2 ， ，允许包含空事件，以匕”表示；s ：为有限的状态集合 ，焉，) ，其中s o 为初始状态；s o ：为初始状态；占：s ，寸s 是状态转移函数；a ：s x j o 是输出函数。状态转移函数占和输出函数a 共同定义了状态的转换集合t ( 因此，有限状态机也可以看作是一个五元组m = ( j ，o ，s ，s o ，r ) ) ，其中每个元素可以表示为一个三元组f = ，其中s 称为转换f 的头状态，i e 门姐o = 兄( 暑，i ) 0分别称为转换t 的输入和输出，s ，= 占( 置，f ) s 称为转换f 的尾状态。我们用墨卫生s ，表示有限状态机肘处于状态时接受输入，使状态转移到s ，并且产生输出o 。当有限状态机处于状态j 时，如果收到一个输入激励i ，则将要进入新的状态占( b i ) ，同时产生输出z ( s i ) 。一个有限状态机可以采用状态转移图来表示，它是一个有向图g = ( y ，e ) ，其中顶点集合v = v i ，v 2 ，h ，对应着f s m 的状态集合s ，有向边集合e = n ，v j ；i k o ) ：v j ，o5 y ，t ，o m o n i e nf s m 的转移，表示在状态一在接收到输入之后，迁移到状态叶，同时输出d 肺。当使用有限状态机模型描述一个协议规范时，状态是协议实体能够停留的稳定条件，输入是协议实体从外界接收到的报文激励或者内部产生的事件激励，输出是协议实体对外界的响应。有限状态机还可以用状态转移表来描述，每行代表一个状态，每列代表一个输入激励，状态和输入激烈相交的出口为相应的输出和目的状态。如图1 - 5 所示，( a ) 为一个f s m 的状态转移图，( b ) 为对应的状态转移表。该f s m 具有四个状套 ，s 。，是，毛 ，两种输入 ，1 2 ，三种输出 0 1d ：，0 3 ；。i t 0 a ) f s m 的状态转移图b ) f s m 的状态转移表图1 - 5f s m 的状态转移图表示和状态转移表表示下面介绍几个和有限状态机相关的基本概念。等价状态：令f w 是一个有限状态机m = ( ，o ，s ，s o ，正a ) ，如果存在状态最s ，0 s ，使得这两个状态对于任意的输入序列都产生相同的输出序列，则称状态蕊墼，籍| | l _煦m一诬s ? 秘s ? 等钕。完全定义的状态机：令m 是一个有限状态机m = ( ，0 ，s ，s o ，万， ) ，如果对于任意状态s i s 和任意的输入f i ，都存在转换t = ，则称状态机m 是完全定义的状态机，反之则称m 是非完全定义的状态机。一般协议实体对应的状态机都是非完全定义的状态机，但我们可以通过添加头状态和尾状态相同，且输出为空的自循环转换来将非完全定义的状态机补齐为完全定义的状态机，一般将这种添加的自循环转换称为非核心转换，其他的称为核心转换。最小化的状态机：令m 是一个有限状态机m = ( ，0 ，s ，s o ，5 ，五) ，如果m 中不存在等价的状态，则称状态机m 是最小化的状态机。路径：假设m 是一个有限状态机，状态暑s ，s j s ，。如果存在转换序列，f 2 ，使得( 1 ) s s 为转换 的头状态：；( 2 ) 对于2 k i q ，转换的头状态是转换“的尾状态；( 3 ) s j 为转换的尾状态：则称转换序列 t 2 ，是一条从墨至l j s j 的路径。强连通有限状态机：假设j w 是一个有限状态机，对任意状态s s ，s ，如果均存在从丑到5 ，的路径，则称m 是一个强连通的有限状态机。一般将有限状态机m 用一个图g = ( 矿，切来表示，图的顶点集合矿代表状态机m 的状态集，图中的边集合代表m 的转换集合，边上的标号是对应转换的输入，输出。图2 1 给出了一个例子，该状态机是一个最小化的完全定义的状态机。图1 _ 6 有限状态机模型非确定有限状态机( n o n - d e t e r m i n i s t i cf i n i t es t a t em a c h i n e ：n f s m ) ：令m 是一个有限状态机m = ( ，0 ，墨，j ，丑) ，如果存在状态s s 和输入f i ，使得转换集合中存在两个或者以上的转换的头状态均为s ，输入均为，形式化的表示为，丑s ，f j 使得( i j ( s ，圳2 ) v q 五( s ，刮2 ) ，则称m 为非确定的状态机，反之m 为确定的状态机。可以将一个非确定的状态机转换为一个确定的状态机，所以本文中如未特别指明，一般的状态机都指的是确定的状态机。1 2 2 2 有限状态机的扩展1 2 2 2 1 扩展有限状态机( e x t e n d e df i n i t es t a t em a c h i n e ：e f s m )一个扩展有限状态机m 是一个八元组m = ( ，0 ，s ，l ，y ，p ，彳) ，其中：s 表示状态的集合，品s 表示初始状态；7 表示转换的集合；y 表示环境变量的集合：p 表示作用于环境变量和输入，输出参数的谓词的集合：肖表示作用于环境变量和输入，输出参数的行为的集合。在状态墨下，对环境变量v 中所有变量的一个赋值，称为状态最的一个环境配置，记为置( 。转换集合t 的每个元素是一个五元组r 薯，s ，j o ，p ，口 ，其中5 。s 称为转换t 的头状态，i 1 和0 0 分别称为转换t 的输入和输出，s 。s称为转换t 的尾状态，p 表示执行转换f 时必须满足的条件，a 表示执行转换f时的动作，只有转换条件p 为真值的情况下，转换t 才可以执行。当使用扩展有限状态机模型描述一个协议规范时，状态是协议实体能够停留的稳定条件；输入是协议实体接收到的外界激励或者内部产生的事件激励( 可能包含一定的输入参数) ；输出是协议实体对外界的响应( 可能包含一定的输出参数) ；转换执行条件是关于输入参数和当前环境变量的条件；转换执行行为包含对输出参数的设置，以及对环境变量的改变。转换f = 表示当协议实体处于状态s 时，接收到外界输入激励或者内部事件f ，如果在当前的环境配置_ ( 矿) 下条件p 能够满足，则执行行为a 来修改环境变量，设置输出参数，对外界产生响应o ( 包含输出参数) 并进入状态_ 。对于转换f = 和状态曩的一个环境配置墨( 矿) ，如果存在输入，满足条件p ，则称转换f 在该环境配置e ( 下可执行。可执行路径：假设m 是一个扩展有限状态机，如果存在转换序列，2 ，使得( 1 ) 假定薯为转换的头状态，则转换在某个环境配置置( 矿) 下可执行：( 2 ) 对于2 七玎，转换的头状耷是转换一。的尾状态，并且转换在执行完转换气一，后的环境配置下是可执行的；则称转换序列f 1 ，t ：，是一条可执行路径。1 2 2 2 2 通信有限状态机( c o m m u n i c a t i n gf i n i t es t a t em a c h i n e ：c f s m )一个通信有限状态机 f 是由状态机集合m 和通信通道集合c 组成n = ( m ，c ) ，其中：m = 嘲， 是有限个数的有限状态机集合；c = 鲰：i , j ，俎f ，) 是有限个数的通道集合；对每一个勺c 代表一个从码到的通信通道，其行为类似于一个先进先出( f i f o ) 的队列，从队列头部取消息作为输入而鸭则将产生的消息放在队列的尾部：如上定义的c f s m 模型能够很好的描述实际协议当中的交互行为，可以将集合m 理解成参与协议交互行为的实体集合，通道集合c 则是实体之间交互的网络连接通道。1 2 2 2 3 事件驱动的扩展有限状态机( e v e n t d d v e ne x t e n d e df i n i t es t a t em a c h i n e ：e e f s m )一个事件驱动的扩展有限状态机m 是一个五元组m = ( s ，s o ，i ，t ) ，其中：s = s o ，品，晶一l 是状态集合，s o s 是初始状态；是事件集合，对任意事件p ) ，e 代表事件名称，歹= ( m ，儿，”) 是事件的参数向量；i 是一系列内部变量组成的向量：7 - 是转换集合，其中的任意元素是一个五元组t - ，其中s 称为转换t 的头状态，s 称为转换t 的尾状态，p ( y ，歹) 是作用在输入参数向量歹和内部变量向量王上的转换条件，而a ( y ，歹) 则是一系列的赋值操作，根据i 和歹的当前值来更新向量j 。该模型将通常的e f s m 模型中的输入、输出事件统一起来用事件来表示，表达更清晰。1 2 2 3 p e t r i 网p e t r i 网( p e t r in e t ：p n ) 是德国学者c a p e t r i 在其博士论文中首次提出的一种特殊的自动机模型，可以用来描述通信系统中异步成分之间的关系。p e t r i网的分析技术主要有两种：可达树分析方法和矩阵方程分析方法。借助p 曲 网的分析技术能得到被模拟系统的有界性、安全性、守恒和可达性等方面的性能评价。目前p e t r i 网有着多种改进形式，如时间p e t r i 网、组合p e k i 网、标号p e t r i网、着色p e t r i 网等等。p e t r i 网因其清晰直观的图形表示、坚实的数学基础和分析技术而在通信协议验证方面得到了广泛得应用，但是它在刻划复杂系统时会显得异常繁琐，也不利于描述协议的进展情况，当进行大型复杂协议的描述时，p e t r i 网模型也同样面临着状态爆炸的难题。基本p e t r i 网可用一个三元组来表示：n = ( p ，t ，f ) ，其中：p ：为有限的位置集合 见，p 2 ，以) ；t ：为有限的转换集合 f ，f 2 ，厶 ；f ：为关系集合，f p r ) u ( r p ) 。若( b f ) f ，则称位置p 为转换r 的输入位置，若( f ，p ) f ，则称位置p 为转换t 的输出位置。1 2 2 4 时序逻辑时序逻辑t l 是模态逻辑的扩充，以状态为可能世界，以状态的演变次序关系为可能世界问的可到达关系。在时序逻辑描述中，使用辅助的时序算子定义时序逻辑公式，每个公式都是关于状态序列的一个断言。一个时序逻辑描述由一组时序公理组成，这些公理描述了对从系统执行开始产生的所有状态序列都为真的性质。时序逻辑通过状态关联进行推理，它附加有与时间相关的操作属性。时序逻辑应用较为成熟，并且数学抽象能力很强，它侧重于通过定义系统外部可见的行为事件来描述系统，即直接描述系统的输入，输出行为，而不关心协议实体的内部变化，。比f s m 、p e t r i 网更易于刻划协议的活动性，因而有利于对协议的各种性质进行分析验证。它的缺点在于协议描述的可读性差，协议描述复杂。p n u e l i 最先将时序逻辑引入计算机科学，用它作为并发程序的推理工具。时序逻辑采用时序操作符来描述系统中事件的发生次序。常用的时序操作符有：o a 表示彳在系统的下个状态为真；a 4 表示从当前状态开始，系统存在一个状态，4 为真；n a 表示从当前状态开始( 包括当前状态) ，a 总是为真；a b 表示从当天状态开始直到丑为真为止( 包括b 为真的那个状态) ，a 总是为真。时序逻辑的种类，随时间结构不同，算子的选择也有差异。目前研究较多的时序逻辑包括：p n u e l i 的线性时序逻辑m p t l 、区间时序逻辑d c ( d u m t i o nc a l c u l u s ) 、分支时序逻辑c t l ( c o m p u m t i o nt r e el o g i c ) 。从逻辑角度来说，时序逻辑t l 是模态逻辑的扩充，以状态为可能世界，以状志的演变次序关系为可能世界间的可到达关系。时序逻转是通过状态关联进行推理的一种技术它附加有与时间相关的操作属性。采用形式化方法定义动态语义和静态语义，其中动态语义用推力规则描述；静态语义由属性语法进行定义。操作的语义基于等价关系的若干类型，用之可证明描述的等价性和正确性。通讯进程演算。如果一个系统的某个性质能用个确定的逻辑表达式描述，井且恒为真( 不随系统的状态变化或执行序列而改变) ，那么这个性质称为系统的不变性质，简称系统不变性。用t l 猫述协议的基本原贝是：用一组公理衰述协议的行为和性质一条公理定义协议状态转换序列中必须满足的不变性或系统所允许状态序列的必须满足的转换条件。t l 公理不定义状志转换中系统所采取的具体方法和过程。协议的t l 描述是一种抽象的描述，“抽象”体现在协议机制、协议行动、协议事件、协议的状态塔被隐含在描述中。t l 的数学抽象能力很强，它侧重于通过定义系统外部可见的行为事件来描述系统，即直接描述系统的翰入，输出行为，而不关心协议实体的内郁变化，比f s m 、p e t t i 网更易于刻划协议的活动性，因而有利子对唯匕议的各种性质进行分析验证。但由于不同学者采用的t l 有差别：采用的方法有差别抽象的程度有差别。即便是对简单的a b 协议，t l 的描述结果也千差万别。有的描述极为抽象，很难理解。这就使得t l 在协议模型技术中的应用推广带来限制，尤其不使用于描述复杂协议困此，提高协议t l 描述的“通俗化”和“直观化以及。标准化是至关重要的问题。1 _ 2 2 5 通讯进程演算进程代数是一门8 0 年代才发展起来的数学，r m i l e r 在这方面作了开拓性工作他的通讯进程演算c c s 已在协议工程等领域内得到重要的应用，是所有进程代数的基础。以c c s 为基础，其它学者也提出了一些进程代数，其中比较成熟的是通讯顺序进程c s p ( t h ec o m m u n i c a t i n gs e q u e n t i a lp r o c e s s ) 。c c s 用三个基本算子定义一个进程，这三个算子是：1 、顺序算子：用于描述进程顺序执行事件的行为一个进程既便是同时执行多个事件观察者也可以将它们按顺序描述。顺序算子用句点“表不。2 、选择算子：用于描述进程从多个事件中选择执行一个的行为，用符号“+ ”表示。3 、并行算子：并行算子也叫做组合或并发算子，用于将多个进程组成一个进程，用符号“ 。表示。并行算子不能用于事件。以上三个基本算子过于简练，它不能表达实际进程的复杂行为引入附加算子或三个基本算子的变种算子可大大提高c c s 的表达能力c s p 定义的算子比c c s 多且大多都是c c s 基本算子的变种算子。一般地说，算子越多，表达能力就越强，代数变换规则就丰富。表达式的等价变换规则是代数系统的核心。在c c s 中表达式的变换规则基于4 观察等价”：对外部观察者来说，如果进程执行两个表达式所表现的行为是不能区分的，那么这两个表达式是等价的。由于c c s 的代数变换规则是基于较强的”观察等价“原则，可以得出结论：用c c s 证明是正确的协议一定是正确的协议，反之不一定。从c c s 的表达是可判定协议是否有活动性、安全性、一致性和完各性，因此可用于验证协议，判定协议的正确性。t 进程执行事件的记录叫做迹i 它可用图表示。c c s 的迹和f s m 图或p e t r i 网有很好的映射关系，可以从f s m 图和p e t r i网中得出c c s 描述。1 - 2 1 3 测试序列生成协议一致性测试时，测试系统向i u t 施加输入事件序列，接收校验输出事件序列，检查状态转换，根据输出事件和状态的转移，判定i u t 的行为是否符合协议规范的描述，这种测试方法称为主动测试方法，其中的输入、输出事件序列叫做测试序列。测试序列说明i u t 所应该表现的逻辑行为，因此它可以从协议模型中推导出来。目前，大部分协议测试序列的生成算法是基于f s m 模型的。测试序列是一组根据协议规范产生的输入、输出事件序列，它是协议一致性测试的核心数据协议一致性测试时，测试执行系统向i u t 施加输入事件序列，接收校验输出事件序列，检查状态转换，根据输出事件和状态转换，判定i l 厂r的行为是否符合协议规范的描述。本节主要介绍四种基于f s m 模型的基本的测试序列生成方法并对它们的特点进行了分析比较。测试序列说明i u t 所应该表现的逻辑行为，因此它可以从协议模型中推导出来( f s m 模型，e f s m 模型，p e t r i 网模型，c c s 模型等) 目前，理论上比较成熟的测试序列生成算法都是基于f s m 模型而基于e f s m 等其它模型的测试序列生成方法仍处于研究探索阶段。对于e f s m 模型的测试序列生成，有学者结合控制流和数据流特性两方面同时考虑其测试序列生成，但通常的做法还是从其控制流特性出发，直接借用基于f s m 模型的测试序列生成算法。基于f s m 模型的测试序列生成算法均要求i u t ( 即它的f s m 摸型) 具有以下四个特性：1 、i u t 的状态数、所能接收的输入事件数、所产生的输出事件数都是有限的、确定的。这个特性保证算法是收敛的。2 、i u t 的f s m 是确定的状态机。即它在每个状态下都能接收所有协议规范描述的输入事件。输入事件可以分为两种：核心事件和非核心事件i u t 在某个状态下对一部分输入事件产生响应( 或产生输出事件，或改变状态，或产生输出事件的同时改变状态) ，这些输入事件称作核心事件，其它输入事件称作非核心事件，如报文丢弃处理等非核心事件是不合法事件的一部分。f s m 图只画出核心事件所引发的转换，因此，测试序列生成算法也只关心核心事件，而非核心事件的副试则留待测试例生成时扩充。3 、对于每个输入事件，如果i u t 产生输出事件，那么该输出事件在给定有限时间内产生。根据这个特性，i u t 的超时事件是可以判定的，它是否产生输出事件也是可判定的。4 、i u t 的每个状态是可达的，即它的f s m 图是联通的。这是所有测试序列生成算法能够执行的基本前提。最佳的测试序列应该满足以下条