（通信与信息系统专业论文）通信协议形式化描述和验证理论与方法的研究.pdf

中罔辩技人学颂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 网验证方法相比，具有自己的优点。 本文在用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 网的展开图方法在验证p e t r i 网行为属性方面的应用；使用p e t r i 网模 型对两种典型的通信协议( t f t p 协议和b g p 协议) 进行形式化描述；在 此基础上，使用p e t r i 网展开图方法对两个协议的行为属性进行了分析，并 且通过对植入错误的协议描述的分析证明了展开图法具有一定的纠错能 力。 关键字：协议工程，形式化描述方法，协议验证，p e t r i 网，展开图法 t f t p 协议，b g p 协议 中周科技夫学碰l 学位论文 摘业 r e s e a c ho n t h e o r y a n dm e t h o d so ft h e f o r m a l d e s c r i p t i o n a n dv e r i f i c a t i o no f c o m m u n i c a t i o np r o t o c o l s a b s t r a c t p r o t o c o li st h ek e r n e lo fn e t w o r ka n dc o m m u n i c a t i o ns y s t e m f o ra s s u r i n g t h eq u a l i t yo fc o m m u n i c a t i n ga n dt h es e c u r i t yo fi n f o r m a t i o nt r a n s f e r r i n g ，i ti s n o t o n l yt h e o r e t i c a l l ym e a n i n g b u ta l s o p r a c t i c a l l y u s e f u lt o i n v e s t i g a t e t h e p r o t o c o lf o r m a l i z a t i o nt h e o r y p r o t o c o lf o r m a l i z a t i o nt h e o r yi sm o s ti m p o r t a n to ft h ep r o t o c o le n g i n e e r i n g a p p l y i n g t h ef o r m a l d e s c r i p t i o nt e c h n i q u e s i np r o t o c o l e n g i n e e r i n g ，t h e r e s e a r c h e so np r o t o c o le n g i n e e r i n gi n c l u d es e v e r a lt h e o r i e sa n dm e t h o d s ，s u c ha s p r o t o c o ld e s c r i p t i o n ，p r o t o c o lv e r i f i c a t i o n ，p r o t o c o lt e s t i n g a n d p r o t o c o l i m p l e m e n t a t i o n p r o t o c o lf o r m a ld e s c r i p t i o n s a r et h em o s t i m p o r t a n ts t e p o f p r o t o c o l e n g i n e e r i n g p r o t o c o l v e r i f i c a t i o na s s u r e st h ec o r r e c t n e s sa n d c o m p l e t i o no fp r o t o c 0 1 p r o t o c o lt e s t i n g i sa ni m p o r t a n tm e t h o dt oc h e c kt h e p r o t o c o li m p l e m e n t a t i o n s a t i s f i e dw i t ht h ep r o t o c o lf o r m a ls p e c i f i c a t i o n p e t r in e ti sa no u t s t a n d i n gg r a p h i c a lf o r m a lm o d e l ，w i t hi t si n t u i t i o na n d b e i n ge a s yt ou n d e r s t a n da n d u s e i t sf i tt od e s c r i b et h eb e h a v i o r a lp r o p e r t i e so f c o n c u r r e n ta n dd i s t r i b u t i n gs y s t e m s w ec a no b t a i nt h ei n f o r m a t i o no fs y s t e m b e h a v i o r su s i n gt h ev e r i f i c a t i o nt e c h n i q u e so fp e t r in e to no b j e c ts y s t e m s u n f o l d i n go f p e t r in e t si sas p e c i a lm e t h o dt oe x p l o r et h es t a t es p a c eo f c o n c u r r e n ts y s t e m s ，w h i c he x c l u d e st h ep o s s i b l ei n t e r s e c t i o no fc o n c u r r e n t e v e n t ss oa st og r e a t l yr e d u c et h ec o m p l e x i t yd e g r e eo fs p a c ea n dt i m ef r o m s t a t e s p a c ee x p l o s i o n c o n t r a s tt o t h et r a d i t i o n a l a n a l y z i n gm e t h o do fp e t r i 2 中国科技人学顿 一学位论文摘要 n e t s ，t h eu n f o l d i n gm e t h o dh a ss o m em e r i t s i nt h i s p a p e r ，w ew i l i a n a l y z es o m ec o m m u n i c a t i o np r o t o c o l s w i t ht h e v e r i f i c a t i o nm e t h o do fp e t r in e tu n f o l d i n gb a s e do nt h ef o r m a ld e s c r i p t i o no f t h e mu s i n gp e t r in e t t h em a i nw o r ki n c l u d e ：s u m m a r i z i n gt h em o s tc o m m o n f o r m a ld e s c r i p t i o nl a n g u a g e sa n dm o d e l s ；a n a l y z i n gt h ea b i l i t yo ft h ep e t r in e t o l 、d e s c r i b i n g c o m m u n i c a t i o n p r o t o c o l s ；i n t r o d u c i n g t h em o s tc o l n m o n v e r i f i c a t i o nm e t h o d s ；a n a l y z i n gt h ev e r i f i c a t i o na b i l i t yo fp e t r in e t s ；s p e c i a l l y a n a l y z i n gt h eu n f o l d i n gm e t h o d o fp e t r in e tv e r i f i c a t i o n ；m o d e l i n gt w o t y p i c a l c o m m u n i c a t i o np r o t o c 0 1 t f t pa n db o p , u s i n gp e t r in e t ；a n a l y z i n gt h e i r a c t i o n p r o p e r t i e su s i n g p e t r in e tu n f o l d i n g m e t h o d ；p r o v i n g t h ec o r r e c t i n g a b i l i t yo ft h ep e t r i n e tu n f o l d i n gm e t h o db ye m b e d d i n gs o m ee r r o r si nt h e d e s c r i p t i o no f t h ep r o t o c o l s k e yw o r d s ：p r o t o c o l e n g i n e e r i n g ，f o r m a ld e s c r i p t i o nt e c h n i q u e p r o t o c o lv e r i f i c a t i o n ，p e t r in e t s ，u n f o l d i n g ，t f t p , b g p 2 中国科技火学颂上学位论文 第一帚结论 1 1 研究背景 第一章绪论 通信协议是计算机网络和通信网络中各种通信实体间交换信息所必须 遵守的一组规则，它规定了信息交换的格式、内容和过程。 通信协议的定义如下；在计算机网络中，为了使计算机或终端之间能 够正确地传递信息，必须有整套关于信息传输顺序、信息格式和信息内 容等的约定，这一整套约定称为通信协议。 不同的协议通常描述某一通信的不同方面，它们集合在一起组成一个 “协议栈”。“协议”和“协议栈”也常用来指实现一个协议的软件。现在的大 多数i n t e r n e t 通信协议由i e t f 规定，其他的则主要由i e e e 或者i s o 组织 规定。i t u t 负责制定电信协议和规程。在电信网和i n t e r n e t 融合的大背 景下，两套标准也趋向融合。 早期的数据通信只局限于一些企业和团体内部，通信设备类型单一， 网络拓扑结构简单，各团体设计和实现自己专用的协议。为了适应更大范 围的数据通信和不同的网络之间的互连和互操作，给网络硬件、软件、协 议、存取控制和拓扑提供标准，2 9 8 4 年国际标准化组织i s o 提出了开放系 统互联i s o o s i 参考模型【1 】。而另一方面，以t c p i p 协议为核心的i n t e m e t 网络体系结构拥有更广泛的用户，成为了事实上的计算机网络工业标准。 计算机或终端之间的通信采用分层结构，比如，国际标准化组织( i s o ) 定义的开放系统互连参考模型( o s r m ) 在功能上把计算机网络划分成七 层，即物理层( 最底层) 、数据链路层、网络层、传输层、会话层、表示层 和应用层。通信只能发生在对等层之间，而各层采用的通信协议是各不相 同的，即使是在同一层，不同的功能要求也可能采用不同的通信协议。如 目前应用很广的t c p i p 协议栈( 协议族) 共分四层，即数据链路层、网络 层、传输层和应用层。每层包含的通信协议各不相同，比如：网络层包括 i p ( 网际协议) 、i g m p ( 网际组管理协议) 、i c m p ( 网际控制报文协议) 等：传输层包括t c p ( 传输控制协议) 、u d p ( 用户数据报协议) 等；应 中囝科技人学坝j j 学位论文 第章绪论 用层包括t e l n e t ( 远程通信网络协议) 、f t p ( 文件传输协议) 、s m t p ( 简单邮件传送协议) 、d n s ( 域名系统) 、s n m p ( 简单网络管理协议) 、 d k l c p ( 动态主机配置协议) 等。 随着计算机通信和网络技术的不断提高，i n t e r n e t 迅速普及，嘲络规模 不断扩大，到2 0 0 5 年初，仅中国内地联网计算机主机总数就达到2 0 8 3 万 台，上网人数达到5 9 1 0 万2 1 。由此带来的通信网络的复杂性与日俱增。 现在，已经形成了以i n t e r n e t 为核心的计算机网络和p s t n 、g s m c d m a 为代表的通信网络。通信网络系统的复杂性在协议方面体现出空间分布性、 并发性、异步性、不稳定性和多样性。这不仅意味着协议开发难度大，周 期长，而且潜在错误多，协议开发过程中任何一点错误和缺陷都将给通信 系统的稳定性、可靠性、坚固性、安全性、容错性以及系统之间互通性和 互操作性带来巨大的危害。因此，需要合适的方法、技术和计算机辅助工 具，使开发过程工程化，以便提高协议的开发效率，促进标准化的协议实 现，因此产生了协议工程( p r o t o c o le n g i n e e r i n g ) 学科 3 】。 协议开发过程就是开发协议的过程。开发协议有两种含义，一是为了 满足新的通信需求，研究开发新的协议，制定协议标准；另一个则是在一 个特定应用环境下，实现某个已经成熟的协议。所谓成熟的协议是指已经 成为标准文本的协议，如t c p i p 协议等；也可以是即将成为标准文本的协 议，如3 0 p p 制定的一系列关于第三代移动通信的协议文本等。 对于第一种含义( 开发新的协议) ，开发协议的目标是形成新的协议文 本，重点是说明本协议应该具有什么功能。其协议开发过程包括： 1 ) 协议环境分析，包括用户要求、通道性质、工作模式等。 2 ) 协议功能设计，根据环境分析结果明确本协议应具有的功能。 3 1 协议元素设计，设计服务原语、p d u 格式等。 4 ) 形成协议文本，用自然语言描述协议结构及协议元素之间的关系。 5 1 协议描述，用一种形式化语言来描述协议内容，包括建议的软件系 统结构、模块划分、系统应具有的行为等。 6 1 协议验证，在开发环境下仿真运行协议软件，验证协议的豇三确性。 对于第二种含义( 实现具体协议) ，开发协议的目标是生成一个软件系 统，该软件系统可以实现具体协议的全部功能或一个功能子集，重点是说 明如何实现协议功能。其协议开发过程包括： 1 ) 协议分析，包括协议环境分析和协议功能分析a 中国搴 技大学颤卜学位论文 第一章绪论 2 ) 协议设汁，包括协议机制设计、协议元素设计及协议组织没计。 3 ) 仂一议拙述，用一种形式化语言来描述设计结果，包括软件系统结构、 模块划分、系统行为实现细节等。 4 ) 协议验证，在开发环境下仿真运行协议软件，验证协议的正确性。 5 ) 协议实现，用某利，编程语言实现协议软件系统( 自动生成代码或手 工编码) 。 6 ) 协议测试，在目标环境下测试协议软件系统。 7 ) 协议维护，在协议软件的使用过程中不断完善系统。 实现具体协议的过程基本上涵盖了开发新的协议的过程，只是两个过 程的出发点和侧重点是不同的。从应用角度来看，实现具体协议的需求大 于开发新的协议的需求，所以本文将重点介绍实现具体协议的过程。在后 续章节中，除非特别说明，“开发协议”均指实现具体协议。 协议工程，是指一体化和形式化的协议开发过程。它的宗旨是为协议 软件的研制和开发提供一整套工程规范。一体化即系统化，其含义是：协 议的设计、验证、实现和测试，在技术上前后镦接，并在同一个开发系统 中完成。而形式化即“模型化”和“抽象化”，是指将协议以及由协议提供的 服务用形式化描述方法( f o r m a l d e s c r i p t i o n t e c h n i q u e s ：f d t ) 描述出来。 开发过程工程化，以便提高协议的开发效率，促进标准化的协议实现，一 体化和形式化都是为更规范进行协议实现工程化服务的。 所谓用工程的方法，就是在开发协议的各个阶段均采用工具，而且这 些工具在技术上前后衔接。被集成在同一个开发环境中。也就是说，协议 的开发可以在同一个开发环境中完成。 在协议工程的不同阶段，协议可以有不同的表示形式，这些表示形式 代表了不同开发阶段的结果。协议的表示形式有： 非形式描述文本( i n f o r m a ls p e c i f i c a t i o n ) ：用自然语言和图表表述的 协议，易读易懂，但不严密，有多义性。非形式描述文本是协议分析和协 议设计完成后的结果。 形式描述文本( f o r m a ls p e c i f i c a t i o n ) ：用f d l 描述的协议，严密，无 二义性，可符号执行，可转换成程序设计语言程序。形式描述文本是协议 描述完成后的结果。对于已经用形式化语言描述的协议文本，在具体机器 上实现时，仍需要经过协议分析和协议设计阶段，并且需要重新用形式他 语言对其进行描述。这是因为，标准化的协议文本重点描述的是协议应该 中国科技人学顿。学位论殳第一章绪论 具有的功能，而在实现协议时，重点拙述的是协议实际具有的功能。特别 是在只需要实现协议的一个功能子集时，更需要对协议进行重新描述。 与机器无关的源程序代码( m a c h i n e i n d e p e n d e n ts o u r c ec o d e ) ：这是 由形式描述文本翻译过来的程序设计语言( p a s c a l ，c 等) 程序。协议本身 有一定抽象性，即协议没有指明这个协议在某个机器上怎样实现，正因为 协议本身是抽象的。它刊适合用f d l 来描述。这样，形式描述文本翻译后 的程序设计语言程序就是与机器无关的代码了。 实现代码( i m p l e m e n t a t i o nc o d e ) ：这是协议实现后的最终代码一般 与机器无关的源程序代码只占最终实现代码的一部份。协议在一种机器上 的实现还包括大量协议文本没有描述的程序，例如缓冲器分配管理，系统 输入输出操作等，这部份程序称作与机器相关代码。 协议工程中采用的工具就是用来描述协议文本，并实现不同表示形式 的文本之间的自动转换。 形式化描述方法是协议工程核心部分，关联了协议工程中的各个过程。 目前适用于协议工程的形式化描述方法种类繁多，各具特色，但也各有不 足。使用什么样形式化描述方法进行协议设计、验证，乃至后续的协议测 试，是协议工程领域中的一个重要的核心问题。 协议验证( p r o t o c o lv e r i f i c a t i o n ) 是协议工程的重要组成部分，是对通 信协议本身的逻辑性和正确性进行验证的过程。它处于协议工程中协议设 计阶段之后，协议实现阶段之前。其工作过程一般是通过选择合适的形式 化描述方法对协议进行形式化描述，然后用基于数学的方法，检验或证明 协议设计的逻辑正确性。 1 2 研究现状 1 2 1 形式描述技术 利用形式化技术对模型进行描述以及验证理论的研究将直接影响到 计算机通信协议开发技术的进步和发展。所以很多国家都投入了大量的人 力物力从事这方面的研究1 - 干1 9 。例如：英国的国家物理局n p l 、法国国家 通信研究中心、德国国家通信研究局g m d 、美国国家标准化研究局、美 中国科技大学硼卜学位论文 第一章绪硷 国新罕布什尔大学互操作研究实验室都在这个领域投入了大量的研究力 量。 形式化描述方法是指在描述、设计和构建计算机系统和软件的过程中 所使用的基于形式逻辑和离散数学的方法和技术。它具备以下重要的特性 【4 ： 数学模型： 它是否可以表达“做什么”而不需要说“怎样做”； 形式化的语法； 它是否可以方便的应用有效的工具来进行自动化分析； 形式化描述方法在协议开发中起到的作用是多方面的。协议规范的描 述是协议开发的基础。一般非形式化的描述可能导致描述的不明确和不一 致。如果描述的不明确和不一致导致协议设计，协议实现出现错误，将来 的修改、维护所要付出的代价就非常大。如果导致的错误没有被发现，则 会影响协议的可靠和使用。形式化描述方法则要求描述的明确性，而描述 的不一致性也就相对易于发现。 目前的形戴化描述方法大都是采用以下几种形式化模型以及基于这 些模型的形式化描述语言： 1 有限状态机f s m 和扩展有限状态机e f s m 模型【5 】【6 】 2 p e t r i 网模型 7 1 1 8 】 3 消息序列图m s c 模型 9 】 4 通讯进程演算c c s 1 0 1l 】和通讯顺序进程c s p 模型 1 2 1 1 1 3 】 5 时序逻辑t l 模型 1 4 1 6 构造类别代数模型 1 5 】 7 基于扩展有限状态机模型( e f s m ) 的s d l 语言f 1 6 】和e s t e l l e 语言 【1 7 】 8 基于经典集合论和前序逻辑( f i r s to r d e rl o g i c ) 的z 语言【1 8 】 9 基于进程代数和多类代数的l o t o s 1 9 1 0 基于进程代数( p r o c e s sa l g e b r a s ) 的r s l 语言 2 0 】 1 1 基于抽象文字表示法的a s n 1 【2 1 】 1 2 基于谓词逻辑描述状态以及状态变迁的关系语言 2 2 】 1 3 ，描述协议一致性测试用例的t t c n 语言 2 3 】 有限状态机( f i n i t es t a t em a c h i n e ：f s m ) 使最常用的协议形式化描述 中幽科拉大学顿1 学位论文 第审绪论 技术。有限状态机通常使用状态转移图( s t a t et r a n s i t i o ng r a p h ：s t g ) 沫 表示。状态转移图是一个有向图，它的顶点代表状态，而它的有向边代表 状态转移。它的每一条有向边都标记了输入和输出。还有些对有限状态 机的扩充，如通信有限状态机( c o m m u n i c a t i o nf i n i t es t a t em a c h i n e ：c f s m ) 2 4 和扩展的有限状态机( e x t e n d e d f i n i t es t a t em a c h i n e ：e f s m ) f 5 1 等等。 p e t r i 网( p e t r in e t ：p n ) 在通信领域得到了广泛的应用。p e t r i 网可以 清楚的表达两个进程之间的通信，它也可以用作其它形式化描述方法的辅 助方法。通过增加一些特殊模型，p e t r i 网也有多种扩展，包括数字p e t r i 网( n u m e r i c a lp e t r in e t ：n p n ) 2 5 1 、有色p e t r i 网( c o l o u r e dp e t f in e t ： c p n ) 【2 6 】 2 7 和时间p e t r i 网( t i m e p e t r in e t ：t p n ) 【2 8 】等等。 s d l ( s p e c i f i c a t i o n a n d d e s c r i p t i o nl a n g u a g e ) 语言是由c c i t t ( i t u t ) 组织开发的电信领域的国际标准。它的数学模型是扩展有限状态机模型 ( e f s m ) ，它可以精确描述一个系统的动作特征。 l o t o s ( l a n g u a g eo f t e m p o r a lo r e d e r i n gs p e c i f i c a t i o n ) 是由i s o 组织 开发出来的语言。l o t 0 8 的基本思想是：一个通信系统可以描述成为一系 列有时间顺序的可以由外部观察到的事件。l o t o s 是用通信系统验算 ( c a l c u l u so f c o m m u n i c a t i o n s y s t e m ：c c s ) 来描述进程的行为和交互，并 且使用a c to n e 语言来描述数据结构和表达式。a c to n e 是一个抽象数 据类型语言，它的数学模型是代数规范。l o t o s 语言存在一些扩展，如 d l o t o s 2 9 1 ，g - l o t o s 3 0 等等。 e s t e l l e 也是由i s o 组织开发的一种语言，它也是基于扩展有限状态机 模型( e f s m ) 的。e s t e l l e 语言使用p a s c a l 作为基础，并且将之扩展以描 述系统的细节、进程的并发和进程间的通信。它通常被用作描述分布式系 统和并行信息处理系统。 z 语言中的z 是指著名的数学家z e r m o l o 。z 语言以经典集合论和前序 逻辑( f i r s to r d e rl o g i c ) 为基础，提供了种称为框架( s c h e m a ) 的结构，以此 来描述规范的状态空间和操作。z 规范说明由一系列框架组成。每个框架 定义一个抽象对象或操作，并用谓词判定描述给出的新的对象或操作的语 义约束。z 框架说明可以组台成新的z 框架。新的z 框架继承其成分框架 的一切属性和约束。这样，系统的z 框架规范说明可以按一定的层次结构 结出。框架的使用为规范说明提供了种演算( c a l c u l u s ) ，通过这种演算， 无论多么大型系统的规格说明都对以通过一个个小的部分来构成。目前关 中陶科技人学颂上学位论义 第一章结论 于z 语言的扩展有z 十+ 语言【3 1 ，o b j e c t z 1 3 2 1 语言等等。 然而，在实际的通信1 办议的设计、丌发中，选择哪一种形式化描述方 法彳是最适当的昵? 每一种形式化描述方法都有它的优点，对描述某些特 定类型的系统可能比其它的形式化描述方法更加合适。 这些形式化捅述方法大致可以划分为两类： 面向属性的是通过系统的属性来间接的描述系统。 面向模型是通过对系统建模来直接描述系统。 面向状态的描述系统的状态以及与之相关的变迁。 面向变迁的无须参考具体的状态，而直接描述变迁。 对形式化描述化方法的分类是很难的，有的形式化描述方法可能同时 属于多个类别，这主要依赖于该形式化描述方法在实际工程中如何运用。 但总的来说，上述划分有助于比较个形式化描述方法的异同。 没有哪一种形式化描述方法适合描述和分析复杂通信协议系统的所有 方面。大多数形式化描述方法都是基于单一的形式化描述语言的，它们只 适合描述系统的某些方面，如控制流、数据、结构、行为等等；或只适合 描述某种类型的系统，如顺序、并发、分布、实时等等。在实际应用中， 往往需要使用多种形式化描述方法对系统的不同侧面进行描述和分析。 1 2 2 协议验证技术 协议验证的主要目的是试图在协议开发的前期最大限度地检测和纠正 协议错误和缺陷，包括死锁( d e a d l o c k ) 、活锁( 1 i v e t o c k ) 、不可执行地行 动、协议外部性能不符合服务要求等。协议验证技术多种多样，但主要可 以分为三类： 可达性分析( r e a c h a b i l i t ya n a l y s i s ) 逻辑证明( l o g i cp r o o f ) 模拟( s i m u l a t i o n ) 。 另外，协议综合将协议设计和协议验证紧密结合起来，也可以认为是 一类验证技术。 可达性分析是最常用的技术，是一种传统的、易于自动化处理的、有 效的协议验证方法。但可达性分析需要从初始状态开始，枚举协议中的所 有可达状态，随着通信协议的复杂性的不断增加，它所面临的状态爆炸问 中网科技人学硕i _ 学位论文 第一章鲔讫 题( s t a t ee x p l o s i o np r o b l e m ) 也随之变得越来越突出。 逻辑证明用推理验算的方法严密地证明各种1 办议性质，所采用的技术 要来自于时态逻辑、谓词逻辑、代数验算等数学领域。 模拟是有选择地对某些可执行地分支进行验证。它是前2 种方法地一 个补充，尽管它不可能包容所有的可能性。但它能更精确地反映系统的行 为，提供理论分手厅所无法得出的结果。 协议综合是由相应的服务描述产生协议描述的规范。它的目的是寻求 一组能确保所产生协议功能齐备，没有逻辑错误的规则，根据协议的服务 规范生成一个目标协议。这组规则： ( 1 ) 使用形式化方法，其过程严密； ( 2 ) 协议构造过程和验证过程融为一体； ( 3 ) 使用工具软件， 可以产生出规模小，但更有效的，更容易维护和修改的协议。它要求： ( 1 ) 实现已给定的服务规范； ( 2 ) 使用一种不会产生错误的方法生成协议。 在协议工程中协议验证和协议综合互补，但这个领域至今取得的进展 很小。 1 3 研究目的 现有的形式化描述模型和描述语言有很多，对于通信协议工程的具体 要求，选择什么样的形式化描述技术对通信协议进行形式化描述是一个至 关重要的问题。我们将分析和比较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 网进行简化，从而部分解决状态空间爆炸问题。但是这种方法 的缺陷在于，变换后得到的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 网的展开图分析法 中周科技人学彤10 学位论文 第一帝绱论 最初的提出是针对异步电路的死锁检测，由于它具有通用性，可以被推广 到通信协议的属性分析。对于通信协议所具有的重要属性，如活性，安全 性等，我们都可以用p e t r i 网展丌图来分析，这给验汪通信协议提出了一个 新的思路，即用图形化的而不是矩阵方程的方法解决非常困难的和抽象的 p e t r i 网验证问题，这种方法的好处在于具有直观性，易懂易用。 1 4 研究方案 本论文的主要内容是针对通信协议的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 网验证方法，找出它们的不足； 研究和分析基于p e t f i 网展开图的协议验证技术的特点： 采用j 基于p e t r i 网展开图的协议形式化验证技术，对_ r 些实际的通 信协议进行形式化描述，以检验它的验证能力： 通过在通信协议的形式化描述中人为植入错误，检验展开图法的 纠错能力。 1 5 论文安排 本文的组织结构如下所示： 第一章绪论 介绍我们从事的研究工作的背景、意义和目的，所采用的研究方案以 及本文的组织结构。 第二章形式化描述技术 通过对非形式化方法与形式化方法的比较，阐述了形式化描述的必要 性：然后介绍了目前几种常用的模型技术以及形式描述语言f d l ，并对它 们各自的特点进行了分析和比较。介绍了p e t r i 网的基本概念并研究了 p e t r i 网对通信协议的强大描述能力，并由此提出使用p e t r i 网对通信协 议进行形式化描述。 中同科控入学颂j 学位论文 第一章绪论 第三章形式化验证技术 阐述了协议验证的目的和协议验证方法的分类，然后介绍了协议验证 特别是协议分析的般方法。 第四章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 网展开图法在通信协议形式化验证方面的应用实例 首先使用p e t r i 网对两种典型的通信协议t f t p 和b g p 进行了形式化 描述，然后用展开图法对它们的行为属性，包括活性、有界性和可逆性， 进行了分析。通过在它们的p e t r i 网形式化描述中植入错误证明了展开图法 对协议行为属性的验证能力。 第六章总结和展望 对以上工作进行了总结，并且提出了一些需要进一步研究的问题。 0 中国科技人学埘【：学位论立 第一二章形式化描述投术 第二章形式化描述技术 形式化方法是一种采用形式化语占来描述( 计算机) 系统的方式 3 3 1 。形式 化语言基于一定的数学理论，由符号集和操作、组合符号的规则集组成。它具有 形式化的语法和语义结构。形式化语言可以分为两大类： ( 1 ) 非解析性的：只可根据系统的可观察行为来描述系统的黑盒特性。 ( 2 ) 解析性的；可以建立系统的数学模型。 形式化方法在计算机科学领域的研究已经有6 0 多年，7 0 年代开始在协议规 范领域掀起了研究热潮。 2 1 形式化描述的必要性 为了说明方便，几乎所有的协议规范都是采用自然语言来描述，有时考虑到 直观性，还会借助于图表。但采用非形式化( 自然语言) 和半形式化( 图表) 方 法描述协议均存在不精确、有歧义及不易验证等缺陷，而采用形式化描述技术 f d t ( f o r m a l d e s c r i p t i o nt e c h n i q u e ) 则能较好地克服上述不足，充分表述协议 的各种特性和体系结构，为协议的验证、实现及一致性测试提供良好的基础。 采用形式化描述技术来描述协议有以下好处【3 4 】： ( 1 ) 使用形式化技术所描述的协议规范是精确的； ( 2 ) 可以通过严格的分析来确定给定规范的完整性和致性； ( 3 ) 可以编写一个合适的编译器处理形式化规范来生成一个协议的部分协 议实现； ( 4 ) 协议的形式化规范可以作为自动验证和自动一致性测试的基础； ( 5 ) 协议的形式化描述可以作为一个协议的形式化文档； ( 6 ) 协议设计者可以使用形式化描述技术来描述协议，这样就可以和协议 实现者建立一个精确的联系； 一般来说，协议的形式化特性应该包含以下五个方面的内容： ( 1 ) 活动性0 i v e n e s s ) ：协议的活动性是指协议运行时一些正确的情况会发 中田科披人学坝l 学位沦文 第一章 形式化描述拙术 生。这些情况包括：预定的事件会产生，指定的协议状态会到达，麻 该进行的协议行动会进行等。协议的活动性体现在终i l 性和进展性两 个方面，或者说，如果协议有终止性和进展性，它就具有活动性。终 止性是指协议从任何一个状念开始运行，总能f 确地达到终止状态； 进是展性指协议从初始状态运行，总能正确地达到指定状态，如栗协 议的某个状态从初始态不可到达，则表明协议有错误。 安全性( s a f e t y ) ：协议的安全性指协议运行时没有错误的情况出现。 这些情况包括：不可接收的事件，不可进一步向前的状态、错误的行 动、错误的条件、变量值越界等。坏事件一般导致死锁( d e a d l o c k ) 或活锁( 1 i v e l o c k ) 。死锁是指协议阻塞在某个状态而无法向前，活锁 是指协议做无意义地循环。 有界性：检验协议的某些属性或参数的值是否有界。 完整性：检验协议是否缺少应有的处理，是否有不期待的接收等。 可恢复性或自同步性：当出现差错后，协议是否能在有限的步骤内返 回到正常状态( 包括初态) 下执行。 2 2 形式化描述模型 目前，协议工程所采用的模型技术来自一些数学模型( 或方法) 和自动机模 型( 或程序模型) ，在理论上比较成熟的形式化模型方法主要有以下几种：有限 状态机f s m 、p e t r i 网、时序逻辑t l 、通讯进程演算c c s 。其中，t l 和c c s 主 要用于描述并发系统的通信过程，常用于协议验证；而f s m 和p e t r i 网都存在“状 态爆炸”的问题，不适用于构造大型复杂的协议，但因其直观易懂而被广泛应用。 2 2 1 有限状态机( f s m ) 模型 有限状态机f s m ( 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 ( e x t e n d e d f 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 ( c o m m u n i c a t i o n f i n i t e s t a t e m a c h i n e ：c f s m ) 。 基本f s m 可用一个五元组来表示：m ；( s ，i ，o ，6 ，丸) ，其中： 1 s 为有限的状态集，网络和分布系统中，状态可理解为发送、接收、空 ) ) ) ) 他 o 巧 中国科技大学顶卜学位论文第二章形式化描述挫术 闲或等待等： 2 i 为输入集，它既可以为有限集，电h 以为无限集，输入值与时矧有关 它可由报文来表示； 3 o 为输出的有限集合，其有关规则与i 相似； 4 8 为状态迁移函数，它由同一个时刻的输入信息及前一个时刻的状态决 定，即存在一个映射( 6 ：s i 一 s ) ； 5 九为动作输出函数，输出信息可以看作输入信息及状态的函数。它由t 时 刻的输入信息及t 时刻的状态决定，即存在一个映射( 九：s i o ) 。 8 和九表示f s m 的行为，在任何一个状态s ，若收到一个输入i i ，那么状 态迁移函数6 将指出自动机的新状态，而动作输出函数k 则指出f s m 产生的动 作和输出。 一个有限状态机可以采用状态转移图、状态转移矩阵或状态转移表等多种方 法来表示，其中最常用的是状态转移图。状态转移图是一个有向图，它的顶点代 表状态，而它的有向边代表状态转移。它的每一条有向边都标记了输入和输出。 f s m 最常使用的技术是可达性分析技术，可达性分析试图产生和检查协议所 有或部分可达状态。所谓可达状态是指协议从初始状态开始经历有限次转换之后 可达到的状态，所有可达状态构成可达图。可达性分析最重要的工作是产生和检 查可达图，判定是否存在死锁、活锁等协议错误。 在迄今已经出现的各种形式化描述技术中，有限状态机：f s m 是最为熏要的 一种形式描述技术，它是很多形式化方法的基础。这主要是由于它直观性强，可 实现与其它形式方法的组合和转换，且易于自动实现，因而在形式化描述中占有 重要地位。但f s m 模型不利于协议验证的实现，不易于描述复杂的系统，当进 行大型复杂协议的构造时，f s m 模型将面临状态爆炸的问题。 2 2 2 时序逻辑( t l ) 模型 p n u e l i 最先将时序逻辑引入计算机科学，用它作为并发程序的推理工具。时 序逻辑采用时序操作符来描述系统中事件的发生次序。常用的时序操作符有： o a 表示：a 在系统的下个状态为真； o a 表示：从当前状态开始，系统存在一个状态，a 为真； 中闫科技人学硕l 学位论文 第一二章蟛式化描述拄术 口a 表示：从当前状态丌始( 包括当前状态) ，a 总是为真； a b 表示：从当前状态开始赢到b 为真为止( 包括b 为真的那个状态) ，a 总 是为真。 时序逻辑的种类很多，随时间结构不