（计算机应用技术专业论文）基于有限状态机的ip协议研究.pdf

基于有限状态机的i p 协议研究摘要摘要随着计算机网络、通信网络以及分布式系统的不断发展，通信协议日渐复杂化。形式化技术和方法在网络协议设计中占有举足轻重的作用。本文对在网络通信协议设计中的模型方法进行了研究。归纳总结了形式化模型、形式化描述方法以及形式化综合方法，通信服务和协议的构造方法。文章主要由六部分构成：绪论部分介绍了研究的问题、背景及相关知识；第二章介绍了有限状态机的相关理论、扩展及对协议模型方法；第三章和第四章主要介绍了e s t e l l e 为代表的形式化描述技术。针对e s t e l l e描述通道的局限性，给出了一个描述广播通道的扩展：第五章到第七章，首先详细分析了t b q c p 协议，包括用到的容错机制；给出其状态机模型以及改进的状态机模型；并使用e s t e l l e 描述。第八章论述了形式化综合方法，仍在研究的一种方法。最后是论文总结。关键字：f s m ；协议；转换；v f n m ；e s t e l l e基于有限状态帆的l p 协议研究a b s w a c ta b s t r a c tf o r m a lm e t h o d sa n dt e c h n o l o g i e sa r em o r ei m p o r t a n ti nd e s i g no fc o m m u n i c a t i o np r o t o c o l sb e c a u s eo f t h ec o m p l e xo f p r o t o c o l s t h i st h e s i sf o c u s e so nt h es t u d yo nf o r m a lm o d e l so fp r o t o c o l s i n c l u d i n gf o u rp a r t s f i r s t 。f i n i t es t a t em a c h i n ea n di t se x t e n d i n gf o r m a l i z a t i o n sa r ei n t r o d u c e da sam a j o rm e t h o df o rs t u d yo np r o t o c 0 1 s e c o n d 。e s t e l l e ，o n eo ff o r m a ld e s c r i p t i o nt e c h n i q u e 。i se x t e n d e dt ob r o a d c a s tc h a n n e lf o rd e s c r i p t i o np o w e r t h i r d ，c o n c r e t ep r o t o c o l sa r ea n a l y z e do rm o d e l e d f i n a l l y , w ei n t r o d u c ef o r m a ls y n t h e s i st h a ta r ed e v e l o p i n gt e c h n i q u e s k e y w o r d ：f s m ；p r o t o c o l ；t r a n s i t i o n ；v f n m ；e s t e l l ei i i原创性声明矿7 2 1 0 0 j本人声明，所呈交的学位论文是本人在导师指导下进行的研究工作及取得的研究成果。尽我所知，除了论文中特尉加以标注和致谢的地方外，论文中不包含其他人已经发表或撰写过的研究成果，也不包含为获得兰州理_ l ：大学或其他单位的学位或证书而使用过的材料。与我共同工作的同志对本研究所作的贡献均已在论文中作了明确的说明。作者签名：塑! 皇篮日期：兰竺竺年月日关于学位论文使用授权说明本人了解兰州理工大学有保留、使用学位论文的规定，即：学校有权保留学位论文，允许学位论文被查阅和借阅；学校可以公布学位论文的全部或部分内容，可以采用复印、缩印或其它手段保存学位论文：学校可根据国家或甘肃省有关部门规定送交学位论文。作者躲丝车翩虢务经吼煎年五月l 日基于有限状态机的l p 协议研究+ 绪论第l 章绪论随着网络服务要求的提高，网络系统的复杂性在协议方面体现出空间分布性、并发性、异步性、不稳定性和多样性，通信协议再也不可能用工程宜觉方法设计出高质量的协议。协议的完整性、正确性、安全性、可移植性和标准化都难以得到保证，而且协议实现后纠正协议描述错误的代价是十分可观。错误导致服务可靠性的降低，引起用户极大的失望，在这种情况下，需要合适的方法、技术和计算机辅助工具，来设计和维护通信协议。协议工程( p r o t o c o le n g i n e e r i n g ) 用形式化的方法描述在协议严格的设计和维护中的各个活动，它是研究对象为协议的软件工程，但它建立一套比现有软件工程一般方法更严格的协议设计方法，使协议开发整个过程体化、系统化和形式化 1 ，2 ，3 。其中，形式化技术( f o r m a lt e c h n i q u e s ) 已经被认为是支持复杂系统开发的有用的方法和工具，特别是它能在更短时间内产生更高性能的软件产品。形式化方法的主要目标是产生一个清晰的、精确的、完整的规范模型和描述，并且为形式上精确定义的验证行为提供基础 1 ，4 ，5 。如图1 所示，在协议的开发中各个活动间的关系图 6 。性能分析图1 1 协议开发主要活动问的关系1 i 课题的研究背景1 1 1 协议工程概述“2 3 蚰通信协议是指两个或多个通信实体相互通信的全过程中所必须遵守的规约和格式之集合。它也可视为协调两个或多个并发进程之规程。近年来，随着计算机网络、通信网络以及分布式系统的不断发展，通信协议有日渐复杂化的趋向。计算机网络及通信已出现了一些令人瞩目的新技术，如信息高速公路、高速信息网络、宽基于有限状态机的【p 协议研究+ 绪论带综合业务数字网( b i s d n ) 、a n 网络、多媒体通信等。这些新型技术对通信协议的设计提出了新的要求。为了使通信协议设计和实现能理论化和规范化地进行。一种新的方法学一协议工程学应运而生。它所包含的主要作业过程是：协议及服务的形式模型、形式描述、协议验证、自动实现、一致性测试、协议转换和性能分析。一体化的、形式化的协议开发过程叫做协议工程。协议开发中所需要的各种开发、管理、维护工具，以及协议的不同表示构成协议工程环境。使协议开发一体化、形式化的理论和技术，以及协议工程系统建造技术通称为协议工程技术或协议开发技术( 简称协议技术) 。所谓一体化( i n t e g r a t e d ) 是指协议的设计、验证、实现和测试，在技术上前后衔接，并在同一个开发系统中完成，体化即系统化。以往的协议开发没有做到一体化，技术上前后阶段不衔接。协议设计者凭自己的经验和智慧设计协议，用自然语言描述出来，经过他人审定或模拟之后，就予以公布。另外的人只在感兴趣时采用某种方法和理论对协议进行论证。有些协议公布后至今也无人对它进行验证。协议验证者往往也没有将验证结果直接反馈给协议设计者。协议实现者经常根据自己的环境和要求修改协议，协议实现之后，他们往往只要求自成系统，不考虑不同协议实现者的产物的互联问题。不考虑自己实现后的协议是否和颁布的协议一致，也不将协议实现中的问题反馈给协议实现者。协议的测试由实现者进行，实际上，这种测试只是一种程序动态调试手段。1 ) 转换( t r a n s f o r m a t i o n ) 系统包括两部分：一是从用户需求转化成服务描述；另一个是从服务描述转化成协议描述。该系统将协议的非形式描述文本转换成形式描述文本。该系统要求高智能化的软件去识别和读懂非形式描述文本，因此该系统实际上是一个人工系统。2 ) 验证( y e r i f i 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 2 形式化模型技术概述形式模型技术( f m t ) 有多种，主要包括状态变跃技术( 如p e t r i 网、有限状基于有限状态机的i p 协议研究+ 绪论态机f s m 等) 、抽象数据类型、文法、时态逻辑( t e m p o r a ll o g i c ) 、高级程序设计语言、集合论和迸程代数( p r o c e s sa l g e b r a ) 等，还有一些混合技术。大多数扩展的状态变跃技术具有坚实的数学基础，例如b e l l 实验室开发的s e l c c f i o n r e s o l u t i o n模型提出了个形式框架，从数学上给出了精确盼语义，把状态规的构造定义成形式代数的产物，阐述了化简方法，解决了可达性分析时的状态爆炸问题，提供了逐步求糟方法。但是这个模型是同步的，所有处理由同一个全局时钟控制，数据流没有表示，抽象级太低。一般来说，扩展的状态变跃技术缺乏形式语义，分析功能弱。所有具有并发功能的程序设计语言中，几乎没有哪种语言是支持非确定性的，而且大多数语言比较复杂，分析困难，没有达到具备实现独立性的抽象程度，当然程序设计语言的最显著优点是只要有编译器，描述可以直接实现。进程代数很有发展前景，它具有一套完善的等价理论，如果与两论相结合，可以用一套完善的分析技术提供一个结构清晰的模型。大多数抽象方法( 时态逻辑、集合论等) 描述严密、实现独立性完好，但几乎不能直观描述性质，分析不很复杂的协议也十分困难，并且需要手工证明，目前缺少这些技术的辅助工具n 5 1 。在迄今出现的各种形式化模型技术中，f s m 是应用极为广泛的一种模型技术i6 1 。它是许多形式化方法的基础。现在许多通信系统采用f s m 来分析和验证。它能够采用图表方式，直观性强，可以与其他形式方法组合和转换，易于自动实现，因而占有重要的地位。但是由于在构造可达树( 图) 时存在状态爆炸问题，不利于协议验证的实现；同时，由于采用图表方式，限制了它的描述能力，需要对其进行扩展，才能表述更复杂的系统。1 1 3 形式描述技术为了提供协议设计的坚实基础，要使用数学的方法，不但能够提供无二义性的描述，而且能够对描述进行形式分析和求精。协议形式化指使用形式描述技术( 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 2 】。理想的f d t 应能支持协议工程活动的各个环节，特别是协议综合、验证、自动实现和一致性测试。利用数学技术允许开发描述语言的编译器和由描述派生的自动测试序列，这将大大提高协议实现和维护的能力，降低提供和维持信息服务的代价。作为一个f d t ，它有如下重要特性俐：完整的语法和语义定义；体系结构、服务和协议的可表达性；协议重要特性( 如：无死锁) 的可分析陛；支持复杂协议的管理( 如：构造能力) ；支持逐步求精的方法；支持实现独立性( 包括并发性、非确定性和适当的抽象机制) ；支持协议生命期的各环节，包括验证、实现和测试；支持自动设计、验证、实现和维护方法。目前主要有三种国际标准f d t ，分别由i s o 和c c i t t 制定【2 ，6 1 。第一种是在1 9 7 6年由c c i t t ( i t u ) 颁布的s d l ( s p e c i f i e a t i o na n dd e s c r i p t i o nl a n g u a g e ) ，是一种基于扩展状态变跃图和抽象数据类型的混合技术，已被电信公司广泛用于描述电子分组交换系统。八十年代i s o 制订o s l 参考模型时，发布了二个f d t ，即基于有限状态机的i p 协议研究+ 绪论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 ) 和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 ) ，在1 9 8 8 年确立了最后的国际标准文本。1 1 4e s t e l l e 技术概述“”e s t e l l e 是基于扩展的状态变迁模型，但使用p a s c a l 语法和数据类型。它有一个形式化的独立于实现的语义。e s t e l l e 标准颁布以后，一直到1 9 9 4 年，e s t e l l e研究小组主要致力工具包的研制，1 9 9 6 年以后，e s t e l l e 标准又被改进了5 0 多处，不过直到现在也没有见到e s t e l l e 的升级版本。1 1 5 研究形式化技术的意义1 , 1 5 1 形式化技术的应用可以提高我国茸前的软件技术水平目前，中国软件的技术水平跟世界上先进的软件开发技术水平相比，存在着很大的差距。中国没有在国际上知名的商品化的软件产品，中国的软件业在中国生产应用中只是起到一个不起眼的角色。中国是一个软件需求大国，但是外国的软件产品在中国的各个应用方面挑着大梁。当然，中国的软件业已经大有发展，但是中国不能局限于自己国家的一些小的应用开发，应走向世界，在国际市场上占有一席之地。这就需要中国的软件产品技术含量要高，最重要的就是要具有较高的可靠性。国际上的大型的高可靠性的软件开发都首先使用形式描述技术对该系统进行描述，然后验证、实现。该技术能在软件开发的各个阶段进行跟踪测试，能及早发现错误以减少后期发现所浪费的大量资金，能通过工具集进行自动转换，以减少人员的编写代码量。目前，形式描述技术在国际上的主要应用还是在通信领域。国际上已经提出要把形式描述技术迸行推广普及到工业领域。1 , 1 5 2 形式化技术在网络通信协议的开发过程中占有举足轻重的作用为使通信协议设计具有正确性，完整性和安全性，并使之易于验证和实现，必须不断开发和完善通信协议的形式化技术，提高协议设计的规范化和理论化程度。所谓协议的形式化技术主要是指协议及服务规范的形式描述、协议的设计验证、实现验证和一致性测试，这已成为网络与分布式系统领域中个十分重要的研究课题。在通信系统和服务的设计初期阶段，讨论主要集中在细节层次，这些细节层次反映了当时的知识层面( 关于数据、消息、组件等) 。包括不相关缅节的描述易于模糊隐藏在一个功能部件或服务背后的主要思想，特别是当它们需要进一步修改和更加精确的描述时。而且如智能网络的位面一样，几个细节和抽象等级( 层次) 经常混在个描述当中。当着眼于要实施的任务和它们的因果关系时，如果提供更加可维持的和可重用的方案描述，从消息中抽象出来的可视化符号能在主要控制流方面给予帮助。因此，m s c 符号经常被使用，但是它主要着眼于消息的交换。这样在相关消息和系统的组件也许不知道的情况下，在设计阶段初期定义功能性是不合适的。而且，在服务描述或在给定服务的抽象等级层面内部或之间可能存在一些模糊的、不一致的或不需要的交互作用。这些用传统的检查方法很难察觉，且经常隐藏其中直到实现后才被发现，这时校正这些错误不仅花费相当大，而且系统的相互协作能力也会受到很大的危害。开发如分布式系统的复杂系统摄重要的方面是为能够合理地确保该系统的正确运行而进行的验证。系统验证在整个系统的开发过程中都是极其重要的。系统设计过程中最有代表性的实施方法是以迭代( 反复或循环) 的方式处理每个连续阶段的逐渐增加的复杂性。这些技术的实现必须靠形式描述技基于有用状态机的i p 协议研究绪论术。形式描述技术是完整的，形式程序的验证也是最可靠的。1 2 课题的应用背景描述系统的传统方法绝大部分依赖于自然语言和图表方法。但是这些方法很难做到以下两点：写出清晰的描述规范和对描述规范进行分析。而且，如果在规范描述阶段引入了一些错误或遗漏了一些部分雨没有被发觉，那么在开发周期中校正它们花赞是相当大的。形式方法致力于解决传统方法所不能解决的或很难解决的问题。形式方法的一个定义就是，使用一组工具和符号( 包括形式语法和语义) 清晰地详细描述计算机系统的需求，它们支持描述规范的性能的验证和关于这个描述规范的最终实现的正确性验证。形式方法主要用于以下几种系统：奉复杂的系统( c o m p l e x ) ：抽象是一种处理庞大系统复杂性的非常重要的技术，是形式方法这个概念的中心。幸并发的系统( c o n c u r r e n t ) ：分布式系统产生并发性。当我们发现很难用因果关系推出并发性时，某种形式方法被研究出来以解决这个难蹶。掌高质量的系统( q u a i t y - c r i t i c a l ) ：这些软件出闯题时并无危险但经济上损失很大，例如金融和电信方面的应用软件。商安全的系统( s a f t y c r i t i c a l ) ：这些软件出问题时可能危害人的性命安全，例如遥控自动驾驶系统和铁路信号传输系统。术高可靠性的系统( s e c u r i t y c r i t i c a l ) ：这些软件出问题时意味着没授权用户的非法进入敏感信息区，例如医疗记录和安全数据库。木标准化的系统( s t a n d a r d i z e d ) ：这种系统设计出来要满足某种国际上认可的标准，重要的是这些标准可以被一致性的解释出来，例如语言规范和协议标准。基于有限状态机的l p 协议研究有限状态机基础第2 章有限状态机基础2 1 形式化模型技术概论协议形式化模型是协议分析和设计的核心技术之一。基于形式化模型，可以实现网络协议的形式化规格，从而为协议的形式化分析与验证、协议综合、协议测试以及协议实现等提供良好的基础。同时，它也是协议形式化描述语言的基础。本章将对协议的主要形式化模型进行介绍。主要包括：有限状态机、p e t r i 网、时序逻辑和进程演算等。本章重点介绍有限状态机模型技术。2 2 经典有限状态机2 2 1f s m 的基本定义“4 ”1有限状态机( f s m ，f i n i t es t a t em a c h i n e ) 是一种数学模型。它包括以下几个部分：一个有限状态集，用于描述系统中的不同状态：一个输入集，用于表征系统所接收的不同输入信息；一个状态转移规则集，用于表述系统在接收不同输入下从一个状态转移到另外一个状态的规则。有限状态机可由如下形式定义给出。定义：有限状态机：有限状态机是一个五元组m ：( 母，6 ，q 0 ，f ) ，其中( 1 ) q = q o ，q 1 ，q n 是有限状态集合。在任一确定的时刻。有限状态机只能处于一个确定的状态q i ；( 2 ) = ol ，o2 ，om ) 是有限输入字符集合，在任确定的时刻，有限状态机只能接收一个确定的输入oj ；( 3 ) 6 ：q 一q 是状态转移函数，如果在某一确定的时刻，有限状态机处于某一状态q i q ，并接收个输入字符oj，那么下一时刻将处于一个确定的状态q = 6 ( qi ，oj ) q 。在这里规定q = 6 ( q ，) ，即：对任何状态q ，当读入空字符e 时，有限状态机不发生任何状态转移；( 4 ) q 0 q 是初始状态，有限状态机由此状态开始接收输入；( 5 ) f q 是终结状态集合，有限状态机在达到终态后不再接收输入。2 2 2 状态转移图对于有限状态机m = ( q ，6 ，q 0 ，f ) 的转移函数6 ，用圆圈( 节点) 表示状态；将存在转移关系的状态用有向弧连接，并在有向弧旁标注相应的输入字符；用标有箭头的节点表示初始状态；属于终结状态集中的状态用双圈表示。由上述规则所建立的有向图称为状态转移图。此外，还用到状态转换表和状态转换矩阵。2 2 3 非确定有限状态机非确定有限状态机是一个五元组m = ( q ，z ，6 。q 0 ，f ) ，其中( 1 ) q = q 0 ，q 1 ，q n ) 是有限状态集合；( 2 ) = ( o1 ，o2 ，o i l lj 是有限输入字符集合：6基于有限状志机的f p 协议研究有限状奋机基础( 3 )6 ：0 xz 一2 。是状态转移函数，如果在某一确定的时刻，非确定有限状态机处于某一状态q i q ，并接收一个输入字符oj，那么下时刻将处于某一状态子集6 ( q i ，oj ) = p 1 ，p 2 ，p k ) ( p i q 。i = 1 ，2 ，k ) 。在这里规定q o ( q ，0 ) ，剐：划任何状态q ，当接收空字符c 时，有限状态机不发生任何状态转移；( 4 ) q 0 q 是初始状态，有限状态机由此状态开始接收输入；( 5 ) fe q 是终结状态集合。在非确定有限状态机中，对于某些q e q 和某些o ，8 ( q ，o ) 可能有多种转移选择，从而带来非确定性。2 2 4 有限状态机的简写形式在一些情况下。我们讨论问题的重点集中在有限状态机或非确定有限状态机m- - ( 0 ，6 ，q 0 ，f ) 的状态集( q ) 、输入集( ) 和状态转移函数( 6 ) 上。这时候，可用如下三元组或四元组表示：m = ( q ，6 ) 或者m = ( q ，6 ，q 0 ) 。2 3 带输出的有限状态机经典的f s m 有两个带输出( 或动作) 的状态机解释：m o o r e 机和m e a l y 机。m c a l 3 ，机将状态转换和动作联系起来。动作需要消耗时间，所以m e a l y 机在动作执行l 0 时候，处于两个状态之问，容易引起概念上的混乱( 有些m e a l y 机采用动作零时问假设自v 决这个问题) 。m o o r e 机很好的避免了这种情况。在m o o r e 机中，动作与状态联系起来，因此，状态总能很好的定义。从形式上来看，m o o r e 机的输出( 或动作) 只与现行状态有关，而m e a l y 机的输出( 或动作) 却与现行状态和现行输入两者有关。m e a l y 机和m o o r e 机在数学上是等价的( 一个总能转换成另一个) ；但是，一般来说，同一系统，m o o r e 机建模要求较多的状态。因为，m e a l y 机对同一状态能使用不同的转换( 对不同触发的转换) ，而且能执行不同的动作；m o o r e 机必须使用不同的状态来表示不同动作被完成的条件。2 3 1m o o r e 机m o o r e 机可形式定义为六元组m ；( q ，z ，6 ， ，q 0 ) ，其中( 1 ) q = q 0 ，q l 。，q n ) 是有限状态集合：( 2 ) = ( o1 ，o2 ，on l 是有限输入字符集合；( 3 ) d = f a l ，a2 ，ar ) 是有限输出字符集合；( 4 ) 6 ：0 x 一岔是状态转移函数；( 5 ) ：q 一彳是输出函数；( 6 ) q 0 q 是初始状态。基于有般状态机的j p 协议研究有限状态机基础在上述m o o r e 机的定义中，我们注意到m o o r e 讥只是在接收输入串的过程中不断改变状态，并且在每个状态上有字符输出。常用来表述初始状态和终结状态。2 3 2m e a l y 机m e a l y 机可形式定义为六元组m = ( q ，4 ，5 ，盖，q 0 ) ，其中( 1 ) q = f q 0 ，q l ，q n ) 是有限状态集合；( 2 ) ； o1 ，o2 ，o m j 是有限输人字符集台：( 3 ) 4 = a l ，a2 ，ar ) 是有限输出字符集合；( 4 ) 6 ：q 一2 。是状态转移函数；( 5 ) ：q 一是输出函数；( 6 ) q 0 q 是初始状态。在上述m e a l y 机定义中，除输出函数凡外q ，4 ，6 ，q 0 的含义均同m o o r e机相同。 ( q ，a ) = a 给出了当机器进入状态q ，并得到输入为。的输出a 。当输入串为( o1 ，o2 ，om 时，设6 ( q 0 ，oi ) = q l ，6 ( q l ，o2 ) = q 2 ，6 ( q i 一1 ，0i ) = q i ，6 ( q n 一1 ，on ) = q n 。这时输出序列为 ( q 0 ，o1 ) ( q l ，o2 ) ( q i ，0i + 1 ) ( q n i on ) 。m e a l y 机的输出和状态转换有关。常用来表述中间状态或过渡状态。2 4 扩展有限状态机2 4 1 传统状态机的不足我们研究的有限状态机本身有两点不足：1 ) 不能方便的模拟变量操作。2 ) 无法模拟任意值传递。状态机处理定义其上的抽象对象序列，既可以添加抽象对象到序列中，同时也可以从序列中取出它们。并且只有在访问这些序列时候，状态机才会被同步。我们对基本的有限状态机模型进行三点修改。首先，我 f 6 1 入一个额外的元素：变量。它与序列定义类似。变量由变量名和拥有的抽象对象组成。在这种情况下，抽象对象往往是整型值。它与真实的序列的主要差别在于变量每次都只能在其有限的取值范围内取一个值。任何个值都能被添加到变量中，但是只有最后一个被添加的值能被取出。第二个改变是序列只被用来转送整型值，而不是未定义的抽象对象。最后一个改变是引入了算术运算符和逻辑运算符来处理变量的内容。由于扩展变量的取值范围有限，对于有限f i f o 序列的有限状态机来说，并不会增加它的计算能力。一个有限取值范围的变量可以用一个有限状态机简单的模拟。2 4 2 扩展有限状态机基于有限状态机的】p 协议研究有限状态机基础如下给出相应扩展的有限状态机数学模型表示。一个e f s m 被定义为五元组m = ( q ，z ，6 ，q 0 ，f ，a ) ，其中，a 是一组交量名的集合；q ，6 ，q o ，f 定义不变1 2 , 5 9 】。在有限状态机中，迁移可描述为t = ( s ，d ，i ，o ) 。其中，s 是迁移t 的源状态，d 是迁移t 的目标状态，i 表示输入，o 表示迁移t 被引发时相应的输出。在扩展的有限状态机中，相应的迁移通常变为t = ( s ，d , i ，c ，a ) ，其中，s 是迁移t 的源状态；d 是迁移t 的目标状态：i 表示输入，且有可能有相应数据作为输入参数；c 表示迁移t 引发的条件；通常是一个与变量相关的关系或逻辑表达式；a 表示迁移被引发时执行的动作，这包含产生相应的输出或对变量值的修改。因此，数据变量集合a 的赋值情况对相应状态机的行为将产生直接的影响。这和普通的状态机是完全不同的。2 5 状态机的本质系统在不同阶段，其工作不同；且当其行为可以分成所谓有限的状态和不重叠的程序块时，系统就显现出状态行为。并不是所有的系统都会显现出状态行为，有些系统只表现出简单的行为。或者连续的行为与历史有关，但不能被合理的分成有限个数目的状态。f s m 是规定系统整体行为的约束的有效方法。处在某一个状态意味着系统只响应所有允许输入的一个子集，只产生可能响应的一个子集，并且改变状态也只是所有可能状态的一个子集。2 5 1 状态状态是系统生命期中的一种情况或条件。这期间，某些不变量( 通常是隐式的)维持着系统完成某些活动，或者系统等待某些外部事件。状态非常有效的抓住了系统历史的有关方面。状态能除去所有可能无关的事件序列，只捕获有关的事件序列。2 5 2 扩展状态每个状态代表所有的程序记忆装置的有效值的一个特殊集。对于只有少许基本变量的简单程学，此种解释也会导致天文数量的状态。所以，程序变量一般是与状态分离的。系统的所有条件( 称为扩展状态) 是定性方面、状态和定量方面及扩展状态变量的结合。有记忆的状态机叫做扩展状态机。2 5 3 监测器扩展状态机经常是不仅对基于定性的状态的激励反映，而且也对基于该状态的有关扩展变量的值起反应。我们引入监钡4 条件来表示动态估算扩展状态变量的值引出的布尔表达式。监测条件影响状态机的行为，开启或关闭某种操作( 如状态的改变) 。监测器的引入是对状态机形式方法加入记忆( 扩展状态变量) 的直接结果。少量的使用，监测器和扩展状态变量会形成具有惊人能力的机制，大大简化状态机的设计：但过量的使用，则监测器会破坏使用状态机本来的目的。因为使用状态机的目的是为了减少在代码中的条件分支数量以及降低在每个分支所要完成的测试的复杂性。监测器则重新引入扩展状态变量彝勺测试以及根据测试结果重新分支。监测器的滥用是基于状态机的设计中结构性衰退的主要机制。9基于有限状态机的i p 拂议研究+ 有限状态机基础2 5 4 事件事件是指对系统很重要的时间和空间的现象。常用来特指现象的类型。一个事件可以有相关参量，可以传递有关现象的定量信息。事件实例产生后，可以传递到一个或多个状态机。其生命周期分3 个阶段：首先，事件实例被接收，并等待处理；其次，事件实例被分发到状态机，成为现行事件；最后，状态机完成处理，被消耗。2 5 5 动作和转换当一个事件被分发时，状态及用完成动作来响应它。任何与现行事件有关的参量值对直接由该事件引起的所有动作都是有效的。从一个状态切换到另一格状态被称为状态转换，而引起状态转换的事件称为触发事件。在扩展状态机中，转换可有一个监测器。只有当监测器估值为t r u e 时，转换才能“启动”。相应于同一个触发，状态可能有多个转换，只要它们有不重叠的监测器。2 5 6 执行模型r t c实际上，执行动作总需时间完成，状态机因此在练歌模式之间变换：空闲监听下一个事件的到达；忙响应事件。当系统在忙于处理低优先级事件时，若高优先级事件到达，则模型会如何处理昵? 只有两种可能性：事件的抢先处理或非抢先处理。在抢先模型中，系统立即挂起低优先级事件，开始处理新的事件。在非抢先模型中，系统处理新事件前，把该新事件存储下来，直到前一个事件已完成处理。此种模式称为“运行到完成”( r t c ，r u nt oc o m p l e t e ) 。在r t c 模型中，系统以离散的、不可分割的r t c 步处理各事件。高优先级事件不能中断别的事件处理，完全避免了内部并发问题。在事件处理期间，系统处于不响应状态。r t c 并不意味着状态机在r t c 步骤完成之前必须独占处理器。在多任务环境下，与忙状态机的任务上下文无关( 没有相互共享变量，没有并发性危险)其他的状态机也可同时运行。状态机形式方法通常都认可r t c 执行语义法。r t c 处理的关键优点是简单化；缺点是在单个状态机情况下事件处理时问不能过长，以保持系统的较高的响应性。1 0基于有限状态机的i f 协议研究形式描述技术第3 章形式描述技术3 1 形式化描述技术概论形式描述语言以一种或多种数学方法为基础，具有严格的语法和语义定义，可以精确、完全地表述协议的功能、性能及行为等。形式描述语言为协议的分析、验证、实现、测试等的系统化和自动化提供了良好的基础。为了能准确地描述o s l ( 开放系统互连) 协议，o s i 的f d t ( 形式描述技术) 小组于2 0 世纪8 0 年代初便开始着手进行形式描述语言的开发研究。最初大约提出了2 0 多种方法，但大致可以归结为两类i 基于有限状态机语言类和基于代数方法语言类。e s t e l l e ( 一种扩充的有限状态机语言) 是前一类语言的典型代表。l o t o s 则是后一种语言的代表”1 。我们将重点介绍e s t e l l e 形式化描述语言。3 2e s t e l l e 形式描述语言口，8 “r ”“13 2 1e s t e l l e 形式描述语吉概述e s t e l l e 是基于扩展的有限状态机( e f s m ) ，是一种形式化、数学化，并且面向实现但又与具体实现相独立的描述技术。它具有良好的结构和定义，并且有很强的表达能力，可以完整、一致、简练，并且准确地描述分布、并行信息处理系统。e s t e l l e 是p a s c a l 语言的扩充。e s t e l l e 中的整数和实数与数学上所习惯使用的相一致，但对实现细节不进行考虑，比如整数可达到的最大值、实数的精度等。e s t e l l e 中的函数同样也允许返回任意类型的值。e s t e l l e 中去除了p a s c a l 中的所有与i o 操作相关的特征。最后，p a s c a l 中的关键字p r o g r a m 在e s t e l l e 中被s p e c i f i c a t i o n 所取代。形式描述语言e s t e l l e 有如下基本特点：( 1 ) 基于扩展的有限状态机( e f s m ) ，专为描述协议而设计：( 2 ) e s t e l l e 是p a s c a l 语言的扩充。用e s t e l l e 描述的协议容易转换成p a s c a l或c 代码，因此它是一种面向协议实现的形式描述语言( f d l ) ：( 3 ) 模块实例可通过初始化语句动态产生。如果协议实现后模块实例对应于一个进程或任务。那么网络进程或任务也是动态产生的：( 4 ) 模块之间的通信方式为异步通信；可以扩展描述同步通信；( 5 ) e s t e l l e 对并发、不确定性、超时、异步通信状态转换有较强的表达能力，但对递归、共享通道( 广播通道) 、同步通信、协议性质( 如不变性等) 的表示尚缺乏有力的手段；( 6 ) 从e s t e l l e 描述中易于提取出协议的f s m 模型或p e t r i 网模型，但不容易提取t l 或c c s 模型。用e s t e l l e 来描述一个协议，最重要的工作就是构造协议的模块结构和通信基于有限状态机的i p 协议研究形式描述技术机制，主要包括：系统中模块的层次构成、模块的类别、通道和交互点的定义、交互点队列的属性，以及模块和通道之间的连接等。3 2 2 相关概念在e s t e l l e 中，一个系统被理解成是由许多相互通信的模块( m o d u l e ) 分层嵌套而构成的，模块之间通过通道( c h a n n e l ) 进行通信，即通道将一个模块的输出与另一个模块的输入队列连接起来。通道和模块之间的连接点称为交互点( i n t e r a c t i o np o i n t s ) 。模块间的信息传递称为交互( i n t e r a c t i o n s ) 。每个模块内部相当于一个有限状态机，有限状态机的每个迁移或转换都由某些输入所触发，状态迁移过程中可能会产生输出。这里的输入对应于模块所收到的消息，而输出的则对应于模块向其它模块所发送的消息。模块( m o d u l e s ) e s t l l e 将一个系统看成是由于许多相互通信的模块分层嵌套而构成的系统。每个父模块控制对其予模块的创建和销毁，系统的每一级可有多个模块，每个模块可通过通道以异步方式与其它模块通信。模块实倒( m o d u l ei n s t a n c e s ) e s t e l l e 所定义的一个模块体，在协议运行过程中可同时生成一个或多个模块实例，模块实例可动态产生和撤销。不同模块实例用模块变量( m o d e lv a r i a b l e s ) 来标识。在e s t e l l e 协议规格中，模块实例的生成部分包括在规格主体( m a i nb o d ie s ) 中。模块特性( m o d u l ea t t r i b u t e ) 按照模块体内有无转换部分来划分。模块分为；非活跃模块( i n a c t i v em o d u l e s ) 、活跃模块( a c t i v em o d u l e s ) 和特征模块( a t t r i b u t e dm o d u l e s ) 。其中，摸块体内无状态转换部分的模块称为非活动模块，初始化非活动模块所产生的模块实例也是非活跃的。模块体内包括状态转换部分的模块称为活跃模块。在对模块进行定义时，如果一个模块头有多个模块体与之关联，并且至少有一个模块体内包含状态转换部分，则将这种模块称为特征模块。模块类别( m o d u l ec l a s s e s ) 模块类别指明了模块的工作方式。模块类别可以是系统进程模块( s y s t e m p r o c e s s ) 、系统活动模块( $ y s t e m a c t i v i t y ) 、进程模块( p r o c e s s ) 以及活动模块( a c t i v i t y ) 。它们的定义描述如下：系统进程模块( s y s t e m p r o c e s s ) 箕本身可以是特征模块，但它的父模块必须为非特征模块，并且必须也是系统进程模块。它的子模块可以是任何类别的模块。系统进程模块的工作方式是：父模块优先于子模块，兄弟模块并行。系统活动模块( s y s t e m s c t i v i t y )其本身可以是特征模块，但它的父模块必须为非特征模块，并且必须是s y s t e m p r o c e s s 或s y s t e m a c t i v i t y 。它的子模块必须是活动模块。系统活动模块的工作方式是：父模块优先于子模块，兄弟模块串行执行( 选择是随意的)迸程模块( p r o c e s s )它必须为特征模块，它的子模块不能为s y s t e m p r o c e s s和s y s t e m a c t i v i t y ，只能为p r o c e s s 。它的工作方式于s y s t e m p r o c e s s 的工作方式相同。活动模块( a c t i v i t y ) 它必须为特征模块，它的子模块不能为s y s t e m p r o c e s s和s y s t e m a c tj v i t y ，只能为a c t i v i t y 。它的工作方式与s y s t e m a c t i v i t y 的工作方式相同。模块嵌套规则( m o d u l en e s t i n ge u 2 e s ) 根据上面对模块类别的讨论，我们可得如下模块嵌套的规则：系统模块的父模块必须为非特征模块；基于有限状态机的i p 协议研究 形式描述技术特征系统模块的子模块必须为特征模块；菲系统模块的子模块不能为系统模块：同一级可以有多个系统模块：s y s t e m p r o c e s s 的子模块可以是p r o c e s s 或a c t i v i t ys y s t e m a e t i v i t y 的子模块为a c t i v i t y ；p r o c e s s 的予模块必须为p r o c e s s ：a c t i v i t y 的子模块必须为a c t i v “y ；非活动模块头定义可以不指明“模块类型”。通道( c h a n n e l ) e s t e l l e 的各模块之间通过通道进行通信。通道的定义包括通道名、通信角色和各个通信角色恕通道旌加交互信息共三个部分。一般情况下，一个通道只有两个通信角色( 即两端各一个) 。在通道定义中需要给出各个角色向通道发出什么交互信息，以及各个交互所附带的参数。交互点( i n t e r a c i o np o i n t s ) 模块与通道之间的连接点称为交互点。一个通道定义两个通信角色，这并不意味着只能有两个模块使用一个通道。多个模块可扮演同一个通信角色并使用同一个通道。一个模块必须定义一个交互点之后才能将自己与一个通道联系起来。如果一个模块要使用父模块定义的通道，它必须在模块头定义中给出交互点定义，这种交互点称为外部交互点。丽如果一个模块要使用它自己定义的通道，那么它必须在模块定义中给出交互点定义，这种交互点称为内部交互点。交互点称为i p ，在e s t e l l e 规格中，交互点的定义用i p 作为关键词。交互点的约束( i pb i n d i n g ) 在模块定义了交互点之后，一个独立的交互点还不存在通信能力，只有当两个以上的交互点约束( b i n d ) 在一起时一个交互点的输入事件才能作为输出事件传递到另一个交互点。在e s t e l l e 中，通过c o n n e c t语句或a t t a c h 语句将交互点约束在一起，反之则通过d i s c o n n e c t 和d e 协c h 语句来解除交互点的约束。：连接端点( c o c c e c t i o ne n d p o i n t s ) 多个i p 利用多条c o n n e c t 语句和a t t a c h语旬串行约束在一起可形成一条连接( c o n n e c t ) ，连接两端的i p 称为连接端点。连接具有如下的特征：即进入一个连接端点的输入事件将自动传递到另一端的连接端点的队列中，中间i p 的队列则隐藏起来。i p 队列( i pq u e u e ) 前面已经提到，模块之间通过通道进行通信时，通道将一个模块的输出与另个模块的输入队列连接了起来，该输入队列也就是j p 的队列。在定义i p 时，必须指明i p 的队列性质：c o i h n o nq u e u e 或i n d i v i d u a lq u e u e 。在多个模块使用同个通道时，它们可使用自己的单独队列，也可以荚享队列，默认为i n d i v i d u a lq u e u e 。输入和输出( i n p u ta n do u t p u t ) 在e s t e l l e 中，w h e n 语句从i p 读入个事件，而o u t p u t 语句往i p 输出一个事件。格式为：w h e ni p m ( a r q u m e n t s )o u t p u ti p i 1 1 ( a r q u m