（计算机软件与理论专业论文）基于模型检查的协议一致性测试生成.pdf

基子模型检查的协议一致性测试生成摘要 摘要 如何从协议规范出发生成满足一定覆盖标准的测试序列和测试套是协议一 致性测试中的一个核心问题，现有的协议一致性测试序列和测试套生成方法大部 分都是基于协议的f s m ( f i n i t es t a t e m a c h i n e ，有限状态机) 模型。与f s m 相比， e 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 的一致性测试生成的研究正在起步。 模型检查技术通常用于硬件电路以及协议规范的形式化验证中，本文将模型 检查技术引入到以e f s m 为模型的协议一致性测试序列和测试套的自动生成中， 认为生成满足一定测试覆盖标准的测试套问题可以转化为模型检查中的反例构 造问题，进而提出了一种新的测试生成方法。该方法用k r i p k e 结构描述协议的 e f s m 模型，用一系列c t l ( c o m p u t a t i o n a lt r e el o g i c ，计算树逻辑) 公式刻画测 试套所要满足的控制流和数据流覆盖标准，然后利用模型检查工具所具有的反例 构造功能为每个c t l 公式构造一个反例，每个反例对应于一条满足定覆盖要 求的测试序列，所有c t l 公式的反例集合就对应于满足一定覆盖标准的测试套， 该方法的显著优点在于：自动生成的测试序列和测试套是完全可执行的。 本文讨论了输入和输出交互不含参数且变量取值范围有限的e f s m ，其等价 k r i p k e 结构的构造方法、迁移覆盖标准咀及变量a l l u s e 覆盖标准的c t l 公式描 述方法。在此基础上研究了输入和输出交互含参数且变量取值范围有限的e f s m 的测试生成，并进一步给出了输入输出参数a l l 1 0 一d f - c h a i n 覆盖标准的c t l 公式 描述方法。利用该方法，使用模型检查工具s m v ，为l m - e s 协议分别生成了满足 迁移覆盖标准、变量a 1 1 u s e 覆盖标准、以及输入输出参数a 1 1 1 0 一d r - c h a i n 覆盖标 准的一致性测试套。 爻验结果表明该力_ 1 i 但同时适用f 食描述( c o m p l e t e l ys p e c i f i e d ) e f s m 和非完全描述( n o n c o m p l e t e l ys p e c i f i e d ) e f s m ，而且对。1 卜定数据流测试覆箍 标准所对应的每个可能待覆盖实体( 即变璜的定义使用对d u p a i r 或者输入输出 参数的简单数据流链s i m p l e i o d f - c h a i n ) ，该方法或者自动判定出不存在覆盖该 中国科学技术大掌t j 、；学位论文 甚十摸型榆古的协议一毁性测试生成摘要 实体的测试序列，或者自动给出一条覆盖浚实体的测试序列，从而实现了协议完 全可执行一致性测试套的自动化生成。此外该方法将测试序列生成的细节完全隐 藏于模型检查工具中，因此陔方法具有高度的自动化程度。 本文的工作扩展了模型检查技术的应用范围，使其从对有限状态系统进行分 析验证扩展到协议一致性测试套的自动生成。 关键词：一致性测试：测试覆盖标准：模型检查：计算树逻辑：k r i p k e 结构 中困科学技一。 顺十学位论文 i i 薹王壁型丝奎塑堕坚二鍪堡塑堕竺堕 塑至 a b s t r a c t h o wt og e n e r a t et e s ts e q u e n c ea n dt e s ts u i t es a t i s f y i n gs o m et e s t c o v e r a g e c r i t e r i ai sak e yp r o b l e mi nt h ef i e l do fp r o t o c o lc o n f o r m a n c et e s t i n gm o s to ft h e p r e s e n tt e s tg e n e r a t i o nm e t h o d sa r eb a s e do np r o t o c o l s f i n i t es t a t em a c h i n e ( f s m ) m o d e l sc o m p a r e dt of 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 ) m o d e lc a nm o d e la p r o t o c o li nam o r ea c c u r a t ea n ds u c c i n c tw a yb e c a u s eo ft h ei n t r o d u c t i o no fv a r i a b l e s ， c o r r e s p o n d i n go p e r a t i o n so nt h e ma n dp r e d i c a t e so nt r a n s i t i o n so nt h eo t h e rh a n d ， t h e s ea d d e df a c i l i t i e sm a k et h et e s tg e n e r a t i o nf r o ma p r o t o c o l se f s mm o d e lm o r e d i f f i c u l tt h a nt h a to ff s mn o w a d a y st e s t i n go fe f s mi ss t i l la ta ne a r l ys t a g e m o d e lc h e c k i n gh a sb e e nu s e dp r i m a r i l yi nh a r d w a r ea n dp r o t o c o lv e r i f i c a t i o n i nt h i st h e s i s ，m o d e lc h e c k i n gi sa p p l i e dt og e n e r a t ep r o t o c o l sc o n f o r m a n c et e s ts u i t e a u t o m a t i c a l l y i ti sp r o v e dt h a tt h ep r o b l e mo ft e s tg e n e r a t i o nf r o me f s mc a nb e t r a n s f o r m e di n t ot h ep r o b l e mo ff i n d i n gw i t n e s s e si nm o d e lc h e c k i n gan e wm e t h o d i sp r o p o s e dt og e n e r a t et o t a l l ye x e c u t a b l ec o n f o r m a n c et e s ts u i t ef r o me f s mu s i n g m o d e lc h e c k i n gt e c h n i q u ei nt h i st h e s i si nt h i sm e t h o d ，p r o t o c o l se f s mm o d e li s d e s c r i b e di nk r i p k es t r u c t u r ea n ds e l e c t e dc o n t r o lf l o wa n dd a t af l o wt e s tc o v e r a g e c r i t e r i aa r ec h a r a c t e r i z e dw i t has e to f c t lf o r m u l a e w i t ht h ea i do f m o d e ic h e c k e r s c o u n t e r e x a m p l eg e n e r a t i o na b i l i t y , at e s ts e q u e n c es a r i s l y i n gs o m ec o v e r a g e r e q u i r e m e n tc a nb eo b t a i n e df o re a c hc t lf o r m u l aa l lc o u n t e r e x a m p l e sw i t hr e s p e c t t ot h es e to fc t lf o r m u l a em a k eu pat e s ts u i t es a r i s f y i n gs o m et e s tc o v e r a g e c r i t e r i o n f i r s t l y , t h et e s tg e n e r a t i o nf r o me f s mw h o s ei n p u ta n do u ti n t e r a c t i o n sd on o t c o n t a i np a r a m e t e r sa n dv a r i a b l e sh a v ef i n i t es c o p ew a sd i s c u s s e di nt h i st h e s i s w e s h o w e dh o wt oc o n s t r u c tt h ee q u i v a l e n tk r i p k es t r u c t u r ef o rs u c hk i n do fe f s ma n d h o wt od e s c iz 、t r a n s i t i o ng o v e r n 5 ：d t e r i o na n dv a r i a a 1 1 u s ec o v era g elr i o ni n c t lf o r m u l a ei j u r t h e r m o r e ，w ed i , c u s s e dt h et e s tg e t lc ：r a t i o nf r o me f s mw h o s e i n p u ta n do u ti n t e r a c t i o n sc o n t a i nf i n i t ep a r a m e t e r sa n dv a r i a b l e sh a v ef i n i t es c o p e s a d d i t i o n a l l y ，t h et e c h n i q u eo fc h a r a c t e r i z i n gp a r a m e t e r s a l l i o - d f - c h a i nc r i t e r i o ni n 率国肄、声技术大学碾学位论义 i i l 雄十模型枪盘的如议一致性测试生j 戊摘要 c t lf o r m u l a ew a sp r e s e n t e d f i n a l l y ，i nt h ec a s eo fi n r e sp r o t o c o l ，t h ec o n f o r m a n c et e s ts u i t e ss a t i s f y i n g a l l t r a n s i t i o nc o v e r a g ec r i t e r i o n ，v a r i a b l e s a l l u s ec o v e r a g ec r i t e r i o na n dp a r a m e t e r s a l l 1 0 d r - c h a i nc r i t e r i o nc o v e r a g ec r i t e r i o nr e s p e c t i v e l ya r ec o n s t r u c t e du s i n gt h i st e s t g e n e r a t i o nm e t h o d ，t h er e s u l t ss h o wt h ef e a s i b i l i t ya n de f f i c i e n c yo f t h i sm e t h o d o u r w o r ke x t e n d st h er a n g eo fa p p l i c a t i o n so fm o d e lc h e c k i n gf r o mf o r m a lv e r i f i c a t i o no f f i n i t es t a t es y s t e m st ot e s tg e n e r a t i o nf r o me f s mm o d e l k e yw o r d s ：c o n f o r m a n c et e s t ；t e s tc o v e r a g ec r i t e r i a ；m o d e lc h e c k i n g ； c o m p u t a t i o n a lt r e el o g i c ；k r i p k es t r u c t u r e 中川是术人学倾i 学位论 i v 基于模型检查的协议一致性测试生成第一章引言 第1 章引言 在过去二十年中，畎信息交换为基础的计算机网络和分布式系统取得了飞跃 性发展，在成功实现不同计算祝系统之间的信息交换中通信协议扮演了极其重 要的角色。与此同时，随着计算机网络和分布式系统的日趋复杂，通信协议的种 类和数量越来越多，其规模也越来越大。如何设计出功能上正确可靠，逻辑上一 致完整的通信协议，并且系统地进行协议规范、协议验证、协议实现和协议测试， 已经成为了一个非常具有挑战性的课题。为了解决以上的问题，很多学者将形式 化方法引入到协议的研究中，从而形成了一个新的研究领域，称作协议工程 ( p r o t o c o l e n g i n e e r i n g ) l a i 0 2 。 作为协议工程学的一个重要分支，协议一致性测试( c o n f o r m a n c et e s t i n g ) 检 查协议的具体实现( i m p l e m e n t a t i o n ) 与协议规范( s p e c i f i c a t i o n ) 符合程度，其目的 是提高分布式系统组件之间能够成功进行通信的概率 d s s o u l i 9 9 。在协议一致性 测试中，如何从协议模型和规范出发生成高质量的一致性测试套是一个核心问 题，而寻找通用、高效的一致性测试套生成方法一直是研究者们不懈追求的目标。 本文尝试将模型检查( m o d e l c h e c l a n g ) 技术用于协议一致性测试套的自动生成， 力求对该问题进行些有益的探索。 本章首先介绍协议一致性测试引入的必要性，然后对协议一致性测试进行概 述，最后对文章的内容结构进行了介绍。 1 1 协议一致性测试的引入 现代计算机网络及分布式系统涉及到系统内不同组件间复杂的交互 ( i n t e r a c t i o n ) 操作，通信协议正是网络及分布式系统中不同实体进行信息交互时 应遵守的规则集合 t a n e n b a u m 0 3 i 。系统中不同的网络实体只有遵守特定的协议 卅现正确可意的u 、为使来自水2 厂家的系统能魄：叻进行通信，必 须千j 卧准化的通信j 办议，这种需求直接导致，1 目际标准化组织d 臼提出了开放系 统j 二联参考模型以及各层的协议标准 d a y 8 3 。 随着网络及分布式系统的快速发展以及遇信技术复杂程度的目益增加，通信 中国科学技术太学ol 学位论文 基于模型检查的协议一致性测试生成第一章引言 协议的标准化清楚地显示出了其在计算机通信系统开发中的重要性，然而仅仅依 靠协议的标准化并不能保征来自不同厂商的异构系统组件之间能够成功进行通 信。这是因为协议标准制定后通常还只是一个自然语言描述的文本，仅靠文本不 但难以保汪对协议规范的详尽完备描述，而且文本描述还可能具有二义性。此外， 协议标准的产品化开发通常由不同的组织以及不同的人员进行，由于不同的开发 人员对协议标准的理解可能不同，采取的实现手段也可能不同，开发过程中又可 能存在这样或那样的错误，所以很容易导致协议具体实现( i m p l e m e n t a t i o n ) 中的 某些功能偏离标准甚至引入缺陷，或者仅实现了标准的某个子集。这些与标准不 一致或相互间不兼容的产品在联网时难以可靠地通信。因此，人们需要一种有效 的方法对各种协议实现进行测试，判断被测实现是否与协议规范相一致，这种方 法便是协议一致性测试。 1 2 协议一致性测试 众所周知，测试就是通过实验的方法来试图发现一个系统中存在的错误或对 系统某一方面的属性进行评估的过程，其目的是为了确信在系统的正常使用中， 系统会按照预期的方式工作，能够实现预期的功能。这种实验通常在一个特定环 境中通过对系统进行正常或异常的使用来实现，并且因为测试活动在时间和空间 上的有限性，对于一个真实系统的测试不可能无遗漏地历经系统的每一种运行情 况。所以测试并不能保证被测系统的完全正确性，即测试只能显示“存在错误”， 而不能证明“不存在错误”。 在软件测试中，通常有结构测试( s t r u c t u r a lt e s t i n g ) 和功能测试( f u n c t i o n a l t e s t i n g ) 之分。结构测试又称为“白盒测试”，它是基于软件内部结构进行的测试， 其目的是通过执行每条语句，遍历程序的每个分支来检查整个程序代码的正确 性。与此相反，功能测试只是依据软件的规格说明对从外部可以观测到的软件功 能进行测试，所以也称之为“黑盒测试”，即将被测试系统看作一个黑盒，仅仅 j ，过观察其外部 啦确定软件的功n 、j 观，而不涉及釉，j 内部结构其 】 足根据软件的规格说明确定软件实现是否达到了预期要求，1 划此预先要有个f _ _ ；j 洁明确的软件功能说明。 在现代通信系统中，为了减小设计和实现上的复杂性，大多数网络通常被组 中国科学技小 、学硕士学位论文 织为层状结构，每一层的目的都是为其上层提供特定服务，并且向上层屏蔽其所 提供服务的实现细节 t a n e n b a u m 0 3 。一台机器上的第一层实体( 进程) 同另外一 台机器上的同层对等实体之间通过遵守第n 层协议来进行消息或数据包的交换。 图1 - 1 给出了一个典型通信协议系统的模型，其中s 层实体通过7 层实体所提供 的服务原语s p ( s e r v i c ep r i m i t i v e ) 在服务接入点s a p ( s e r v i c e a c c e s s p o i n t ) 与7 层 实体进行交互。而r 层实体又通过其下面的层实体所提供的服务原语与j v 层 实体进行交互，从而完成与另外一台机器7 层实体之间协议数据单元 p d u ( p r o t o c o l d a t au n i t ) 的交换。每层实体行为的定义通常称作协议规范( p r o t o c o l s p e c i f i c a t i o n ) 。 一爪s p 、s a p ? 一廿s p ：t r a n s p o r tl a y e r ， 一， n e t w o n kl a y e r 图1 1 通信协议系统模型 协议一致性测试就是测试协议实体对于协议规范声明的一致性要求的遵循 程度的过程 c a v a l l i 9 6 。在一致性测试中，被测对象i u t ( i m p l e m e n t a t i o nu n d e r t e s t ) 是协议实体的一个具体实现。一致性测试属于黑盒测试的范畴，对于儿，7 1 的测试是完全相对于其参考规范进行的，测试者只能根据，u r 对输入的响应来 分析判断，u r 相对于参考规范的一致性程度，测试中并不关注儿盯的内部实现 细节。 图卜2 简”，：、：，明了协议致。试的原理：通常( 禽有一个上接口l , o d r i n t e 椭c e ) 利下按1 ( l o w e rl u t e 哟。j ，一致性测试。破称作控制观磐- ! i p c o ( p o i n t so f c o n t r o l a n d o b s e r v a t i o n ) 的标准接口处完成。因为通信经常意味着 异步性，所以p c o 可以模拟为两个f i f o 队列。对于旧，【仃进行消息交互的测 中国科学蕾、大学硕士学位论文 基于模型检查的挤议一致性棚试生成第一章引言 试器( t e s t e r ) 来说，通常有i - _ n 试器u t ( u p p e rt e s t e r ) 和下测试器l t ( l o w e rt e s t e r ) 之分。叩和l t 分别控制着儿叮的上下接口。在测试中，( ，r 扮演着，明所提供 服务的使用者角色，7 通常扮演着i u t 对等实体的角色，也就是说，i u t 与7 进行通信来为u 7 提供服务。i u t 和u 7 通过抽象服务原语a s p ( 4 b s t r a c ts e r v i c e n 砌m v p ) 进行交互，而，u 7 和7 _ 通过交换协议数据单元p d u 来提供它们的服 务。 t h ep c oh a st w of i f oq u e u e s ： 。 s e n d ( f r o mt e s t e rt oi u n r e c e i v e ( b yt e s t e rf r o mi u t ) 图1 - 2 一致性测试的原理 1 。3 一致性测试主要研究内容 目前，关于协议一致性测试的研究主要集中在两个方面：( 1 ) 一致性测试方 法和一致性测试结构的研究；( 2 ) 一致性测试序列和测试套生成方法的研究。 1 3 1 一致性测试方法 1 s 0 定义了四种抽象测试方法 c c i t t 9 1 ，一种是局部的，三种是外部的， 分别为分布式、协调式和远程式。在局部测试法中，上下测试嚣与i u t 在同一 系统中，而l i 溜测试方法中，测试器远离i u i 。通过网络相联。) 。一j 方法 可以测试多层系统中的某一层，也呵以测试多层系统一l ，的几层。 下面列这些方法进行简单介绍和比较。 ( 1 ) 局部测试法 中幽t 一。产技术大学颈学位论支 6 萋于模型检查的济议一致性测试生成第一章；1 言 局部测试法的结构如图1 3 所示。在这种方法中，u 兀兀，u r 同处于一台 机器中，测试不需要低层通讯的支持，i u t 和r 的接口设在亿t 的底部，c ，7 和儿叮的接口设在1 u t 的顶部( 即为几研的服务访问点) 。由于u 7 和7 可以 拟和在一个程序中，u 7 1 和7 之间的测试协同过程兀甲( 殆甜c o o r d i n a t e p r o c e d u r e s ) 容易实现。 图1 - 3 局部测试法 ( 2 ) 分布式测试法 分布式测试法如图l - 4 所示。在这种方法中，c 仃和，r 处于同一个机器中， ，分布在其它机器中。l t 和儿盯借助于( 一1 ) 层服务交换消息( 可以实现在线 测试) ，它们之间的接口j p c p 从儿叮转移到r 中，三r 扮演的角色是( j v 一1 ) 层 服务的使用者。u r 和三，的测试协同过程咒i p 隐含在测试例中，测试周步问题 由u r 和丁的操作者来实现。 中国科学技本，、学硬士学位论文 图1 - 4 分布式测试法 7 基于模型检查的协议一致性铡试生成第一章亏l 言 ( 3 ) 协同式测试法 协同式测试法实际上是分布式测试法的一种变形如图i 5 所示。协同式方 法和分布式方法的根本区别在于：协同式方法引入测试管理协议t m p ( t e s t m a n a g e m e n tp r o t o c 0 1 ) ， ，r 和r 通过交换7 m 一肋u 实现测试协同过程。刀订一 p d u 的交换有两个途径，一是7 m 叫，d u 作为( d a s p 的用户数据传送给，u r ， ，u 7 将之传送给l t ( i n - - b a n d 方式) ：二是7 m 叫u 直接利用( 卜1 ) 层服务传 送( o u t - - b a n d 方式) 。 图1 - 5 协同式测试法 ( 4 ) 远程测试法 远程测试法的结构如图1 - 6 所示，该方法的最大特点是没有u l 因此也不 存在，和三丁的协同闯题。测试例完全用一1 ) 一s p 描述。远程方法适用于被 动式协议实体或服务型协议实体的测试。 s u t t e s ts y s t e m 哦1l o w e r 穗s t e r ： ：。i = = = = 个t p c 。眺 山 1 ) c r 2 ) c c 7 ，：；q 列学技术大学硕士学姆母文 图1 - 6 远程测试法 基于模型检查的协议一致性测试生成第一章引言 1 3 _ 2 一致性测试序列和测试套生成 对协议进行一致性测试，选择适当的测试方法建立测试系统是实现协议一致 性测试的基础，而测试套( t e s t s u i t e ) 是一致性测试的核心和主线，两者是互相配 合，互相制约的。一个有好的测试方法的测试系统，可以极大地简化测试序列和 测试套的设计，使测试能方便、自动、高效地进行：而一个好的测试套也可以极 大地减轻测试系统的负担。 测试套由一系列测试序列所构成，而测试序列是一个输入预期输出序列。 i s o 将测试套规范化为层状结构 c c i t t 9 1 ，自上而下分为测试组( t e s t g r o u p s ) 、 测试例( t e s tc a s e s ) 、测试步( t e s ts t e p s ) 和测试事件( t e s te v e n t s ) 。测试组规定该 组中测试例的逻辑顺序，测试例是测试组中最重要的部分，每个测试例由测试步 组成，测试步规范化为一系列测试事件，这些测试事件包括，( 仃发送或接收的 一个p d u 或a s p 等。 i s o 将测试例分为通用测试例、抽象测试例和可执行测试例 c c i t t 9 1 。通 用测试例由测试体和该测试体的初始状态组成。测试体是为完成一定测试目的并 对可能的测试结果进行判定所必需的测试事件序列。测试结果判定有三种结论： 通过( p a s s ) 、失败( 而西和无结论( i n c o n c l u s i v e ) 。一旦获得通用测试套，就可根 据不同的测试方法生成相应的由抽象测试实例组成的抽象测试套。 抽象测试例是把通用测试例加上测试前缀( t e s tp r e a m b l e ) 和测试后缀( v e s t p o s t a m b l e ) ，并按照控制观察的要求表达出来得到的。测试前缀是当儿口不在该 测试例之测试体要求的初始状态时，使儿叮到达测试体要求的初始状态的一个 测试事件序列。而测试后缀是测试体测试结束后，使儿玎回到需要的稳定状态， 以便后面测试运行的一个测试事件序列。 可执行测试例是由抽象测试例，根据实际测试系统、协议实现一致性声明 ( h c s ) 、1 u t 及其环境的附加信鼠( p i x i t ) 进行推导并参数化得来的，成为测试的 一个具体1 j 嘎，运行在实际测i 。r 系统上。三类测试- 铡的演变过程如图一7 所示。 中汹，；学技术大学硕士学位论，i 9 基于模型检查的济泌一致性涮试生成第一章引言 通用测试例 抽象测试方法 抽象测试例 p l c s 选中的测试例 p l x i t 参数化的测试例 1 4 文章的组织 可执行测试例 p l c s 选中的可执行测试例 p i x i t 参数化的可执行测试例 图1 7 测试实例演变过程 本文的章节组织是：第2 章介绍传统的协议一致性测试序列和测试套生成方 法，首先介绍基于f s m 模型的基本测试序列生成方法，并对它们的特点进行比 较分析，然后介绍现有的基于e f s m 模型的测试生成方法。在第3 章中，首先介 绍计算树逻辑c 仡和模型检查的有关概念，然后介绍符号模型技术以及符号模 型检查工具s m v o 第4 章具体讨论怎样将模型检查技术应用于基于e f s m 模型 的协议一致性测试序列和测试套的生成中。在第4 章中，首先讨论输入输出交互 不含参数且变量取值范围有限的e f s m 的测试生成，然后讨论输入输出交互含有 参数且变量取值范围有限的e f s m 的测试生成。第5 章讨论如何利用本文提出的 测试生成方法为i n r e s 协议构造一致性测试套，并给出利用该方法得到的分别满 足3 种覆盖标准的l r t r e s 协议测试套。第6 章对文章进行总结并对未来工作进行 展望。 蝇科学技术大学硕士学”葩义 基于模型检查的协议一致性设j 试生成第二章现有的一致性溯试序列和测试套生成方法 第2 章现有的一致性测试序列和测试套生成方法 测试序列是根据协议规范产生的输入输出事件序列，将一系列测试序列按 照某种方式组织起来就构成了测试套。测试序列和测试套是协议一致性测试的核 心数据。在进行协议一致性测试时，测试执行系统向儿7 施加输入事件序列， 接收校验输出事件序列，检查状态迁移，根据输出事件和状态迁移，判定i u t 的行为是否符合协议规范的描述。本章首先对测试序列生成方法进行概述，然后 介绍四种基于f s m 模型的基本测试序列生成方法，并对它们的特点进行分析比 较，然后介绍现有的基于e f s m 模型的测试序列生成方法，并对它们的特点进行 分析。 2 1 测试序列和测试套生成方法概述 测试序列说明了儿仃所应该表现的逻辑行为，因此它可以从协议模型( 尺m 模型、e f s m 模型、n 们网模型、c c s 模型等) 中推导出来。目前，理论上比较 成熟的测试序列生成方法都是基于f s m 模型的，而基于e f s m 等其它模型的测 试序列生成方法仍处于研究探索阶段 l e e 9 6 a 1 。 基于f s m 模型的测试序列生成方法均要求，【盯( 即它的f s m 模型) 具有以下 四个特性 h o l z m a n n 9 1 1 ： ( 1 ) 儿口的状态数、所能接收的输入事件数、所产生的输出事件数都是有限 的、确定的。这个特性保证算法是收敛的。 ( 2 ) 儿仃有完整性，即它在每个状态下都能接收所有狭义规范描述的输入事 件。输入事件可以分为两种：核心事件和非核心事件。几t 在某个状态下对一部 分输入事件产生响应( 或产生输出事件， 变状态) ，这些输入事件称作核心事件， 州生肖研去只关心核心q t 。 或改变状态。或产生输出事件的同时改 其它输入事件称作非核心事件。测试序 ( 3 j 时于每个输入事仃如果儿盯产生输f ti ! 每f t - ，那么该输出刊斗在给定有 限时间内产生。根据这个特性，己，7 的超肘事件是可以判定的，它是否产生输出 事件也是可判定的。 ( 4 ) 儿，7 1 的每个状态是可达的，即它的f s m 是连通的。这是所有测试序列生 一 ，因科学技术大学磺上? ：位论文 l l 基于模型检查的协议一致性测试生成 第二章现有的一致性测试序列和测试套生成方法 成方法的基本前提。 基于f s m 模型的状态迁移的测试可以分三步进行： s t e p l ：用一个测试前缀序列把f s m 置于某个状态： s t e p 2 ：施加某个输入，并观察它的输出，此举用于检查是否有输出错误； s t e p 3 ：检查f s m 的新状态并确定状态满足规范要求。用于检查是否有迁移 错误。 2 2 基于f s m 的测试序列生成方法 基于f s m 的测试序列生成方法主要有以下四种 s i d h u 8 9 】，即周游法 ( t r a n s i t i o nt o u rm e t h o d ) ，也称7 1 方法 n a i t 0 8 1 ；区分序列法( d i s t i n g u i s h i n g s e q u e n c e s m e t h o d ) ，也称d 方法 g o n e n c 7 0 ；特征序列法( c h a r a c t e r i n g s e q u e n c e s m e t h o d ) ，也称w 方法 c h o w 7 8 ；唯一输k 输出序列法( u n i q u el n p u t o u q ，u t s e q u e n c e s m e t h o d ) s a b n a n i 8 5 ，连l 称( 圩p 方法。下面对这四种方法分别进行简单 介绍。 2 - 2 1f s m 模型 定义2 1 有限状态机f s m ( 厅”i t es t a t em a c h i n e ) ：一个完全描述的有限状态 机是一个5 元组 s ，测试序列由四部分组成：( a ) 引 导序列i ( b ) 待测迁移i o ( 带下划线标记) ；( c ) 状态0 的u i o 序列：( d ) 同步序 列r i m d l 。 ( a x ，e l y ，a y x ，r i n u l l ) ：测l 式状态迁移卜a i x l ( 垒，6 丘，r i n u l l ) ：测试j 吠态迁移l c y 呻4 c 仉矾，b y ，鲍，吵，出，r i m d l ；测试状态迁移2 一a y l 中丛 # 技术大学磺士学位论- 1 6 基于模型检查的协议一致性测试生成第二聋现有的一致性测试序歹4 和测试套生成方i 去 ( 眇，酞，坳，丛，砂，以。r i n u l l ：，测试状态迁移2 一b x - - 3 f 吵，b x ，垡尘，b y ，r i n u l l ) 俐啊试状态迁移3 一b x 寸5 砂，丝，蛳，北，n n u l l ：，例试状态迁移4 一b r 斗3 ( 掣，鲣，盼，r i n u l l ) ；n 试状态迁移4 一b x _ 5 ( 钞，n 詹，鱼坐，b x ，r i m d l ：测试状态迁移5 一b y - - 2 f 吵，们，致，吵，r i n u l l ) ；测试状态迁移5 - c y 寸5 砂，a x ，a , z ，c ，嘶，r i l n u h ：测试状态迁移5 b l y _ i 利用【，方法产生的测试序列的长度明显要比d 方法产生的短。但并非每个 f s m 都存在u i o 序列，图2 5 所示的f s m 就不存在u i o 序列。 一个f s m ，如果没有u i o 序列，则也没有d 序列，解决的办法是采用下面 介绍的形方法。 2 2 5 形方法 图2 5 不存在u i o 序列的f s m 肜方法包含了两个输入序列集合w s e l 和p s e t 。w s e t 是f s m 最4 、的特征 集，它使得每对状态能够桐可区分。即对不同| 勺4 态应用玎2 s c ，观察到的输出应 该是能够卜分的。ps e t 包含j 昕有部分路径，目 谍测试树组成，。的根结点 是初始状态，每个迁移只出现一次。 对于图2 - 5 所示的f s m ，叮以按如下步骤求甜w s e l ： s t e p l ：输入a ，将状态集合争( 1 ，2 ，3 ，4 ) 划分为两个子集： 一：、 科学技术大学颈士学峙。：文 基于模型检查的协议一致性测试生成第二章现有的一致性测试序列和测试套生成方法 ( 1 ) 输出r & = ( 2 ，3 ) ；( 2 ) 输出y = l ，4 ) ： & 印2 ：输入b ，把s l 再划分为两个子集： ( 1 ) 输出rs 1 2 = 2 ) ：( 2 ) 输出ys 1 2 = 3 ) ； s t e p 3 ：输入b ，将再划分为两个子集： ( 1 ) 输出r 岛l = 1 ) ；( 2 ) 输出y 2 = 4 ) ； 从而可以得到w _ s e 卢 a b 。每个状态对特征序列的输出响应如下： 状态l ：w y ，b x ；状态2 ：幽，b a r ；3 ：矾，劬；状态4 ：砂，妙。p s e t 为： f s ，口，b ，a b ，册，b b ，b a ，b a b ，6 船 ，其中s 表示空序列。因此对于图5 所 示的硒w 而言，用w 方法产生的测试序列为： p s e t w s e t2 ( a ，b ，砌，曲，b a ，b b ，a b a ，a b b ，绷，a a b ，b b a ，b b b ，b a a ， b n b b a b a ，b a b b ，b a a b 。 2 2 6 测试序列的优化 测试序列的长度直接影响着测试效率，因而寻找最短测试序列一直是研究测 试序列生成方法的学者们的目标。这方面已有的研究工作主要是围绕着前面提到 的四种测试序列生成方法，提出各种改进技术。以u i o 方法为例： 1 9 8 8 年，a h o ，d a h b u m 等提出结合中国乡村邮路算法寻找以u i o 序列为特 征序列的最短测试序列 a h 0 8 8 1 。这种方法的基本思想是：把所有特征序列中的 头尾两个端点连在一起构成有向图g ：这个图与原来的有向图g 一起构成一个 新图。用中国乡村邮路算法，求出新图的欧拉回路，就可得到一个优化的u i o 序列。 1 9 9 0 年，s h e n 、l o m b a r d i 和d a h b u r a 等提出了多u i o 序列的方法 s h e n 9 0 1 。 这一方法是前一方法的延伸。它的优化思想是：每个状态可能有多个u i o 序列。 当一个状态的某个川d 序列与另一个状态的明0 序列相临时，可以减少整个路 径的开销。因而它考虑从每个点的多个u i o 序列中选取出“对接效果”最好的 序列不 此外还有很多对测试序列进行优化的方法，例如y u 和l i u 提出的利用多个 u i oj ：f 列和部分叠加相结合的方法来缩短测试序列；h i e r o n s 等提出的利用逆向 判定迁移来缩短测试序列长度的方法等等，在此不再累述。 围科学技术大学硕士。f 。= 沦文 基于模型检查的协议一致性测试生成第二蕈现有的一致性测试序列和测试套生成方法 2 3 基于e f s m 的测试序列生成方法 一般而言，一个协议规范通常可以划分为协议的控制部分和数据部分 【b o u r h f i 0 6 ，其中协议控制部分可以很方便地用f s m 来描述，因此前面介绍的基 于f s m 的测试生成方法生成的测试序列可以很好地被用来测试协议控制部分。 对于协议规范的数据部分来说，其通常包括变量以及基于这些变量值的操作，对 于这些元素，f s m 的描述能力就显得不足了 l e e 9 6 b ，具体地讲，( 1 ) f s m 不能 方便地模拟对变量进行的操作；( 2 ) f s m 不能方便地模拟变量值的转换。因此对 于包含数据部分的实际协议规范来说，f s m 并不能以一种简洁明确的方式对其 进行模拟。 扩展有限状态机e f s m ( e x t e n d e d f i n i t e s t a t e m a c h i n e ) 用变量对f s m 进行扩 展。对于包含数据部分的协议来说，e f s m 可以精确简洁地对其进行描述。例如， i e e e8 0 22l l c 协议规范 a n s i 被描述为含有1 4 个控制状态，一定数目的变量 和一系列状态迁移，其中个典型的状态迁移为： c h r r e n t s t a t es e t u p i n p u ta c k _ t i m e re x p i r e d p r e d i c a t es _ v l a g = l o u q ，u tc o n n e c t c o n f i r m a c k o np f l a g ：2 旺r e m o t e b u s y 一0 n o ：t s t a t en o r m a l 其意味着当系统处于状态s e t u p 时，如果接收到输入信号 a c kt i m e re x p i r e d ，并且变量sf l a g 的值等于l ，那么系统将输出信号 c o n n e c tc o n f i r m ，将变量pf l a g 和r e m o t eb u s y 的值置为0 ，并移 到n o r m a l 状态。 2 。3 1e f s m 模型 定义2 2 扩展有限状蓉机e f s m ( e x t e n d e df i n i t es t a t em a c l u n e ) 可以形式地 表d 为一个6 元组 ，其中 s 是状态的有限集合，s o es 是初始状态； 中网科学技术大学f ，! 学位论文 基于模型检壹的协议一致性测试生成 第二掌现有的一致性测试序列和测试套生成方法 ，是输入交互( i n t e r a c t i o n ) 的有限集合： 0