（通信与信息系统专业论文）基于petri网的tcp协议的研究.pdf

硕士学位论文摘要计算机网络技术是当今发展最迅速的计算机技术之一，而保证网络稳定可靠运行的关键是计算机网络协议。协议是计算机网络的灵魂，协议设计、开发复杂性的增加导致了协议工程技术的出现。协议工程用形式化的方法描述在协议严格的设计和维护中的各个活动。形式描述技术是整个协议工程的关键所在，它不但能够提供无二义性的描述，而且能够对描述进行形式分析和细化。目前已有多种成熟的形式描述技术，建立在异步并发概念上的p 吼r i 网是应用较广的一种形式描述技术。本文主要对p e t r i 网技术及其在网络协议中的应用进行研究。首先，简要介绍了形式描述技术在协议工程中的应用范围，p e t r i 网技术的基本概念和发展状况。其次，针对随机p e t 网在系统性能分析时其状态空间随着网规模的增大而指数性的增长，造成求解稳定状态概率的复杂性这一问题，提出了一种随机着色p e t r i 网( s c p n ) ，并给出了其系统性能分析的方法。在对t c p 协议作详细的非形式化分析的基础之上，利用有色p e t r i 网对其连接建立模块和数据传输模块建立了形式化模型，并通过有色p e t r i 工具c p nt 0 0 1进行模型的仿真，得到了模型的可达树。在系统地总结了p e t r i 网的性质基础上，通过p e t r i 网的可达树的分析方法，对模型的性质进行了分析与验证，从而确定了t c p 协议的逻辑正确性。最后通过所提出的随机着色p e t r i 网对t c p 协议的数据传输模块做了定量的性能分析。这些研究工作对于深入理解t c p 协议、分析改进协议和具体实现协议都起着不可或缺的重要作用。关键词：形式化描述；有色p e t r i 网；t c p 协议；可达树；随机着色p e t r i 网基于p e t r i 网t c p 协议的研究a b s t r a c tc o m p u t e rn e t w o r kt e c 1 1 1 0 l o g yi so n eo ft h em o s tr a p i d l y d e v e l o p i n gc o m p u t e rt e c h n o l o g i e s c o m p u t e rn e t 、v o r kp r o t o c o l i st h ek e yp o i n tt ok e e pn e t w o r ks t e a d ya n dw o r kr e l i a b l e a sw ea l lk n o w ：p r o t o c o li st h es o u lo fc o m p u t e rn e t w o r k t h ei n c r e a s eo fp r o t o c o ld e s i g na n dc o m p l e x i t yr e s u l t si nt h es t a r to fp r o t o c o le n g i n e e r i n gt e c h n o l o g v p r o t o c o le n g i n e e r i n gu s e saf o r m a lm e t h o dt od e s c r i b ea nt h ea c t i v i t i e sd u r i n gs t r i c tp r o t o c o ld e s i g na n dm a i n t e n a n c e f o n n a ld e s c r i p t i o nt e c h n i q u e sa r et h ek e yo ft h ew h o l ep r o t o c 0 1e n g i n e e r i n g ，w h i c hn o to n l yp r o v i d eu n a m b i g u i t yd e s c r i p t i o 玛b u ta l s op e 墒r mf o r m a l l ya n a l y s i sa n dt h i n n i n g s c u l l r e n t l yt h e r ea r em a n yk i n d so fw e l l d e v e l o p e df o r m a ld e s c r i p t i o nt e c h n i q u e s t h ep e t r in e t ，w h i c hi sb a s e do nt h ec o n c e p to fa s y n c h r o n o u sa n di n t e r c u r r e n t ，i so n eo ft h em o s tp o p u l a rd e s c r i p t i o nt e c h n i q u e s t h i sp a p e rc o n c e n t r a t e so np e t r in e tt e c h n o l o ；wa n di t sa p p l i c a t i o n si nt h en e 帆o r kp r o t o c 0 1 f i r s t l yw ei n t r o d u c et h ea p p l i c a t i o nr a n g ea b o u tt h ef o m a ld e s c r i p t i o nt e c h n i q u e si nt h ep r o t o c o le n g i n e e r i n g ，a n dt h eb a s i cc o n c e p t sa n dd e v e l o p m e n tc o n d i t i o n sa b o u tp e t r in e t w h i l et h es t o c h a s t i cp e t r in e t su s ei na n g l i c i z i n go ft h es y s t e mp e 怕r m a n c e ，t h es t a t es p a c ei n c r e a s e si ne x p o n e n t i a la st h es c a l eo ft h es y s t e ma c c r e t i o n ，t h a tl e a dt os o l v i n gs t a b i l i z a t i o np r o b a b i l i t ym o r ec o m p l e x i t v i na l l u s i o nt ot h i sd e f i c i e n c v w ep u tf o r w a r da 王( i n do fs t o c h a s t i cc o l o r e dp e t r in e t ( s c p n ) ，a n a l y z et h em e t h o d so ft h es t o c h a s t i cc o l o r e dp e t r in e t s ( s p u s e dt om o d e l i n ga n dp e r f o r m a n c eq u a n t i t a t i v ea n a l v s i s b ya n a l y z i n gt c pp r o t o c o ld e t a i l e d ，c o l o r e dp e t n e tw h i c hi so n eo fa d v a n c ep e t r in e t i su s e dt ob u i l daf 0 m a lm o d e lo fc o n n e c t i o nc o n s t r u c tm o d e la n dd a t at r a n s m i tm o d e l w eg e tt h er e a c h a b i l i t v1 r e eb vu s i n gc n pt o o lt oe m u l a t et h ec o l o rp e t r in e t sm o d e l w i t hs y s t e m a t i cc o n c l u s i o no nt h ep r o p e r t vo fp e t r in e t ，w bv a l i a t i n gt h e1 0 9 i cc o r r e c t n e s so ft c pp r o t o c o lb yt h em e t h o r d r e a c h a b i l i t vt f e eo fp e t r in e tt oa n a l v z et h em o d e l l a s t l v ，w eu s es t o c h a s t i cc o l o r e dp e t r in e t st om a k ear a t i o n a la n a l v s i sa b o u tt h em o d e lo ft h et c pp r o t o c 0 1 t h e s ew o r kh a sa ni m p o r t a n tr o l ei nd e e p l yu n d e r s t a n d i n g ，a n a l y z i n ga n dr e a l i z i n gt h ep r o t o c 0 1 k e yw o r d s ：f o r m a ld e s c r i p t i o n ；c o l o r e dp e t r in e t ；t c pp m t o c o l ；r e a c h a b i l i 够7 1 1 1 1 e e ；s t o c h a s t i cc o l o r e dp e t r in e t硕士学位论文插图索引图1 1 协议工程系统3图3 1t c p 报文格式2 l图3 2t c p 数据在口数据报重的封装2 3图3 3 使用三次握手的连接建立2 4图3 4 数据传送2 5图3 5 使用三次握手的连接终止2 6图3 6 半关闭2 7图3 7 滑动窗口2 9图3 8 带有指针的滑动窗口2 9图3 9 慢启动和拥塞避免3 1图3 1 0 快速重传和快速回复3 2图5 1t c p 连接的c p n 模型4 0图5 2t c p 数据传输的c p n 模型4 1图5 3t c p 协议连接建立的可达树4 4图5 4t c p 协议数据传输的可达树4 5图5 5 数据传输模型的马尔可夫链4 6i基于p e t r i 网t c p 协议的研究附表索引表5 1 颜色和变量类型的定义3 9表5 2 库所和变迁的定义3 9表5 3 颜色和变量类型的定义4 0表5 4 库所和变迁定义4 0表5 5t c p 协议的数据传输的s c p n 模型状态集4 6兰州理工大学学位论文原创性声明和使用授权说明原创性声明本人郑重声明：所呈交的论文是本人在导师的指导下独立进行研究所取得的研究成果。除了文中特别加以标注引用的内容外，本论文不包含任何其他个人或集体已经发表或撰写的成果作品。对本文的研究做出重要贡献的个人和集体，均已在文中以明确方式标明。本人完全意识到本声明的法律后果由本人承担。作者签名：醐吲叶月7 日学位论文版权使用授权书本学位论文作者完全了解学校有关保留、使用学位论文的规定，即：学校有权保留并向国家有关部门或机构送交论文的复印件和电子版，允许论文被查阅和借阅。本人授权兰州理工大学可以将本学位论文的全部或部分内容编入有关数据库进行检索，可以采用影印、缩印或扫描等复制手段保存和汇编本学位论文。同时授权中国科学技术信息研究所将本学位论文收录到中国学位论文全文数据库，并通过网络向社会公众提供信息服务。作者签名：；芬毒花导师签名缈矿| 日期：卅年厂月圻日日期：杉年r 月圹日硕士学位论文第1 章绪论计算机网络是计算机和通信密切结合的产物，近些年来得到了迅速的发张，已逐渐成为信息社会的基石。网络协议是计算机中不可缺少的的一个重要组成部分，它是计算机和计算机之间以及计算机和其他设备之间进行数据通信的必要条件。随着计算机通信和网络技术的不断提高，i n t e r n e t 迅速普及，网络规模不断扩大，网络系统的复杂性在协议方面体现出空间分布性、并发性、异步性、不稳定性和多样性，再也不可能用工程直觉的方法设计出高质量的协议，协议的完整性、正确性、安全性、可移植性和标准化都难以得到保证，而且协议实现后纠正协议描述错误的代价是十分可观。错误导致服务可靠性的降低，引起用户极大的失望，在这种情况下，需要合适的方法、技术和计算机辅助工具，来设计和维护通信协议。协议工程( p r o t o c o le n g i n e e r i n g ) 用形式化的方法描述在协议严格的设计和维护中的各个活动，它是研究对象为协议的软件工程，但它建立了一套比现有软件工程一般方法更严格的协议设计方法，使协议开发整个过程一体化、系统化和形式化【1 ，2 1 。其中，形式描述技术( f d l ，f o r m a ld e s c r i p t i o nt e c h n i q u e s ) 已经被认为是支持复杂系统开发的有用工具，特别是它能在更短时间内产生更高性能的软件产品。形式描述技术的主要目标是产生一个清晰的、精确的、完整的规范描述，并且为形式上精确定义的验证行为提供基础。1 1 课题的研究背景通信协议是计算机网络和通信网络中各种通信实体间交换信息所必须遵守的一组规则【3 】，它规定了信息交换的格式、内容和过程。具体定义如下：在计算机网络中，为了使计算机或终端之间能够正确地传递信息，必须有一整套关于信息传输顺序、信息格式和信息内容等的约定，这一整套约定称为通信协议。随着计算机通信和网络技术的不断提高，i n t e r n e t 迅速普及，网络规模不断扩大，到2 0 0 5 年初，仅中国内地联网计算机主机总数就达到2 0 8 3 万台，上网人数达到5 9 l o 万。由此带来的通信网络的复杂性与日俱增。现在，己经形成了以i n t e r n e t 为核心的计算机网络和p s t n ，g s m c d m a 为代表的通信网络。通信网络系统的复杂性在协议方面体现出空间分布性、并发性、异步性、不稳定性和多样性。这不仅意味着协议开发难度大，周期长，而且潜在错误多，协议开发过程中任何一点错误和缺陷都将给通信系统的稳定性、可靠性、安全性、容错性以及系统之间互通性和互操作性带来巨大的危害。因此，需要合适的方法、技术和计算机辅助工具，使开发过程工程化，以便提高协议的开发效率，促进标准化的协基于p e l r i 网的t c p 协议的研究议实现，因此一种新的方法学一协议工程学应运而生。它所包含的主要作业过程是：协议及服务的形式描述、协议验证、自动实现、一致性测试、协议转换和性能分析，其中形式描述技术( f d t ) 贯穿于整个协议开发过程的始终，是协议工程学的基础。协议开发过程就是开发协议的过程。开发协议有两种含义，一是为了满足新的通信需求，研究开发新的协议，制定协议标准；另一个则是在一个特定应用环境下，实现某个已经成熟的协议。所谓成熟的协议是指己经成为标准文本的协议，如t c p i p 协议等，也可以是即将成为标准文本的协议，如3 g p p 制定的一系列关于第三代移动通信的协议文本等。协议的开发包括六个过程【1 1 ：( 1 ) 协议设计，p d u 格式，协议机制，服务原语等设计；( 2 ) 协议描述，用某种语言确切的描述协议元素；( 3 ) 协议的验证与性能分析，对所描述的协议验证其正确性，分析其性能；( 4 ) 协议的实现，根据描述的协议产生网络硬软件；( 5 ) 协议的测试，对实现的协议进行测试；( 6 ) 协议的维护，对网络硬软件进行维护；协议工程，是指一体化的、形式化的协议开发过程。协议开发中所需要的各种开发、管理、维护工具，以及协议的不同表示构成协议工程环境。使协议开发一体化、形式化的理论和技术，以及协议工程系统建造技术通称为协议工程技术或协议开发技术( 简称协议技术) 。所谓一体化( i n t e g r a t e d ) 是指协议的设计、验证、实现和测试，在技术上前后衔接，并在同一个开发系统中完成。以往的协议开发没有做到一体化，技术上前后阶段不衔接。协议设计者凭自己的经验和智慧设计协议，用自然语言描述出来，经过他人审定或模拟之后，就予以公布。另外的人只在感兴趣时采用某种方法和理论对协议进行论证。有些协议公布后至今也无人对它进行验证。协议验证者往往也没有将验证结果直接反馈给协议设计者。协议实现者经常根据自己的环境和要求修改协议，协议实现之后，他们往往只要求自成系统，不考虑不同协议实现者的产物的互联问题。不考虑自己实现后的协议是否和颁布的协议一致，也不将协议实现中的问题反馈给协议实现者。协议的测试由实现者进行，实际上，这种测试只是一种程序动态调试手段。所谓形式化是指用形式描述语言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 s ) 连接协议开发的各个阶段。每种f d l 都以一种或多种形式描述技术做基础，有严格的语法和语义定义，它抽象于具体的实现，可符号执行，可转换翻译成程序设计语言。协议的形式描述是f d l 发展的最主要动因。当协议用一种f d l 描述之后，协议的自动化验证、自动化实现、自动化测试便可在协议工程系统中进行了。在协议工程的不同阶段，协议可以有不同的表示形式( 见图1 1 ) ，这些表示2硕士学位论文形式代表了不同开发阶段的结果。协议的表示形式有：非形式描述文本( i n f o r m a ls p e c i n c a t i o n ) ：用自然语言和图表表述的协议，易读易懂，但不严密，有多义性。形式描述文本( f o r m a ls p e c m 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 ) ：这是协议实现后的最终代码。一般与机器无关的源程序代码只占最终实现代码的一部分( 5 0 ) 。协议在一种机器上的实现还包括大量协议文本没有描述的程序，例如缓冲器分配管理、系统输入输出操作等，这部分程序称作与机器相关代码。测试套具( t e s ts u i t e ) ：这是一组关于协议测试步骤和测试数据的文件，它由协议的形式描述文本产生。测试套具是用另外一种语言描述的( 形式描述语言或非形式描述语言) 。性能分析非形式描述文本验证鳖蔗程序代码l 铡试套工炒( 前t芒皇v图1 1 协议工程系统【1 1协议工程包括下列多个子系统，每个子系统由多个软件工具构成。1 ) 转换( t r a n s f o r m a t i o n ) 系统该系统将协议的非形式描述文本转换成形式描述文本。该系统要求高智能化3善不基于p e t r i 网的t c p 协议的研究的软件去识别和读懂非形式描述文本，因此该系统实际上是一个人工系统。2 ) 验证( v e r i n c a t i o n ，v a l i d a t i o n ) 系统对协议进行验证检查，发现并修改潜在的错误。3 ) 性能分析( p e r f o r m a n c ea n a l y s i s ) 系统对协议性能进行分析评价，修改协议，提高性能。4 ) 翻译( t r a n s l a t i o n ) 系统将形式描述文本翻译成程序代码。5 ) 实现( i m p l e m e n t a t i o n ) 系统它实际是具体操作系统所提供的程序开发环境( 编辑、编译、连接、调试、排错等) 。实现代码在这个系统中产生。6 ) 测试( t e s t ) 系统测试套具在该系统中执行，对实现代码进行测试，分析结构，检测错误，将错误反馈给实现系统，修改实现代码。在某些情况下，错误信息还必须反馈给协议实现者。7 ) 测试套具生成( t e s ts u i t eg e n e r a t i o n ) 系统根据协议的形式化描述文本产生测试程序和测试数据，该系统的部分工作可有人工完成。图1 1 所示是一个完整的协议工程系统，随着协议工程技术的发展，系统中的软件工具将越来越完善，越来越方便，自动化程序也将逐步提高。形式化描述方法是协议工程核心部分，关联了协议工程中的各个过程。目前适用于协议工程的形式化描述方法种类繁多，各具特色，但也各有不足，使用什么样形式化描述方法进行协议设计、验证，乃至后续的协议测试，是协议工程领域中的一个重要的核心问题。协议验证( p r o t o c 0 1v e r i n c a t i o n ) 是协议工程的重要组成部分，是对通协议本身的逻辑性和正确性进行验证的过程。它处于协议工程中协议设计阶段之后，协议实现阶段之前。其工作过程一般是通过选择合适的形式化描述方法对协议进行形式化描述，然后用基于数学的方法，检验或证明协议设计的逻辑正确性。1 2 课题的研究现状1 2 1 形式化描述技术利用形化技术对模型进行描述以及验证理论的研究将直接影响到计算机通信协议开发技术的进步和发展。所以很多国家都投入了大量的人力物力从事这方面的研究工作。例如：英国的国家物理局n p l 、法国国家通信研究中心、德国国家通信研究局g m d 、美国国家标准化研究局、美国新罕布什尔大学互操作研究4硕士学位论文实验室都在这个领域投入了大量的研究力量。为了提供协议设计的坚实基础，要使用数学的方法，不但能够提供无二义性的描述，而且能够对描述进行形式分析和细化。协议形式化指使用形式描述技术( 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 应能支持协议工程活动的各个环节，特别是协议综合、验证、自动实现和一致性测试。利用数学技术允许开发描述语言的编译器和由描述派生的自动测试序列，这将大大提高协议实现和维护的能力，降低提供和维持信息服务的代价。作为一个f d t ，它有如下重要特性【4 】：1 ) 完整的语法和语义定义；2 ) 体系结构、服务和协议的可表达性；3 ) 协议重要特性( 如：无死锁) 的可分析性；4 ) 支持复杂协议的管理( 如：构造能力) ；5 ) 支持渐进细化的方法；6 ) 支持实现独立性( 包括并发性、非确定性和适当的抽象机制) ；7 ) 支持协议生命期的各环节，包括验证、实现和测试；8 ) 支持自动设计、验证、实现和维护方法；目前的形式化描述方法大都是采用以下几种形式化模型以及基于这些模型的形式化描述语言【4 】：1 ) 有限状态机f s m 和扩展有限状态机e f s m 模型：2 ) p e t r i 网模型；3 ) 消息序列图m s c 模型；4 ) 通讯进程演算c c s 和通讯顺序进程c s p 模型；5 ) 时序逻辑t l 模型；6 ) 构造类别代数模型；7 ) 基于扩展有限状态机模型( e f s m ) 的s d l ( s p e c i n 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 ) 语言和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 ) 语言；8 ) 基于经典集合论和前序逻辑的z 语言；9 ) 基于进程代数和多类代数的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 m c a t i o n ) ；1 0 ) 基于进程代数的r s l 语言；1 1 ) 基于抽象文字表示法的a s n 1 ；1 2 ) 基于谓词逻辑描述状态以及状态变迁的关系语言；1 3 ) 描述协议一致性测试用例的t t c n 语言；5基于p e t r i 网的t c p 协议的研究有限状态机是最常用的协议形式化描述技术，通常使用状态转移图( s t a t et r a n s i t i o ng r a p h ) 来表示。状态转移图是一个有向图，它的项点代表状态，而它的有向边代表状态转移。它的每一条有向边都标记了输入和输出。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 网( c o l o u r e dp e t r i n e t ：c p n )和时间p e t “网( t i m ep e t r in e t ：t p n ) 等等。e s t e l l e 、l o t o s 和s d l 是f d t 目前主要的三种国际标准，分别由i s o 和c c i t t 制定【5 】。1 9 7 6 年c c i t t ( i t u ) 颁布s d l ，是一种基于扩展状态变跃图和抽象数据类型的混合技术，已被电信公司广泛用于描述电子分组交换系统。八十年代i s o 制订o s i 参考模型时，发布e s t e l l e 和l o t o s ，在1 9 8 8 年确立了最后的国际标准文本。e s t e l l e 也基于扩展的状态变换模型，但使用p a s c a l 语法和数据类型，八十年代初有人试图协调e s t e l l e 和s d l ，终因没有共同的语义模型而失败。e s t e l l e 和s d l 规范呈现“转移化 风格，而l o t o s 规范呈现“结构化”风格。e s t e l l e 和s d l 有三个弱点：( 1 ) 语义需重新定义；( 2 ) 缺乏分析技术；( 3 ) 实现不具有独立性。l o t o s 提供形式语义，保证描述不存在二义性，便于分析和一致性测试理论的研究。没有哪一种形式化描述方法适合描述和分析复杂通信协议系统的所有方面。大多数形式化描述方法都是基于单一的形式化描述语言的，它们只适合描述系统的某些方面，如控制流、数据结构、行为等等；或只适合描述某种类型的系统，如顺序、并发、分布、实时等等。在实际应用中，往往需要使用多种形式化描述方法对系统的不同侧面进行描述和分析。1 2 2 协议验证技术协议验证【6 】的主要目的是试图在协议开发的前期最大限度地检测和纠正协议错误和缺陷，包括死锁( d e a d l o c k ) 、活锁( 1 i v e l o c k ) 、不可执行地行动、协议外部性能不符合服务要求等。协议验证技术多种多样，但主要可以分为三类：1 )可达性分析( r e a c h a b i l i t ya n a l y s i s )可达性分析是最常用的技术，是一种传统的、易于自动化处理的、有效的协议验证方法。但可达性分析需要从初始状态开始，枚举协议中的所有可达状态，随着通信协议的复杂性的不断增加，它所面临的状态爆炸问题( s t a t ee x p l o s i o np r o b l e m ) 也随之变得越来越突出。2 )逻辑证明( l o g i cp r o o f )逻辑证明用推理验算的方法严密地证明各种协议性质，所采用的技术主要来自于时态逻辑、谓词逻辑、代数验算等数学领域。6硕十学位论文3 )模拟( s i m u l a t i o n )模拟是有选择地对某些可执行地分支进行验证。它是前两种方法的一个补充，尽管它不可能包容所有的可能性。但它能更精确地反映系统的行为，提供理论分析所无法得出的结果。1 2 3 研究基于p e t r i 网的形式描述技术的意义1 9 6 2 年联邦德国的c a r la d a mp e t r i 在他的博士论文用自动机通信中首次使用网状结构模拟通信系统1 7 】。这种系统模型后来以p e t r i 网为名流传。从1 9 8 0年召开第一次p e t r i 网理论和应用的国际研讨会以来，每年一次的国际研讨会连续不断，p e t r i 网理论和应用在不断的充实和完善。最早将p e t r i 网用于协议描述研究的是加利福尼亚州立大学i r v i n e 分校的m e r l i n 博士，1 9 7 4 年他发表了“计算系统可恢复性的研究 的博士论文。法国的d i a z m 博士研究了基于p e t r i 网的协议描述技术，详细研究了p e t r i 网在协议描述和验证的方法，其后g b e r t e l o t 和r t e r r a t 又作了具体的论述。在2 0 世纪8 0 9 0 年代，澳大利亚的j b i l l i n g t o n 教授概述了p e t r i 网在协议工程中的应用，现在p e t r i 网系统已被用于许多复杂协议和服务的描述和分析之中。p e t r i 网理论是在并发的概念上建立起来的，它直观地表示了非确定性，可用于表达不同抽象级上的系统概念。p e t r i 网能用许多方法构造，例如，用简单c h a n n e l a g e n c y 网来表示系统结构，在逐步求精后定义系统的p e t r i 网行为。p e t “网有一套成熟的数学理论工具，建立了许多分析技术，包括可达性分析、不变量分析、保持特性的变换、构造理论、形式语言理论、同步距离以及网的分解和等价。p e t r i 网的形式基础是用p e t r i 网与其他并发模型建立了连接。这对分布式系统的描述和分析是很有益的。近几年来，人们的注意力集中在如何将代数的抽象数据类型融合在高级网结构中，极大地方便了表示描述协议和服务所用的高级p e t r i 网系统。选择p e t r i 网为研究f d t 的对象，有以下几条依据【7 】1 ) 3 种标准f d t 只支持协议工程的1 2 个活动。e s t e l l e 是一种过程语言，可以描述协议细节，用它描述的协议仅便于实现；l o t o s 描述协议实体的外部行为，不关心实体内部变化，用它描述的协议抽象级别高。l o t o s 定义了一套证明行为表达式的形式系统，用它描述的协议仅便于验证；s d l 是一种混合式的f d t ，缺乏形式语义，缺乏分析技术。2 ) p e t r i 网具有异步并发特性，因而决定了它的主要应用方向是分布式系统。根据外延公理，一个变迁的发生完全由它的外延决定，因与系统全局状态无关。这一点十分适合网络体系结构、协议和服务的特点。7基 p e t r i 网的t c p 协议的硼究3 ) p e t r i 网具备一套严密的数学理论，各种技术极有利于验证和分析。4 ) p e t r i 网表现出面向对象技术的各个特性，将是一种优良的可用图形表示的面向对象语言。5 ) p e t r i 网是协议工程中的研究热点和有国际倾向性的协议开发技术。有人推测，现有的协议形式描述技术必须具有一个公共语义模型，能够把这些技术转换成公共模型，并且分析、仿真和测试的各个工具都基于公共模型。p e t r i 网可能为e s t e l l e ，l o t o s 和s d l 这3 种标准f d t 提供如上所述的一个公共模型。1 2 3 1 提高软件技术水平目前，中国软件的技术水平跟世界上先进的软件开发技术水平相比，存在着很大的差距。中国没有在国际上知名的商品化的软件产品，中国的软件业在中国生产应用中只是起到一个不起眼的角色。中国是一个软件需求大国，但是外国的软件产品在中国的各个应用方面挑着大梁。当然，中国的软件业已经大有发展，但是中国不能局限于自己国家的一些小的应用开发，应走向世界，在国际市场上占有一席之地。这就需要中国的软件产品技术含量要高，最重要的就是要具有较高的可靠性。国际上大型的高可靠性的软件开发都首先使用形式描述技术对该系统进行描述，然后验证、实现。该技术能在软件开发的各个阶段进行跟踪测试，能及早发现错误以减少后期发现所浪费的大量资金，能通过工具集进行自动转换，以减少人员的编写代码量。目前，形式描述技术在国际上的主要应用还是在通信领域。国际上已经提出要把形式描述技术进行推广普及到工业领域。1 2 3 2 便于网络通信协议的开发为使通信协议设计具有正确性，完整性和安全性，并使之易于验证和实现，必须不断开发和完善通信协议的形式化技术，提高协议设计的规范化和理论化程度。所谓协议的形式化技术主要是指协议及服务规范的形式描述、协议的设计验证、实现验证和一致性测试，这已成为网络与分布式系统领域中一个十分重要的研究课题。在通信系统和服务的设计初期阶段，讨论主要集中在细节层次上，这些细节层次反映了当时的知识层面( 关于数据、消息、组件等) 。包括不相关细节的描述易于模糊隐藏在一个功能部件或服务背后的主要思想，特别是当它们需要进一步修改和更加精确的描述时。而且如智能网络的位面一样，几个细节和抽象等级( 层次) 经常混在一个描述当中。当着眼于要实施的任务和它们的因果关系时，如果提供更加可维持的和可重用的方案描述，从消息中抽象出来的可视化符号能在主要控制流方面给予帮助。因此，可视化符号经常被使用，但是它主要着眼于消息的交换。这样在相关消息和系统的组件也许不知道的情况下，在设计阶段初期定义功能性是不合适的。而且，在服务描述或在给定服务的抽象等级层面内部8硕士学位论文或之间可能存在一些模糊的、不一致的或不需要的交互作用。这些用传统的检查方法很难察觉，且经常隐藏其中直到实现后才被发现，这时校正这些错误不仅开销相当大，而且系统的相互协作能力也会受到很大的危害。开发如分布式系统的复杂系统最重要的方面是为能够合理地确保该系统的正确运行而进行的验证。系统验证在整个系统的开发过程中都是极其重要的，系统设计过程中最有代表性的实施方法是以迭代( 反复或循环) 的方式处理每个连续阶段的逐渐增加的复杂性。这些技术的实现必须靠形式描述技术。形式描述技术是完整的，形式程序的验证也是最可靠的。1 3 课题的应用背景描述系统的传统方法绝大部分依赖于自然语言和图表方法，但是这些方法很难做到以下两点，即写出清晰的描述规范和对描述规范进行分析。而且，如果在规范描述阶段引入了一些错误或遗漏了一些部分而没有被发觉，那么在开发周期中校正它们花费是相当大的。形式方法致力于解决传统方法所不能解决的或很难解决的问题。形式方法的一个定义就是，使用一组工具和符号( 包括形式语义) 清晰详细描述计算机系统的需求，它们支持描述规范性能的验证和关于这个描述规范最终实现的正确性验证。形式方法主要用于以下几种系统【4 j ：1 ) 复杂的系统( c o m p l e x ) ：抽象是一种处理庞大系统复杂性的非常重要的技术，是形式方法这个概念的中心。2 ) 并发的系统( c o n c u r r e n t ) ：分布式系统产生并发性。当我们发现很难用因果关系推出并发性时，某种形式方法即被研究出来以解决这个难题。3 ) 高质量的系统( q u a l i t y c r i t i c a l ) ：这些软件出问题时并无危险但经济上损失很大，例如金融和电信方面的应用软件。4 ) 高安全的系统( s a f t y c r i t i c a l ) ：这些软件出问题时可能危害人的性命安全，例如遥控自动驾驶系统和铁路信号传输系统。5 ) 高可靠性的系统( s e c u r i t y c r i t i c a l ) ：这些软件出问题时意味着没授权用户的非法进入敏感信息区，例如医疗记录和安全数据库。6 ) 标准化的系统( s t a n d a r d i z e d ) ：这种系统设计出来要满足某种国际上认可的标准，重要的是这些标准可以被一致性的解释出来，例如语言规范和协议标准。1 4 课题研究的内容本文主要对p e t r i 网技术及其在网络协议中的应用进行研究。首先，简要介绍了形式描述技术在协议工程中的应用范围，p e t r i 网技术的基本概念和发展状9基 p e t r i 网的t c p 协议的研究况。其次，针对随机p e t r i 网在系统性能分析时其状态空间随着网规模的增大而指数性的增长，造成求解稳定状态概率的复杂性这一问题，提出了一种随机着色p e t r i 网( s c p n ) ，并给出了其系统性能分析的方法。在对t c p 协议作详细的非形式化分析的基础之上，利用有色p e t r i 网对其连接建立模块和数据传输模块建立了形式化模型，并通过有色p e t r i 工具c p nt 0 0 l进行模型的仿真，得到了模型的可达树。在系统地总结了p e t r i 网的性质基础上，通过p e t r i 网的可达树的分析方法，对模型的性质进行了分析与验证，从而确定了t c p 协议的逻辑正确性。1 5 论文的结构第1 章绪论。第2 章p e t r i 网基本原理：主要介绍了p e t r i 的定义，基本性质，应用和发展，以及一些扩展的p e t r i 网( 有色p e t r i 网( c p n ) 、随机p e t r i 网( s p n ) ) 。第3 章t c p 协议的分析：主要对t c p 协议的的连接建立，数据传输，连接终止，流量控制，拥塞控制等方面做作了详细的分析。第4 章一种随机着色p e t r i 网：针对随机p e t “网在系统性能分析时其状态空间随着网规模的增大而指数性的增长，造成求解稳定状态概率的复杂性这一问题，提出了一种随机着色p e t r i 网( s c p n ) ，并分析了其系统性能分析的方法第5 章t c p 协议的p e t r i 网模型及性能分析：根据有色p e t r i 网的建模的方法和工具c p nt o o l ，对t c p 协议的连接建立和数据传输建立了有色p e t r i 网模型，得到了可达树，通过可达树的方法对协议模型的真确性进行验证。最后通过这种随机着色p e t “网对t c p 协议的数据传输模块做了定量的性能分析。1 0硕士学位论文第2 章p e t r i 网基本原理p e t r i 网是一种用于并发系统建模和分析的重要工具【7 1 。它着眼于系统中发生的变化，变化发生的条件及发生后的影响，变化间的关系等。p e t r i 网系统可以分作三类：基本网系统，网的库所表示一种布尔状态，因此每个库所中最多只能有一个标记；库所变迁系统，一个库所可以有多个标记；高级网系统，如谓词变迁系统和有色p e t r i 网系统，高级网系统与前两种网系统的差异在于高级网系统的标记具有类型。由于高级p e t r i 网提供了类型和层次结构描述能力，能够以一种紧凑的、简化的模型来描述一个复杂系统，因此本文主要采用高级p e t r i 网建立形式化模型和系统性能分析。2 1p e t r i 网的基本概念2 1 1p e t r i 网的定义定义2 1 ：三元组n = ( p t ；f ) 称为有向网( d i r e c t e dn e t ，简称网( n e t ) ) 的充分必要条件是【7 】：1 ) 尸n 丁= a ；2 ) j p u 丁a ；3 ) fep 丁u 丁p ( i ”为笛卡儿积) ；4 ) 面聊( ，) u c d d ( f ) = p u 丁；其中面聊( f ) = xi 砂：( x ，y ) 毋，d ( f ) = yl 了x ：( x ，y ) 毋为f 的定义域和值域。p 和t 分别称为网n 的库所集和变迁集，p 的元素称为库所( p l a c e ) ，t 的元素称为变迁( t r a n s i t i o n ) 。f 为网n 的流关系( f l o wr e l a t i o n ) 。库所集和变迁集是有向网的基本成分，流关系是从它们构造出来的，所以在p t 和f 之间用分号( ；) 隔开。库所和变迁是两类不同的元素，所以p n 丁= a ，而尸ur g 表示网中至少要有一个元素。每个库所代表一种资源，资源的流动由流关系规定，所以变迁只能与库所有直接的流关系：f 尸丁u r 尸( ”为笛卡儿积) ，不参与任何变迁的资源表现为孤立的库所，不引起资源流动的变迁表现为孤立的t 元素，如聊( f ) u c d d ( ，) = 尸u 丁规定网中不能有孤立元素。一个网可以用一个有向二分图来表示：库所用圆圈或椭圆来表示，变迁用方框或粗杠来表示，对x ，少p u 丁，若( x ，y ) f ，则从x 到y 画一条有向弧。显然，基于p e t r i 网的t c p 协议的石j f 究有向弧只存在于圆圈和方框之间，任意两个圆圈之间或任意两个方框之间都没有有向弧连接。定义2 2 ：设n = ( p ，t ；f ) 为一个网，对x 尸u r ，记o x = y p u ri ( y ，p ) f )x o = y p uri ( x ，y ) f )称o x 为x 的前集或输入集，妒为x 的后集或输出集，o x u ，称为元素x 的外延。显然，一个变迁的外延是由某些库所组成的集合，一个库所的外延是由某些变迁组成的集合。2 1 2 网系统的定义定义2 3 ：六元组= ( p ，t ；f ，k ，w ，m o ) 构成网系统的条件是8 】：( 1 ) n = ( p t ；f ) 构成有向图，称为的基网。( 2 ) k ，w ，m o 依次为n 上的容量函数、权函数和标识。m o 称为的初始标识( i n i t i a lm a r k i n g ) 。( 3 )任一变迁f 丁在m 有发生权的条件是：跏o f ：m ( p ) ( p ，) 跏，o ：( m ( p ) + 肜( p ，f ) ) k ( p ) ，记作m 【t 。( 4 )若m t ，则t 在m