（计算机应用技术专业论文）协议形式化模型及建模技术研究.pdf

浙江理工大学硕士学位论文 摘要 协议是网络的血液和生命，计算机网络的发展是网络协议设计和开发的结果。随着通 信网络向着高速度、高性能、多媒体等方向的发展，协议变得越来越复杂，通信协议的设 计已经成为通信网络设计和实现的关键。 本文首先介绍协议工程和基本的形式化模型。这些模型包括：有限状态机、扩展有限 状态机、p e t r i 网、进程代数、时态逻辑和抽象数据类型。它们是协议工程的理论基础和 核心技术。 然后对形式化描述语言的三个国际标准( s d l 、e s t e l l e 、l o t o s ) 进行了深入分析。 指出了这三种形式化描述语言在描述协议模型方面的不足：它们都只能支持协议工程活动 的某几个环节。统一建模语言u m l 支持软件工程中从需求分析到设计实现部署的各个阶 段。所以，u m l 在协议工程中的应用已经成为国内外一个研究热点。u m l 语言可能是一种 更为理想的协议形式化描述语言。 最后深入研究了模型驱动构架m d a 、u m l 及其建模技术，重点是u m l 类图和状态 图。但是u m l 在描述状态机的行为时，缺乏清晰和严格的行为语义，导致不能直接用它 来开发复杂协议。因此必须给u m l 增加行为语义。标准的形式化描述语言均提供了严格 准确完备的行为语义。所以，如何将u m l 和标准的形式化描述语言融合起来是研究重点。 本文的创造性工作主要如下： 提出u m l 状态图的交互抽象状态机模型i a s m s 。并用i a s m s 定义了一种具有消 息传送功能的u m l 状态图的形式化语义。 研究基于m d a 的协议建模技术。利用u m lp r o f i l e 机制，定义了一种“基于m d a 的协议建模语言l _ 交互抽象状态机描述语言i a s m s d l 。基于m d a 的p i m p s m 思想，开发了一个u m l 模型信息提取器r 2 t s p d l ，定义了从u m l 模型到s d l 模型的变换规则。 本文的研究成果已应用于导师承担的浙江省重点科技攻关项目“通信协议一致性测试 集自动生成软件”之中，用于对被测协议的形式化建模并提取出后续用于协议一致性测试 的模型信息。该项目是研究基于模型驱动构架的协议一致性测试集的自动生成。 关键词：协议工程，形式化模型，m d a ，u m l ，形式化语义 浙江理工大学硕士学位论文 a b s t r a c t p r o t o c o li st h eb l o o da n dl i f eo fn e t w o r k t h ed e v e l o p m e n to fc o m p u t e rn e t w o r ki st h e r e s u l to f i t sp r o t o c o l sd e s i g na n dd e v e l o p m e n t w i t ht h ec o m m u n i c a t i o nn e t w o r kd e v e l o p i n gt o t h ed i r e c t i o no f h i 曲s p e e d 、h i g hp e r f o r m a n c e 、m u l t i m e d i aa n ds oo n , p r o t o c o lh a sb l n c o m em o r e a n dm o r ec o m p l e x t h ed e s i g no fc o m m u n i c a t i o np r o t o c o lh a sb e c o m et h ek e yo ft h ed e s i g n a n dr e a l i z a t i o uo f c o m m u n i c a t i o nn e t w o r k f i r s t , i n t r o d u c et h ep r o t o c o le n g i n e e r i n ga n dt h eb a s i cf o r m a lm o d e l s n em o d e l si n c l u d e ： f i n i t es t a t em a c h i n e 、e x t e n d e df i n i t os t a t em a c h i n e 、p e t r in e t 、p r o c e s sa l g e b r a 、t e m p o r a l l o g i ca n da b s t r a c td a t at y p e t h e ya r et h et h e o r yf o u n d a t i o n sa n dc o r et e c h n i q u e so ft h e p r o t o c o le n g i n e e r i n g t h e n , t h o r o u g h l ya n a l y z et h et h r e ei n t e r n a t i o n a l s t a n d a r d so f f o r m a ld e s c r i p t i o n l a n g n a g e ( s d l 、e s t e l l e 、l o t o s ) p o i n to u tt h ei n s u f f i c i e n c yo ft h et h r e el a n g u a g e si n d e s c r i b i n gp r o t o c o lm o d e l s ：e a c ho n ec a no n l ys u p p o r ts e v e r a lp h a s e so ft h ep r o t o c o l e n g i n e e r i n g t h eu a l f i e dm o d e l i n gl a n g u a g eu m ls u p p o r t st h ee a c hp h a s e ，f r o mt h es o f t w a r e d e m a n da n a l y s i st ot h ed e s i g nr e a l i z a t i o nd e p l o y m e n t t h e r e f o r e ，t h ea p p l i c a t i o no f u m li nt h e p r o t o c o le n g i n e e r i n gh a sb e c o m eah e a t e dp o i mo fr e s e a r c hi nt h ew o r l d u m lm a y b eam o r e p e r f e c tp r o t o c o lf o r m a ld e s c r i p t i 蚰l a n g u a g e i nf i n a l ，r e s e a r c ht h o r o u g h l yo nm o d e ld r i v e na r c h i t e c t u r em d a 、u m la n di t sm o d e l t e c h n i q u e t h ee m p h a s i so f t h er e s e a r c hi st h eu m l c l a s sd i a g r a m sa n ds t a t e c h a r t s b u tu m l l a c k st h ec l e a ra n ds t r i c tb e h a v i o rs e m a n t i c st od e s c r i b et h es t a t e m a c h i n e sb e h a v i o r , w h i c h r e s u l t st o 啪n o ts t r a i g h t l yd e v e l o pt h ec o m p l e xp r o t o c o lw i t hu m l t h u sw em u s te n h a n c e u m ls o m eb e h a v i o rs e m a n t i c s t h es t a n d a r df o r m a ld e s c r i p t i o nl a n g u a g e sh a v ep r o v i d e dt h e s t r i c ta n da c c u r a t es e m a n t i c s t h e r e f o r e ，h o wt os y n c r e t i z eu m la n dt h es t a n d a r df o r m a l d e s c r i p t i o nl a n g u a g e si st h ei m p o r t a n tp a r to f t h er e s e a r c h 1 1 1 em a i nc r e a t i v i t i e so f t h i sd i s s e r t a t i o na r ee x p l a i n e d 髂f o l l o w s ： p r o p o s ea ni n t e r a c t i v ea b s t r a c ts t a t em a c h i n e sm o d e li a s m so f u m l s t a t c c h a r t s a n d d e f i n eas t a t e c h a r t sf o r m a ls e m a n t i c sw i t l lm e s s a g e - p a s s i n gu s i n gi a s m s r e s e a r c ho nt h ep r o t o c o lm o d e lt e c h n i q u eb a s e do nt h em d a d e f i n ea p r o t o c o l m o d e l i n gl a n g u a g eb a s e do nt h em d a 一一i n t e r a c 吐v ea b s t r a c ts t a t em a c h i n e s d e s c r i p t i 0 1 1l a n g u a g ei a s m s d lu s i n gt h eu m lp r o f i l em e c h a n i s m b a s e do nt h e n 浙江理工大学硕士学位论文 m d ai d e ao fp i m p s m d e v e l o pau m lm o d e li n f o r m a t i o ne x t r a c t i o nr 2 t s p d la n d i n f l k et r a n s f o r m a f i o nr u l e sf r o mu m lm o d e lt os d lm o d d t h er e s e a r c hr e s u l to ft h i sd i s s e r t a t i o ni sa p p l i c a b l ei nt h es c i e n c ec r u c i a lp r o j e c to f z h e j i a n gp r o v i n c e ，t h ea u t o m a t i cg e n e r a t i o ns o f t w a r eo fc o m m u n i c a t i o np r o t o c o lc o n f o r m a n c e t e s ts u i t e s , m a n a g e db ym yt u t o r t h er e s u l ti su s e dt om a k et h ef o r m a lm o d e lf o rt h et e s t e d p r o t o c o la n de x t r a c tt h em o d e li n f o r m a t i o nf o r t h es u c c e e d i n gp r o t o c o lc o n f o r m a n c et e s t t h e p r o j e c tr e s e a r c h e st h ea u t o m a t i cg e n e r a t i o no fc o m m u n i c a t i o np r o t o c o lc o n f o r m a n c e t e s ts u i t e s b a s e do nt h em o d e ld r i v e n a r c h i t e c t u r e 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 lm o d e l ，m o d e ld r i v e na r c h i t e c t u r e , u n i f i e d m o d e l i n gl a n g u a g e ，f o r m a ls e m a n t i c s l i i 浙江理工大学硕士学位论文 术语表 a bp r o t o c o l ： a l t e r n a t i n g b i tp r o t o c o l 交换位协议 a d t ：a b s w a c td a t at y p e 抽象数据类型 a s m s ：a b s t r a c ts t a t em a c h i n e s抽象状态机 b n f - b a c k u sn o r m a lf o r m u l a巴科斯范式 c a s e ： c o m p u t e x - a i d e ds o f t w a r ee n g i n e e r i n g计算机辅助软件工程 c c s ：c a l c u l u so f c o m m u n i c a t i o ns y s t e m s通信系统演算 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 t i l ： c o m p u t a t i o n t r e et e m p o r a ll o g i c计算树时态逻辑 c w m ：c o m m o nw a r e h o u s em e t a m o d e l 公共仓库元模型 d o m ：d o c u m e n t o b j e c tm o d e l文档对象模型 d t d s ：d o c u m e n t t y p ed e f i n i t i o n s 文档类型定义 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 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 nm o d e ll a n g u a g e扩展有限状态机语言 f d l ：f o r m a ld e s c r i p t i o nl a n g u a g e形式化描述语言 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形式化描述技术 f o l t l ：f i r s t - o r d e rl i n e a rt e m p o r a ll o g i c 一阶线性时态逻辑 f s m ：f i n i t es t a t em a c h i n e有限状态机 g p d l ： g r a p h i c a lp r o t o c o ld e s c r i p t i o nl a n g u a g e 图形协议描述语言 i a s m s ：i n t e r a c t i v ea s m s交互抽象状态机 i a s m s d l ：i a s m sd e s c r i p t i o nl a n g u a g e交互抽象状态机描述语言 lil：larchi n t e r f a c el a n g u a g el a r c h 接口语言 l o t o s ：l a n g u a g eo f t 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时序规范语言 lsl：larchs h a r e dl a n g u a g el a r c h 共享语言 m d a ：m o d e ld r i v e na r c h i t e c t u r e模型驱动构架 m o f ： m e t a - o b j e c tf a c i l i t y 元对象设施 m s c ： m e s s a g es e q u e n c ec h a r t s 消息序列图 o c l ： o b j e c tc o n s t r a i n tl a n g u a g e对象约束语言 o l e ： o b j e c tl i n k i n ga n de m b e d d i n g对象连接与嵌入 o m g ： o b j e c tm a n a g e m e n tg r o u p对象管理组织 v i 浙江理工大学硕士学位论文 p i m ：p l a t f o r m i n d e p e n d e n tm o d e l 平台独立模型 p s m ：p l a t f o r m s p e c i f i cm o d e l 平台相关模型 p u m l ： p r e c i u m l精确u m l r t f ：r e v i s i o nt a s kf o r c e su m l 修订任务组 r 2 t s p d l ：r o s e - t o t s p d lu m l 模型信息提取器 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 v g ：s e a l a b l ev e c t o rg r a p h i c s可缩放矢量图形 tl：temporall o g i e 时态逻辑 t s p d l ：t e x t u a ls p e c i f i c a t i o np r o t o c o ln e s c d p t i o nl a n g u a g e 文本规格协议描述语言 t s p d l 2 s d l ：t s p d l - t o s d lt s p d l 2 s d l 编译器 u m l ：u n i f i e dm o d e l i n gl a n g u a g e统一建模语言 v d m ： v i e n n a d e v e l o p m e n tm e t h o d 维也纳开发方法 x m i ：x m l b a s e dm e t a d a t ai n t e r c h a n g e基于x m l 的元数据交换 x m l ：e x t e n s i b l em a r k u pl a n g u a g e可扩展标记语言 x u m l ：e x e c u t a b l eu m l可执行u m l i 浙江理工大学学位论文原创性声明 本人郑重声明：我恪守学术道德，崇尚严谨学风。所呈交的学位论文，是本人在导师 的指导下，独立进行研究工作所取得的成果。除文中已明确注明和引用的内容外，本论文 不包含任何其他个人或集体已经发表或撰写过的作品及成果的内容。论文为本人亲自撰 写，我对所写的内容负责，并完全意识到本声明的法律结果由本人承担。 学位论文作者签名：律f 虱嗣 日期：岬年，月叩日 浙江理工大学学位论文版权使用授权书 学位论文作者完全了解学校有关保留、使用学位论文的规定，同意学校保留并向国家 有关部门或机构送交论文的复印件和电子版，允许论文被查阅或借阅。本人授权浙江理工 大学可以将本学位论文的全部或部分内容编入有关数据库进行检索，可以采用影印、缩印 或扫描等复制手段保存和汇编本学位论文。 本学位论文属于 保密口，在 不保密口 学位论文作者签名： l 萍闯峨 醐：1 年妒哆日 年解密后使用本版权书。 指导教师签名：酬 日期：唧年，月妇日 浙江理工大学硕士学位论文 1 1 研究背景及意义 第一章引言 随着计算机网络技术应用的日益普遍，新一代通信网络朝着数字化、智能化、个人化 和综合化方向发展，网络提供的服务由传统的通信服务转向信息服务。软件规模急剧增大， 结构也越来越复杂，这就给通信网络协议的开发带来许多困难。同时，网络系统的复杂性 在协议方面体现出空间分布性、并发性、异步性、不稳定性、多样性和实时性等特点，通 信网络协议再也不可能用工程直觉方法设计出高质量的协议。因此，采用协议工程( p r o t o c o l e n g i n e e r i n g ) l q 的方法设计出功能上正确可靠、逻辑上一致完整和易于有效实现的通信网络 协议，并且使整个设计和实现的过程更加规范化和自动化，从而提高通信协议软件的生产 率、可靠性和可维护性，促进标准化的实现，已经成为一个十分重要和富有挑战性的研究 课题。 2 0 0 2 年初，对象管理组织( o b j e c tm a n a g e m e n tg r o u p ，o m g ) 宣布：模型驱动构架( m o d e l d r i v e n a r c h i t e c t u r e ，m d a ) 【2 l 是它的战略方向。1 9 9 7 年o m g 定义了第一个面向对象建模标 准统一建模语言( u n i f i e dm o d e l i n gl a n g u a g e 。u m l ) 口 4 】，当o m g 提出m d a 时，可以 说是顺其自然迈出的下一步。从科学研究发展趋势看，m d a 很可能就是软件开发方式的 下一个重大进步，m d a 是一种将会对未来i t 技术产生重大影响的开发方法学。 在o m g 内部，m d a 从系统和软件供应商群体中获得了异乎寻常的强有力支持。i b m ， s u n ，m i c r o s o f t 在支持m d a 这一点上也达成了一致，它们都坚定地支持这一方法。 这意味着，m d a 成长和繁荣所必需的主流工具和平台的支持已经指日可待了1 5 】。 虽然m d a 依然处于发展的“初级阶段”，但是已经展现出了极大改变软件开发状况的 潜力。今天，软件开发过程的焦点是编写代码。在未来，焦点从代码迁移到了模型，这对 软件开发过程、用来编写模型的语言以及软件开发工具都会有重大影响。人们将会定义新 的适合m d a 的建模语言。这些语言可以支持对系统的完整说明，既包含静态方面也包含 动态方面。这样的语言将扮演今天高级编程语言所扮演的角色。 在通信软件和协议工程领域，已经广泛使用形式化方法( f o r m a lm e t h o d ) 描述协议模型。 i t u t 和i s o 都发布了协议形式化描述语言的国际标准，如s d l ，e s t e l l e 和l o t o s 。 目前，协议工程正在从m d a 这一变革中吸取营养。m d a 在通信软件与协议工程中的 应用已经引起国际标准化组织、学术界和企业界的关注，许多研究计划正在开展，许多研 究小组正在工作。i t u t 开展了m d a 在电信领域中应用的研究工作。i t u t1 7 研究小组， 浙江理工大学硕士学位论文 问题1 7 1 7 正在研字r 统一建模语言l r m l 与i t u t 语言的结合，包括z 1 0 9 1 6 1 的修订工作”。 在i t u - t 的z 1 0 9 建议中定义了与s d l 一起使用u m l1 5 并映射到s d l 的方法。此外， 从s d l 语言到u m l1 5 的动作语义的映射【7 】已经定义。欧洲电信标准协会e t s i2 5 0 特别 工作小组s t f 正在研究“用于通信系统的u m lp r o f i l e ”。特别需要关注的是欧洲的联合研 究计划m o d a - t e l ，m o d a - t e l 已在m d a 应用于电信领域做了大量工作嗍。 所以，提出一种“基于m d a 的协议建模语言”，研究基于m d a 的协议建模技术， m d a 建模语言u m l 将成为平台独立模型( p l a t f o r mi n d e p e n d e n tm o d e l ，p i m ) 2 1 语言，而协 议形式化描述语言将成为平台相关模型( p l a t f o r ms p e c i f i cm o d e l ，p s m ) 2 语言，通过变换工 具和变换定义可以实现模型变换的自动化。模型不再是软件开发过程中的分析结果，而是 一个工件。建模语言也不再是设计语言，而是编程语言。这样，m d a 把软件开发的注意 焦点提到了更高的抽象层次，m d a 可以用来创建良好的设计，应付多样化的实现技术， 延长软件的生命期。 m d a 世界现在还未到来，许多问题还没有定论。但是，从计算机技术的发展历史来 看，模型驱动构架思想的出现是自然而合理的。m d a 带来的是一场变革，在这场变革面 前，我们需要有敢于开拓进取的勇气。从科学研究的发展趋势看，m d a 正在挑战上一代 软件开发方法的极限，并促进软件开发的下一个黄金时代的开创。本文的研究工作正是在 这个背景下进行的。 1 2 本文的主要工作 本文的工作主要包括下列一些内容： ( 1 ) 研究和探讨了目前协议工程学研究的热点：m d a 在电信领域中的应用。 ( 2 ) 在深入分析和理解u m l 状态图表示法和语义的基础上，对模型中表述对象动态行 为部分的内容以形式化语言抽象状态机( a b s t r a c ts t a t em a c h i n e s ，a s m s ) 唧作了精确的描述。 ( 3 ) 本文重点围绕着如何实现基于m d a 的协议建模技术进行了研究和探索。基于 u m l 的类图和状态图，利用u m lp r o f i l e 轻型扩展( l i g h t w e i g h te x t e n s i o n ) 机制【5 】，定义了 一种“基于m d a 的协议建模语言”交互抽象状态机描述语言( i n t e r a c t i v ea s m s d e s c r i p t i o nl a n g u a g e ，i a s m s d l ) 。设计了从p i m 模型到p s m 模型自动变换的全过程。文 中详细阐述了该变换过程中的变换步骤和变换规则。 2 浙江理工大学硕士学位论文 1 3 论文结构 论文共分七章。 第一章，介绍课题的研究背景、意义和内容。 第二章，介绍协议工程和基本的形式化模型( f o r m a lm o d e l ) ，研究形式化描述语言 ( f o n t a ld e s c r i p t i o nl a n g u a g e ，f d l ) 的三个国际标准。 第三章，介绍u m l 的发展历史和u m l 2 0 的主要特征，研究u m l 的结构建模和行为 建模技术。 第四章，分析u m l 在行为建模方面的不足，指出u m l 融合标准的协议形式化描述语 言是u m l 的发展趋势之一。 第五章，为弥补u m l 在行为建模方面的不足，基于交互抽象状态机i a s m s 定义了 u m l 状态图的行为语义。 第六章，研究基于m d a 的协议建模技术，定义了一种“基于m d a 的协议建模语言”， 设计了从p i m 模型到p s m 模型自动变换的全过程。 第七章，对本文创新点及相关工作的总结和对下一步工作的展望。 3 浙江理工大学硕士学位论文 2 1 协议工程 第二章协议工程及形式化模型 2 1 1 协议工程的发展历史 协议工程是2 0 世纪8 0 年代才发展起来的- - f l ! l l e 常活跃的新兴学科。它采用形式化的方 法描述在协议严格的设计和维护中的各个活动，是研究以协议为对象的软件工程。但所建 立的协议设计方法比现有软件工程的一般方法更严格，从而使协议开发的整个过程一体 化、系统化和形式化。 二十年前，美国学者w c l y n c h 在a c m 通信杂志上发表了题为“在半双工电话线上实 现可靠的全双工传输”的文章”0 1 ，首先提出了一个后被广泛引用的协议交换位协议 ( a 1 t e m a t i n gb i tp r o t o c o l ，简称a b 协议) 。他在该文最后提出一个猜想，认为这类协议至少 需要两位控制信息才能正确运转，希望能用形式化的方法来证明或否认他的猜想。 l y n c h 的文章引起了英国国家物理实验室k a b a n l e t t 等三人的注意。第二年，他们用有 限状态机( f i n i t es t a t em a c h i n e ，f s m ) 的方法验证了只用一位控制信息的a b 协议仍能正确 地运行，否定t l y n c h 的猜想。 尽管l y n c h 和b a m e t c 所讨论的协议是极其简单的，但却引起了人们对协议形式化描述 与验证的关注和研究，开始了研究协议形式化描述技术( 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 d t ) 的新纪元。在而后的三十年间，协议的形式化描述技术有了很大的发展。大致可以分为以 下四个阶段： ( 1 ) 研究各种形式化描述技术阶段( 1 9 6 8 - - 1 9 7 9 ) 这个阶段人们提出了各种描述协议的模型，主要有：有限状态机模型，p e t r i 网模型， 形式化语言模型，高级语言模型和混合模型等，在本章的下一节将具体介绍。在这一发展 阶段，上述各种形式化描述技术都得到了实际应用。 ( 2 ) 形式化描述技术的标准化阶段( 1 9 7 9 - - - 1 9 8 5 ) 人们在验证协议正确性的过程中发现协议实现中的错误主要是由于用自然语言描述 的协议文本自身就存在着二义性，要使标准协议是精确、无二义性的，必须对协议的描述 手段进行标准化。这项工作是由i s 0 仃c 9 7 s c 2 1 完成的，在8 0 年代先后定义了 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 nm o d e ll a n g u a g e ) u u 和l o t o s ( l a n g u a g eo f t e m p o r a l o r d e r i n gs p e c i f i c a t i o n ) b 2 1 两种形式化描述语言。 4 浙江理工大学硕士学位论文 此外，c c i t t q 3 9 v i i 研究组在8 0 年代也提出t s d l ( s p e e i f i e a t i o n a n d d e s e r i p t i o n l a n g u a g e ) “3 l 语言，这个语言与e s t e l l e 类似，基于扩展有限状态机( e x t e n d e d f i n i t es t a t e m a c h i n e ，e f s m ) 0 4 模型，主要用于开发程控软件，但也用作形式化描述语言。 ( 3 ) 协议工程阶段( 1 9 8 5 - - 1 9 9 5 ) 在这一阶段，人们开始研究基于i s o 或c c i t t 建议的形式化描述语言( s d l 、e s t e l l e 、 l o t o s 等) 的协议开发方法。美国学者t e p i a t k o w s k i 在1 9 8 3 年首先提出了“协议工程” 的概念，h r u d i n z a i 在1 9 8 5 年详细阐述了基于形式化描述技术的协议工程的各个阶段中的 主要任务。i s o 的e s t e l l e 和l 0 1 o s 于1 9 8 8 年9 月形成最后的正式版本，协议工程已由研 究阶段转到正式实现的阶段。 进入8 0 年代后，世界的一些著名研究所与公司已经开发了基于各种形式化描述技术的 协议开发系统。这些协议开发系统的共同特点是它们使用的描述技术是自己定义的，不是 标准化组织建议的，但它们和i s o 的e s t e l l e 语言很类似。这些系统为研制基于i s o 的形式 化描述技术的协议开发系统提供了宝贵的经验与方法【1 6 】。 ( 4 ) 形式化描述技术的发展和成熟阶段( 1 9 9 5 - - ) 在( 3 ) 阶段，实践中人们发现现有的形式化描述技术并不能很好地满足用协议工程的方 法来实现协议，协议开发人员往往需要根据实际应用领域对形式化描述技术进行扩展才能 满足实际需求，协议工程的发展比较缓慢。因此，人们一方面又重新对原有的形式化描述 技术进行了分析和研究，参考了其它软件工程中的概念和方法，如s d l 9 8 就加入了面向对 象的思想，以使形式化描述技术具有更广泛的应用领域，更明确的定义和更清晰简洁的描 述；另一方面也对不少有前途的形式化描述技术进行了研究。人们已经认识到用单一的一 种形式化描述技术是很难满足协议工程整个过程的，因此不同形式化描述技术的融合、相 互协作是一个主要研究方向。 2 1 2 协议工程的国内外研究现状 目前，国内外对协议工程的研究主要集中在协议形式化建模、协议规格的形式化描述、 协议性能分析、协议设计自动实现和协议测试，也有少数在研究协议验证。8 0 年代初，欧 洲的一些研究机构开始研究协议一致性测试，i s o 于1 9 9 1 年推出i s 0 9 6 4 6 标准，它的诞生 是协议一致性测试领域的重要里程碑1 7 1s ，1 9 。在电信协议的一致性测试领域，已经有人做 了许多的研究和工作1 2 0 , 2 1 捌。现在英国国家物理实验室、法国国家通信研究中心、德国国 家通信研究局、美国国家标准化研究局和美国新罕布什尔大学互操作研究实验室等都在这 浙江理工大学硕士学位论文 个领域投入了大量的研究力量。2 0 0 3 年在法国召开的t e s t c o m2 0 0 3 大会的主题是。下一 代网络的测试技术”，e t s i 于该年发布新一代测试集描述语言t t c n - 3 修订版标准r 3 】。 国内对协议工程的研究起步较晚，开始于8 0 年代末。国内有关形式化描述与测试集自 动生成方面的主要研究成果有：南京通信工程学院最先研究了e s t e l l e 语言并实现了 e s t e l l e 语言的半自动生成系统幽。北京邮电大学承担了s d l 语言的语义研究和制定工作 【2 5 捌。清华大学提出一种基于有限状态机的外部行为描述的形式化模型，在此基础上开发 了测试集自动生成工具t u g e n e 2 7 1 ，后来又提出一种综合数据流和控制流的协议测试集生 成方法，改进了t u g e n 的性能【2 射。协议验证方面内蒙古大学利用消息序列图( m e s s a g e s e q u e n c ec h a r t s 。m s c ) 采用模型检查技术，对i p v 6 的邻居发现协议的属性进行了形式化验 证刚。 2 1 3 协议工程系统 协议工程包括协议生命期周期内的所有范围，主要设计和开发活动如下： 分布计算资源用户要求； 高级体系结构设计，即建立一个协议集提供的服务分层结构； 提供分层结构中的各级服务描述，一般由两部分组成：独立于实现的描述，适用于 国际标准；逐步求精的实现描述，与环境条件有关； 目标实现。 协议工程主要结合综合和分析的方法来研究和实现协议工程的各个活动。综合方法包 括协议综合( p r o t o c o l a n a l y s i s ) 和协议自动实现( p r o t o c o l a u t o m a t i c i m p l e m e n t a t i o n ) 。 协议综合是由相应服务描述产生协议描述( p r o t o c o ls p e c i f i c a t i o n ) 的规范。协议描述定 义了各层的通信实体之间相互通信的消息格式、交换消息的顺序和各通信实体的功能，并 建立文档。协议自动实现是由协议描述到某个实现的自动转换。分析方法包括协议验证 ( p r o t o c o lv a l i d a t i o n ) 和一致性测试( p r o t o c o lc o n f o r m a n c et e s t i n g ) 。协议验证与协议综合互 补，它证明协议描述是否满足服务描述中的要求；一致性测试与自动实现互补，它测试实 现与独立于实现的描述是否一致。 协议工程还包括协议性能分析( p r o t o c o lp e r f o r m a n c ea n a l y s i s ) 、协议转换( p r o t o c o l t r a n s i t i o n ) 和协议维护( p r o t o c o lm a i n t e n a n c e ) 。性能分析通过分析协议描述，确定吞吐量、 时延、可靠性和有效性等性质。当两个不兼容的协议体系结构系统通信时，需要协议转换， 即将两个体系结构相互转换。协议维护涉及到纠正实现中的错误，更新协议文本，甚至提 6 浙江理工大学硕士学位论文 出全新的协议，协议维护需要对以上系列协议工程活动作一致性的修改。 一个典型的协议工程系统如图2 1 所示。 2 2 基本的形式化模型 图2 0 1 协议工程系统 形式化方法( 形式化模型) 的基本含义是借助数学的方法来研究计算机科学中的有关问 题。( e n c y c l o p e x i i ao fs o i t w a r ee n g i n e e r i n g ) 对形式化方法定义为：“用于开发计算机系统 的形式化方法是基于数学的用于描述系统性质的技术。这样的形式化方法提供了一个框 架，人们可以在框架中以系统的方式刻画、开发和验证系统” 3 0 1 。换言之，在软件开发的 全过程中，凡是采用严格的数学语言，具有精确的数学语义的方法，都称为形式化方法。 从广义角度，形式化方法是软件开发过程中分析、设计及实现的系统工程方法。从狭义角 度，形式化方法是软件规格和验证的方法。 软件的形式化开发方法，最早可追溯到2 0 世纪5 0 年代后期对程序设计语言编译技术 的研究，当时b a c k u s 提出了巴科斯范式( b a c k u sn o r m a lf o r m u l a , b n f ) 作为描述程序设计语 言语法的元语言。在2 0 世纪6 0 年代，面对当时出现的软件危机，f l o y d 、h o a r e 和m a n n a 等开展的程序正确性证明研究推动了形式化方法的发展。他们试图用数学方法来证明程序 的正确性并发展成为了各种程序验证方法，但是受程序规模的限制，这些方法并未达到预 期的应用效果。2 0 世纪8 0 年代，在硬件设计领域形式化方法的工业应用结果，掀起了软 件形式化方法的学术研究和工业应用的热潮。p n u e l i 提出了反应式系统规格和验证的时态 逻辑( t e m p o r a ll o g i c ，t l ) 方法，c l a r k e 和e m e r s o n 提出了有穷状态并发系统的模型检验方 ， 浙江理工大学硕士学位论文 法。近十年来，形式化方法的研究及其在工业中的应用得到了长足的发展。研究人员建立 了系统设计人员易于理解的规格概念和术语，以及有效应用这些概念和术语的形式化规格 方法及语言，建立了功能更加强大和完善的模型检验和定理证明技术，并开发出了与之相 应的从研究原型到商品化产品的支撑工具和环境。 且前，已建立了多种适用于软件系统规格的形式化方法。从形式化规格到目标软件系 统的可实现和可执行角度，已建立的形式化方法可分为三类：操作类、描述类和双重类。 ( 1 ) 操作类方法基于状态和转移，通过可执行模型来描述系统，模型本身能够采用 静态分析和模型执行而得到验证。这类方法包括有限状态机、扩展有限状态机、p e t r i 网及 高级p e t r i 网等。 ( 2 ) 描述类方法基于数学公理和概念，通过逻辑或代数给出系统的状态空间，具有 高度抽象的特点，便于通过自动工具进行验证。基于不同的数学基础，描述类方法迸一步 分为：基于代数的描述类方法，如通信系统演算( c a l c u l u so f c o m m u n i c a t i o ns y s t e m s ，c c s ) 、 通信顺序进程( c o m m u n i c a t i o ns e q u e 嘣a lp r o c e s s e s ，c s p ) 、z 方法、维也纳开发方法( v i e n n a d e v e l o p m e n tm e t h o d , v d m ) 和l a r c h 方法等；以一阶线性对态逻辑( f i r s t - o