（精密仪器及机械专业论文）协议一致性测试研究及测控系统形式化协议设计技术.pdf

东南大学博l 二学位论文摘要随着网络技术的发展，组建网络化测控系统已是现代测控工作者的重要任务，通信协议是网络的灵魂，如何设计出具有测控网络特点、功能上正确可靠，逻辑上完整的通信协议，并且系统地进行协议验证、协议测试和协议实现，已经成为一个非常具有挑战性的课题。论文致力于将近年来新兴的交叉学科一一协议工程引入测控领域。协议工程是一体化、形式化的协议开发过程。形式化协议理论是协议工程中一个重要的研究领域，论文的一个研究重点是：结合一简单的测控系统实例。详细讨论了协议形式化设计工作。具体包括协议文本设计技术、协议形式化描述技术以及基于形式化描述的协议验证、协议实现和协议一致性测试技术等。论文另一个研究重点是协议一致性测试。目前，常用于协议一致性测试的形式化模型主要是有限状态机( f s m ) ，论文基于f s m 模型讨论了一致性测试序列生成技术、执行技术及测试方法首先，对常见的u i o 序列生成技术进行比较研究，提出一种m u i o 生成算法。并成功应用于动态协议一致性测试工作中：在测试序列生成算法方面：对常见算法进行了比较研究，在此基础上，提出了一种基于u i o 的最短序列生成算法的改进算法；基于b u i o 概念提出了一种新的一致性测试序列的算法，算法利用m b u i o 序列、i l u i o 序列和叠加技术，只需计算i u t 的中国邮递员路径头节点的b u i o 和末节点的u i o ，其他状态的m b u i o 和删i o 序列则隐舍在测试序列之中，同时不需要像其他算法一样首先生成测试子序列，然后将其叠加串接，而是直接生成一个测试序列，通过b u i o 序列和u i o 序列的共同作用，扩大了算法的适用场合；在测试序列生成方法方面：提出了一种高效率、高可靠性的基于f s m 模型的u i o测试序列生成方法，通过数学模型的转换，利用l p 工具，快速、高效地获得测试序列，理论证明：对不含汇聚边的f s m ，l p 方法解最优：随后论文分析了传统静态测试方法的缺陷，提出了一种动态协议一致性测试算法利用测试树的概念将动态生成与动态执行相结合从而消除了测试问的冗余，提高了测试效率：最后论文从系统测试方法的角度讨论了主动测试和被动测试方法充分分析了两者的优缺点，提出环境配置测试方法。使被测试系统自动获得特定信息或者运行到特定状态，简化了准备阶段的测试行为同时能够实现对被测实现进行有针对性的测试。论文的研究工作不仅对学科交叉起到了重要推动作用，而且通过对协议一致性测试序列生成技术、动态协议一致性测试技术、环境配置测试方法等方面的研究在测试序列生成、序列执行、测试方法等层面具有指导意义与实用价值。关键词：协议工程；形式化技术；协议一致性测试；动态协议一致性测试东南大学博t 学位论文a b s t r a c tw i t ht h ed e v e l o p m e n to f t h en e t w o r kt e c h n i q u e ，c o n s t r u c t i n gm o d e r nm e a s u r e m e n ta n dc o n t r o ls y s t e mh a sb e c o m eac r u c i a lt a s kf u rm o d e r nm e a s u r e m e n ta n dc o n t r o le n g i n e e r a sw ek n o w , t h ec o m m u n i c a t i o np r o t o c o lh a sp l a y e dap r e d o m i n a n tr o l ei nn e t w o r k , a sr e s u l t , h o wt od e s i g nac o m m u n i c a t i o np r o t o c o l 。w h i c hn o to n l yc o r r e c ti nf u n c t i o na n di n t e g r a t e di nl o g i c ，b u ta l s oc 卸b ev a l i d a t e d ，t e s t e da n di m p l e m e n t e di ns y s t e m i cm a n n e rh a sb e c o m eav e r yc h a l l e n g e a b l ep r o b l e m t h i sp a p e rc o m m i t st oi n t r o d u c i n gp r o t o c o le n g i n e e r i n gi n t ot h ef i e l do fm e a s u r e m e n ta n dc o n t r o l ，w h i c hh a sb e c o m eab u r g e o n i n gi n t e r d i s c i p l i n a r ys u b j e c ti nr e c e n ty e a r s p r o t o c o le n g i n e e r i n gi s 彻i n t e g r a t e da n df o r m a lp r o t o c o ld e v e l o p m e n tp r o c e d u r e f o r m a lp r o t o c o lt h e o r yi sa ni m p o r t a n ts u b f i e l di nt h ep r o t o c o le n g i n e e r i n g ；t h i sp a p e rd i s c u s s e st h ep r o t o c o lf o r m a ld e s i g ni nd e t a i lb yi n t e g r a t i n gas e r i e so fs i m p l ye x a m p l e sf o rm e a s u r e m e n ta n dc o n t r o ls y s t e m w h i c hi n c l u d e sp r o t o c o lt e x td e s i g nt e c h n i q u e 。p r o t o c o lf o r m a ld e s c r i p t i o nt e c h n i q u e , f o r m a ld e s c r i p t i o nb a s e dp r o t o c o lv a l i d a t i o n , p r o t o c o li m p l e m e n t a t i o na n dc o n f o r m a n c et e s t i n gt e c h n i q u ee r e i na d d i t i o n , t h i sp a p e rf o c u s e so nt h ep r o t o c o lc o n f o r m a n c et e s t i n g t od a t e ，t h et r a d i t i o n a lf o r m a lm o d e lf u rp r o t o c o lc o n f o r m a n c et e s t i n gi sf i n i t e s t a t e m e c h a n i s m t h i sp a p e rd i s c u s s e st h es e q u e n c eg e n e r a t i n gt e c h n i q u e ，i m p l e m e n t i n gt e c h n i q u ea n dt e s t i n gm e t h o do fp r o t o c o lc o n f o r m a n c et e s t i n gb a s e do nt h em o d e lo ft h ef i n i t e - s t a t e - m e c h a n i s m a tf i r s t , t r a d i t i o n a lu i os e q u e n c eg e n e r a t i n gt e c h n i q u e sa r cr e s e a r c h e da n dc o m p a r e d a n dan e wm u l eg e n e r a t i n gm e t h o di sp r o p o s e dt oa p p l yi ts u c c e s s f u l l yt ot h ed y n a m i cp r o t o c o lc o n f o r m a n c et e s t i n g i nt h ec a s eo ft e s t i n gs e q u e n c e g e n e r a t i n ga l g o r i t h m ，a ni m p r o v e ds h o r t e s ts e q u e n c e - g e n e r a t i n ga l g o r i t h mf u ru i oi sd e v e l o p e db a s e do nt h ec o m p a r i s o na m o n gt h et r a d i t i o n a lt e s t i n gs e q u e n c ea l g o r i t h m s b e s i d e st h a t , an e wc o n f o r m a n c et e s t i n gs e q u e n c em e t h o di sp r e s e n t e db a s e do nb u i oc o n c e p t i o n , i nw h i c ht h en e wm e t h o dt a k e sa d v a n t a g eo fm b u i os e q u e n c e 。m u i os e q u e n c ea n do v e r l a pt e c h n i q u e ，e n l a r g e st h ea p p l i c a t i o nf i e l db yi n t e g r a t i n gb u i ow i t hu i os e q u e n c e i nt h ec a s eo ft e s t i n gs e q u e n c eg e n e r a t i o n , a l le f f i c i e n ta n dr o b u s tu i ot e s t i n gs e q u e n c eg e n e r a t i n gm e t h o di sp r o p o s e db a s e do nf s mb yt r a n s f o r m i n gt h em a t h e m a t i c a lm o d e la n de m p l o y i n gt h el pt 0 0 1 t h ef o l l o w i n gr e s e a r c hi nt h e o r ya n de x p e r i m e n t sc a np r o v et h a tt h el pc a ng e tt h eo p t i m a ls o l u t i o ni nt e r m so f n o n c o n v e r i n gf s m a n dt h e n , t h i sp a p e ra n a l y z e st h ed e f e c t so f t h et r a d i t i o n a ls t a t i ct e s t i n gm e t h o d ，a n dp r o p o s e sad y n a m i cp r o t o c o lc o n f o r m a n c e - t e s t i n ga l g o r i t h m i nt h i sa l g o r i t h m ，t h ed y n a m i cg e n e r a t i o ni sc o m b i n e dw i t hd y n a m i ci m p l e m e n t a t i o nb ym a k i n gu s eo fc o n c e p t i o no ft e s t i n gt r e et oe l i m i n a t et h et e s t i n gr e d u n d a n c ya n di m p r o v et h et e s t i n ge f f i c i e n c y f i n a l l y , t h ea c t i v ea n dp a s s i v et e s t i n gm e t h o di sd i s c u s s e df r o mt h ea s p e c to fs y s t e mt e s t i n gm e t h o di nt h i sp a p e a n dan e we n v i r o n m e n tc o n f i g u r a t i o nm e t h o di sp r e s e n t e dt oe n a b l et h e东南大学博 二学位论文t e s t i n gs y s t e ma c h i e v et h eg j v e ni n f o r m a t i o no rs t a t ea u t o m a t i c a l l y a sam o l t , t h et e s t i n go f t h ep r e p a r a t i v ec a nb es i m p l i f i e da n dt h ew h o l et e s t i n gs e q u e n c ec a nb em o r ep e r t i n e mt ot h es y s t e m t h es t u d yo f t h ep a l x * n o to n l yp l a y sad r i v e nf o r c ep a r to nt h es u b j e c t si o t e r c r o s s ，b u ta l s oh a ss o m es i g n i f i c a n c ei nt e s t i n gs e q u e n c eg e n e r a t i o n , s e q u e n c ei m p l e m e n t a t i o na n dt e s t i n gm e t h o db yr e s e a r c h i n go np r o t o c o lc o n s i s t e n tt e s t i n gs e q u e n c eg e n e r a t i o nt e c h n i q u e ，d y n a m i cp r o t o c o lc o n s i s t e n tt e s t i n gt e c h n i q u ea n de n v i r o n m e n tc o n f i g u r a t i o nt e s t i n gm e t h o d k e yw o r d s ：p r o t o c o le n g i n e e r i n g ：f o r m a lt e c h n i q u e ；p r o t o c o lc o n f o r m a n c et e s t i n g ：d y n a m i cp r o t o c o lc o n f o r m a n c et e s t i n g1 1 1东南大学博士学位论文缩略词3 g p p ( t h e3 r dg e n e r a t i o np a r t n e rp r o j e c t )第三代合作伙伴计划a s p ( a b s t r a c ts e r v i c ep r i m i t i v e )服务原语 t s ( a b s t r tt e s ts u i t e )抽象测试集c c i t t ( c o m m i t t e ec o n s u l t a t i v ei n t e r n a t i o n a lt e l e g r a p ha n dt e l e p h o n e ) 国际电报电c c s ( c a l c u l u so fc o n u n i c a t i o ns y s t e m s )c p p ( c h i n e s ep o s t m a np r o g r a m )c s p ( c o m m u n i c a t i o ns e q u e n t i a lp r o c e s s e s )c s p ( c o n s t r a i n ts a t i s f a c t i o np r o b l e m )d f s m ( d e t e r r a i n i s t i cf s m )d 方法( d i s t i n g u i s h i n gs e q u e n c e sm e t h o d )e b e ( e x t e r n a lb e h a v i o re x p r e s s i o n )e f s m ( e x t e n d e df s m )e p a ( e t h e r n e tf o rp r o c e s sc o n t r 0 1 )话咨询委员会通信系统演算中国邮递员问题通信顺序进程约束满足技术确定有限状态机区分序列法即d 方法外部行为描述形式化模型扩展有限状态机用于工业测量与控制系统的e p a 系统结构与通信标准e s t e l l e ( e x t e n d e ds t a t et r a n s i t i o nl a n g u a g e )扩展状态变迁语言e t s ( e x e c u t a b l et e s ts u i t e )可执行测试集e t s i ( e u r o p e a nt e l e c o m u n i c a t i o n ss t a n d a r d si n s t i t u t e )欧洲电信标准协会h y r ( f o r m a ld e s c r i p t i o nt e c h n i q u e )形式化描述技术f s m ( f i n i t es t a t em a c h i n e )有限状态机f r s c ( t h ef e d e r a lt e l e c o m m u n i c a t i o n s s t a n d a r d sc o m m i t t e e )联邦电信标准委员会i e e e ( t h ei n s t i t u t eo fe l e c t r i c a la n de l e c t r o n i c se n g i n e e r s )电子电气工程师协会i s o ( i n t e r n a t i o n a ls t a n d a r d so r g a n i z a t i o n ) 数据通信领域中最重要的国际化标准组织i t r r ( i m p l e m e n t a t i o nu n d e rt e s t )被测实现i t u - t ( i n t e r n a t i o n a lt e l e c o m u n i c a t i o nu n i o n t )国际电信联盟标准部l o t o s ( l a n g u a g eo ft e m p o r a lo r d e r i n gs p e c i f i c a t i o n )时间顺序规格语言l t ( l o w e rt e s t e r )测试系统中下测试器m s c ( m e s s a g es e q u e n c e sc h a r t )消息序列图n f s m ( n o n - d e t e r m i n i s t i cf s m )非确定有限状态机p c o ( p o i n to fc o n t r o la n do b s e r v a t i o n )测试系统中控制观察点p d u ( p r o t o c o ld a t au n i t )协议数据单元p l ( p r e d i c tl o g i c )谓词逻辑i v东南大学博t 学位论文p i c s ( p 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 a n c es t a t e m e n t )协议一致性申明条款p i x i t ( p r o t o c o li m p l e m e n t a t i o ne x t r ai n f o r m a t i o nf o rt e s t i n g ) 被测协议实现的附加信息s d l ( s p e c i f i c a t i o na n dd e s c r i p t i o nl a n g u a g e )规格化描述语言s i ( s t a t ei d e n t i f y )状态验证t 方法( t r a n s i t i o nt o u rmethod)t方法t c ( t e s tc a s e )测试用例t c p ( t e s tc o o r d i n a t i o np r o c e d u r e s )测试协调过程t l ( t e n s el o g i c )时态逻辑t s t ( t e s ts u i tt r e e )测试用例树t t c n ( t r e ea n dt a b u l a rc o m b i n e dn o t a t i o n )树型表格联合表示法o l o 方法( u n i q u ei n p u t o u t p u ts e q u e n c e sm e t h o d )唯一输入输出序列法即u 方法u i o 序列( u n i q u ei n p u t o u t p u ts e q u e n c e s )唯一输入输出序列即o l o 序列o t ( u p p e rt e s t e r )测试系统中上测试器- 方法( c h a r a c t e r i n gs e q u e n c e sm e t h o d )特征序列法也称_ 方法v东南大学学位论文独创性声明本人声明所呈交的学位论文是我个人在导师指导下进行的研究工作及取得的研究成果。尽我所知，除了文中特别加以标注和致谢的地方外，论文中不包含其他人已经发表或撰写过的研究成果，也不包含为获得东南大学或其它教育机构的学位或证书而使用过的材料。与我一同工作的同志对本研究所做的任何贡献均已在论文中作了明确的说明并表示了谢意。研究生签名：垒鸷e t 期：兰蔓。i东南大学学位论文使用授权声明东南大学、中国科学技术信息研究所、国家图书馆有权保留本人所送交学位论文的复印件和电子文档，可以采用影印、缩印或其他复制手段保存论文。本人电子文档的内容和纸质论文的内容相一致。除在保密期内的保密论文外，允许论文被查阅和借阅，可以公布( 包括刊登) 论文的全部或部分内容。论文的公布( 包括刊登) 授权东南大学研究生院办理。研究生签名：圣l - 耻导师签名：e t 期：。7 一f第一章引言第一章引言1 1 课题的研究背景及意义随着网络技术的发展。组建网络化测控系统已是现代测控工作者的重要任务，通信协议是网络的灵魂，如何设计出满足测控系统特点的、功能上正确可靠，逻辑上完整的通信协议，并且系统地进行协议验证、协议测试和协议实现。已经成为一个非常具有挑战性的课题。论文致力于将近年来新兴的交叉学科一一协议工程1 2 l1 3 j b l a 测控领域，为网络化测控技术及网络仪器技术的发展添砖加瓦1 1 1 网络化测控技术是现代测控技术重要发展方向之一随着科学技术的高速发展，要求处理的信息量愈来愈大、速度要求愈来愈快；且测控对象空间位置亦较分散，测试对象愈来愈多，测试系统愈来愈庞大为此测控系统出现了现场化、远程化、网络化的需求1 4 1 1 5 l 【6 】。传统的自动测试系统正从g p i b 、v x i 、p x i 、l x i 的集中式向分布式发展，将测控系统中空间上分散的基本功能单元( 计算机、测试仪器、铡试模块、传感器、控制模块等) 通过网络联系起来，形成网络化测控系统。网络化测控系统将传统的测控技术与网络技术相结合构成信息采集、传输、处理和应用的综合网络，顺应信息化发展的要求，借鉴信息网络发展的新技术。必能高速发展网络化测控技术1测控系统网络特点测控网络与信息网络相比，具有共性，亦具有自身特点：( 1 ) 测控网络特别强调系统响应的实时性和响应时间的确定性，此是工业控制网络的重要指标之一以太网由于采用c s l i a c d ( 载波侦听多路访问冲突检测) 介质访问控制机制，因此具有通信不确定性的特点，并成为其应用于工业数据通信网络的主要障碍。虽然以太网交换技术、全双工通信技术以及i e e e 8 0 2 1 p & q 规定的优先级技术在一定程度上避免了碰撞，但也存在着一定的局限性：以太网交换机的存储转发机制同样使通信延迟具有不确定性。通信延迟的不确定性主要来自于其排队延迟。无论采用哪种存储转发机制，当同时来t l 于多个端口的报文需要向同一东南大学博l 学位论文个端口转发时，交换机就必须将这些报文进行排队缓冲，并依次转发。因此，交换机的缓冲池大小将直接影响了来自于某一端口的报文能否以及何时被成功转发。以太网交换机存在的“广播风爆”问题。工业数据通信网络中广泛采用广播方式发送的实时数据报文，同样会产生碰撞。除了通信实时性要求外，测控网络的通信还具有以下特点：( 2 ) 周期与非周期信息同时存在，正常工作状态下，周期性信息( 如过程测量与控制信息、监控信息等) 较多，而非周期信息( 如突发事件报警、程序上下载等) 较少；( 3 ) 有限的时间响应，一般办公室自动化计算机局部网响应时间可在几秒范围内，而工业控制局域网的响应时间应在0 o l 1 秒；( 4 ) 信息流向具有明显的方向性，通信关系比较确定。正常工作情况下变送器只需将测量信息传送到控制器，而控制器则将控制信息传送给执行机构，来自现场仪表的过程监控与突发时间信息则传向操作站，操作站一般只需将下载的程序或配置数据传送给现场仪表等；( 5 ) 根据组态方案，信息的传送遵循严格的时序；( 6 ) 测控网络传输的信息以短帧为主，且信息交换频繁，此特点要求网络协议简单实用、效率高，对网络的吞吐量要求不高。( 7 ) 网络负荷较为平稳。( 8 ) 工业现场测控网络一般要求能总线供电。工业现场测控网络不仅能传输通信信息，而且要能为现场设备的传输工作提供电源。2网络化测控系统需要解决的一些关键技术组建测控系统的测控网络以前使用的多为现场总线，但现场总线种类繁多，多种现场总线技术并存、现场总线技术标准不统一( d e v i c e n e t 、f i e l d b u sh i 、p r o f i b u s 、h a r t ) ，给用户带来不便。由于低成本和高性能，信息网络e t h e r n e t 已经渗透到工业控制中。网络速度的高速提升，使得e t h e r n e t 因碰撞而引起的信息传输时间的随机性已被大大降低，其越来越适应工业控制系统的实时性要求。实时性测控网络必须满足两个主要的技术指标：给定范围的时延和高度可保证的传输即信息在限定的延时范围内被成功地传输；需要在以太网和t c p i p 协议之上建立完整有效的通信服务模型制定有效的实时通信服务机制和实时通信服务质量( q s ) 支持策略，形成为广大工控生产商及用户所接受的应用层、用户层协议t 进而形成开放的标准。可靠性和安全性系统的软硬件应进行环境适应性要求的可靠性设计；硬件模块和网络体系的故障诊断、隔离和恢复技术；为防止可能受到的病毒、黑客的非法入侵等必须对系统进行安全性设计2第一章引言近年来。国内外出现了许多组织从事工业e t h e r n e t 技术研究，取得了一些成果。国内：浙江大学与浙大中控等联合推出了基于e p a ( e t h e r n e tf o rp l a n ta u t o m a t i o n )分布式网络控制系统。在解决了以太网用于工业现场设备间通信的确定性通信调度、总线供电、网络安全、可互操作等关键技术的基础上，起草的我国第一个拥有自主知识产权的现场总线国家标准，是我国第一个被国际认可和接受的工业自动化领域的标准。国外：国际上一些组织也正积极研究将e t h e r n e t 技术应用于工业控制现场的相关技术和标准：在实时以太网技术中，将有e t h e r c a t 、e t h e r n e tp o w e r l i n k 、p r o f i n 盯、h o d b u s - i d a和e t h e r n e t i p 等5 个主要的竞争者。到目前为止可以将工业以太网的实时响应时间做到5 l o m s ，相当于现有的现场总线。工业以太网在技术上与商用以太网是兼容的，对于响应时间小于5 m s 的应用。工业以太网已不能胜任，为了满足高实时性能应用的需要。各大公司和标准组织纷纷提出各种提升工业以太网实时性的技术解决方案。在i e e e8 0 2 3 标准的基础上，通过对其和相关标准的实时扩展以提高实时性，并且做到与标准以太网的无缝连接出现了实时以太网( r e a lt i m ee t h e r n e t ，简称r t e ) 。2 0 0 3 年5 月。i e c s c 6 5 c 专门成立了w g ll 实时以太网工作组，负责制定i e c6 1 7 8 4 2 “基于i s o i e c8 8 0 2 3 的实时应用系统中工业通信网络行规”垂国际标准，该标准包括c o m m u n i c a t i o np r o f i l ef a m i l y2e t h e r n e t i p 、c p f 3p r o f i n e t 、c p f 4p n e t 、c p f 6i n t e r b u s 、c p f i ov n e t i p 、c p f i lt c n e t 、c p f l 2e t h e r c h t 、c p f l 3e t h e r n e tp o w e r l i n k 、c p f l 4e p ( 中国) 、c p f l 5m o d b u s t c p 以及c p f l 6s e r c o s 等1 1 种实时以太网行规集。根据实时以太网实时扩展的不同技术方案，可将实时以太网通信协议模型分为5 类，( 1 ) 经过常规最大努力提高实时性的基于一般工业以太网的通信协议模型；( 2 ) 采用在t c p i p 之上进行实时数据交换方案的实时以太网通信协议模型；( 3 ) 采用经优化处理和提供旁路实时通道的通信协议模型；( 4 ) 采用集中调度提高实时性的实时以太网通信协议模型；( 5 )采用类似i n t e r b u s 现场总线“集总帧”通信方式和在物理层使用总线拓扑结构提升以太网实时性能的实时以太网通信协议模型。为了提高系统实时性，e t h e r n e t 协议出现了改进型版本：如r e n l e r 、r t c c 等。目前，网络化测控技术利用现有的通信网络构建网络化测控系统，这需要测控技术学者掌握协议实现技术；同时，针对测控系统特点研究新型网络协议一一要求建立完整有效的通信服务模型、制定有效的通信机制，此要求测控技术学者掌握协议设计技术，协议设计技术是网络化测控技术学者致力研究的一个重要方向。论文致力于将近年来新兴的交叉学科一一协议工程引入测控领域。八十年代，欧美率先开展此方面的研究，取得了阶段性成果。近年来，我国在计算机、通信领域亦开展了这方面的研究工作，将此引入测控技术领域有着至关重要的意义，使用形式化描述技术f d t ”“”不仅使协议开发变得规范化拥有了验证、仿真、联合仿真测试机制，使开发者尽可能早的获东南大学博士学位论文知协议缺陷，最大限度的检测和纠正死锁活锁、不可执行等行为进行协议完善克服非形式化验证是基于设计者的工作经验，缺乏数学严密性和科学性的缺点，而且缩短了协议开发周期，给传统测控技术赋予了新的内容，给测控工作者提出了一个前所未有的机遇和挑战。1 1 2 协议工程协议工程是2 0 世纪8 0 年代才发展起来的一门非常活跃的新兴学科。它采用形式化的方法贯穿于严格的协议设计和维护中是研究以协议为对象的软件工程但所建立的协议设计方法比现有软件工程的一般方法更严格，从而使协议开发“一体化”( i n t e g r a t e d ) 和“形式化”( f o r m a l ) ，它的宗旨是为协议软件的研制和开发提供一整套工程规范。一体化即系统化，其含义是：协议的设计、验证、实现和测试，在技术上前后衔接，并在同一个开发系统中完成。而形式化；是指将协议以及由协议提供的服务用形式化描述方法描述出来。协议工程包括形式化描述、协议验证、协议综合、协议实现、协议测试等多方面的理论和技术。在这些形式化技术中，形式化描述与验证技术是整个协议设计与实现的基础，关联了协议工程中的各个过程，对协议实现的正确性、完整性和复杂度有至关重要的影响；协议测试包括测试被测协议实体与形式化描述的一致性以及协议实体的互操作性和性能测试，其中一致性测试是基础。“协议”最早是由r a s c a n t l e b u r y 和k a b a r l e t t ，于1 9 6 7 年4 月在英国国家物理实验室的一份题为死锁( d e a d l o c k s )协议处于非终止状态，但是没有事件可以发生。如所有的协议进程都在等待某个不可能被满足的条件。活锁( l i v e l o c k s )执行序列进行未定义的循环，而协议却没有取得有效的进展。非正常终止( i m p r o p e rt e r m i n a t i o n ) ；( 2 ) 不完备性错误( i n c o m p l e t e )1 3东南大学博上学位论文未定义报文接受( u n s p e c i f i e dr e c e p t i o n ) ，即接收方并没有预测到该报文的到达，也不知道如何对之响应。参见附录实例。( 3 ) 超规范错误( o v e r - s p e c i f i e d )存在不可达状态或不可执行事件。( 4 ) 模糊状态( a m b i g u i t ys t a t e )存在意义模糊，容易产生歧义状态。2 3 2 通信协议基本性质一个。好”的协议( w e l l f o r m e dp r o t o c 0 1 ) 应该具有：活跃性、安全性、一致性和完备性等。协议的活跃性指协议运行时一些“好”事情一定会发生这些好的事情包括：预定的事件会产生；指定的协议状态会达到；应该进行的协议行动会进行协议的活跃性体现在终止性( t e r m i n a t i o n ) 和进展性( p r o g r e s s ) 两个方面，或者说，如果协议有终止性和进展性，它就有活跃性。终止性是指协议从任何一个状态开始运行。总能正确地达到终止状态；进展性是指协议从初始状态运行总能正确地达到指定状态；回归性( r e c u r r e n c e 或是c y c l i o g ) 是指某些情况下终止状态和初始状态是同一的。这样，协议从初始状态开始运行总能正确的回到初始状态并可反复运行，所以可以说回归性= 终止性+进展性= 活跃性。安全性指协议运行时。坏”事情不会出现，这些坏事情包括不可接收的事件、不可进一步向前的状态、错误的行动、错误的条件、变量值越界( o v e r f l o w ) 等等。坏事情一般导致两种结果：死锁和活锁。协议一致性指协议所描述的服务( s e r v i c e ) 和协议行为一致：如果第n 层协议的用户所要求的服务以及它所能观察到的服务性质与第n 层协议内部机制所表现出的总体行为和性质是一致的。那么协议就具备一致性。一致性包括两个方面：协议应该提供用户要求的服务；协议无需提供用户没有要求的服务完备性指协议性质完全符合协议环境的各种要求，即协议的构造考虑了用户要求、用户特点、通道性质、工作模式等各种潜在因素的影响，考虑了各种错误事件、异常情况的处理。为了使一个复杂的通信协议是一个“好”协议，必须使用形式化描述方法为协议提供规范化描述和可靠的检测手段。通过对协议的形式化描述，能够正确地、无歧义地表达协议设计标准，并根据此标准使用形式化分析技术，对协议进行有效地验证和测试。2 3 3 协议验证基本方法形式化验证即利用形式化技术中的相关理论进行协议验证。协议验证是一门涉及数理逻4第二章形式化协泌设计技术辑、时态逻辑以及图论等多项基础理论的新兴技术。协议验证是对协议的功能和性能进行校验的过程，是保证协议开发质量的必要环节。形式化验证既可以发现原协议描述中的逻辑错误“，又可以发现在形式化描述过程中，由于对原协议理解不当而增加的逻辑错误。协议形式化验证首先需要对协议性质进行系统的语言描述，然后基于协议的形式化模型或者形式化语言描述，通过适当的技术对协议性质进行分析验证。协议验证包括两种形式：静态分析和动态分析。静态分析是从描述的静态形式入手对协议的上下文无关语法、作用域规则以及其它的语义进行检查，通常是通过使用某一描述工具的编译器完成的，它不涉及描述的执行过程。而动态分析需要考虑系统的动态行为，即被描述系统的执行行为，同时它可检测出静态分析检测不出来的某些协议错误。图2 2 协议验证方法动态分析方法主要有三大类，如图2 2 所示。第一类方法是逻辑证明，致力于证明协议设计中没有错误。这类方法认为检测不到错误并不能说明协议设计中没有错误，认为证明没有错误比检测协议设计中错误更为重要i ”。逻辑证明是运用推理验算方法严密地证明协议各种性质，证明通过一系列步骤完成，每一个步骤都从一组假设中推导出一个结果，所采用的推理验算技术主要来自于时态逻辑t l 、谓词逻辑p l 、代数验算等数学领域。c l o s ec o v e r 技术盼4 ”就属于这一类协议验证方法。逻辑证明中包含不变性证明l “4 q 和等价性证明【拍4 7 1 等。不变性是指如果一个通信协议系统的某个性质能够用一个确定的逻辑表达式描述，并且不随系统状态和执行序列的变化而改变，那么这个性质就称为系统的不变性。系统不变性分析包含两部分工作：( 1 )完全正确地找出协议系统的不变性质，形成严格定义的不变性表达式；( 2 )以某种方法执行协议，验证不变性表达式是否恒为真。通常意义上的不变性证明指的是第二项工作。等价性是指如果两个通信协议形式化描述或协议规范在某种程度上“相同”和“无差别”，那么它们可以互相替换，如果一个正确，那么另一个也正确。第二类方法是可达性分析。可达性分析是试图产生和检查协议所有或部分可达状态，进而检验基于状态或者基于状态序列的协议性质。所谓可达状态是指协议从初始状态开始经历有限次状态转换之后可达到的状态，所有可达状态构成了系统可达状态空间。可达性分析算法是用来生成并检验一个特定的初始状态可达的所有状态的算法，主要包括：穷尽搜索( f u l ls t a t es p a c es e a r c h ) 、受控部分搜索( c o n t r o l l e dp a r t i a ls e a r c h ) 、随机搜索( r a n d o mw a l k ) 东南大学博上学位论文这类方法相信检测出错误并修正错误的过程具有非常重要的实用价值，认为尽管检测不到错误并不能说明协议设计中没有错误，然而当出现错误的概率小于一定标准时。在工程应用中是可以接受的。目前大部分的协议验证技术属于这种情况。可达性分析技术由于具有较强的工程应用背景受到广泛的关注，许多学者对此进行了深入的研究。m g g o u d a 在 3 9 中提出了c l o s ec o v e r 协议验证方法。s i m o n 等提出了局部协议验证技术，局部协议验证不是把所有进程的执行看成一个整体，而是分别考虑各个进程的所有执行构造出n 个包含整体信息的局部树局部树中的每一个状态由总的可达树中的一些全局状态合并得到，避免了构造全局可达树。还有一些学者提出了一些改进的协议验证技术：公平可达性分析及其扩展f 9 “”i 、最大前进状态搜索( m a x i m a lp r o g r e s ss t a t ee x p l o r a t i o n ) 州、一r e p l a c e m e n t 技术岬l 、协议映射( p r o t o c o lp r o j e c t i o n ) i a “，v u o n g和c o w a n 在 5 5 提出了分解图法，对话矩阵( d u o l o g u e m a t r i x ) 分析法及其扩展体现于 5 6 。基于并发路径的协议验证方法在 5 7 ，5 8 。5 9 中得到讨论。为了降低复杂度，研究者利用各种不同的方法试图只搜索全局树中最有可能发生的一部分或者起着更重要作用的部分，这些方法中有概率搜索、启发式搜索等等。一般来讲。这些技术比上面提到的技术更有效，代价是并不能保证协议没有错误。如：概率验证【5 9 ”“6 2 。“，启发式搜索，随机状态搜索( r a n d o ms t a t ee x