（测试计量技术及仪器专业论文）协议形式化技术的应用研究.pdf

南京邮电大学硕士研究生学位论文摘要 摘要 协议工程就是一体化、形式化的协议开发过程。协议工程的目的是用来减少协议开发 中潜在的错误，提高协议开发的效率，促进标准化的发展。协议的形式化理论是协议工程 的核心。它运用形式化方法进行协议工程学的研究，研究内容包括：协议分析、协议设计、 协议描述、协议验证、协议实现和协议测试的理论和方法。协议形式化描述是协议实现和 协议测试的重要前提，协议验证保证协议设计的正确性和完整性，协议测试是保证协议实 现满足协议规范的重要手段。 本文以协议工程的理论为依据，并以a b 协议为研究对象，首先从协议分析开始，研究 了协议分析技术，并且对协议的上层用户及底层用户的环境要求进行了讨论分析；然后根 据有限状态机的理论基础，研究了a b 协议的有限状态机模型，并根据该模型通过s d l 技 术实现了对协议的描述和仿真；最后，进一步研究了协议验证的相关概念，本文讨论了几 种验证方法，并对其中的一种方法提出改进，在此基础上采用改进的方法对a b 协议的状 态机模型进行了验证。通过验证结果的对比，显示了改进方法的优越性。 主题词：协议工程；形式化技术；协议描述；协议验证；有限状态机； s d l 南京邮电大学硕士研究生学位论文 a b s t r a c t a b s t r a c t p r o t o c o le n g i n e e ri st h ep r o c e s so fi n t e g r a t i v ed e v e l o p m e n ta n df o r m a ld e v e l o p m e n t p r o t o c o le n g i n e e ri st od e c r e a s et h ep o t e n t i a le r r o r s ，t oi n c r e a s et h ee f f i c i e n c yo fe m p o l d e r , t o a d v a n c et h ed e v e l o p m e n to fs t a n d a r d i z a t i o n 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 f t 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 gt h ef o r m a ld e s c r i p t i o nt e c h n i q u e si np r o t o c o le n g i n e e r i n g ， t h er 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 st h e p r o t o c o la n a l y s e ，p r o t o c o ld e s i g 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 lt e s t i n g a n dp r o t o c o li 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 i s c r i p t i o n si st h em o s ti m p o r t a n ts t e po fp 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 lv a l i d a t i o na s s u r e st h ec o r r e c t n e s sa n dc o m p l e t i o no fp r o t o c 0 1 p r o t o c o l t e s t i n gi sa ni m p o r t a n tm e t h o dt oc h e c kt h ep r o t o c o li m p l e m e n t a t i o ns a t i s f i e dw i t ht h ep r o t o c o l f o r m a ls p e c i f i c a t i o n t h i sp a p e rb a s e so nt h et h e r yo fp r o t o c o le n g i n e e r b yr e s e a r c h i n ga bp r o t o c o l ，t h ep a p e r a n a l y z e st h ep r o t o c o l ，s t u d i e st h eu p p e ru s e ra n dl o w e ru s e r sr e q u e s to fe n v i r o n m e n t b a s e do n f s m ，t h ep a p e re d u c e dt h em o d e lo ff s ma b o u ta bp r o t o c 0 1 u s i n gt h em o d e la n dt h et e c h n i q u e o fs d l ，i ti se a s yt os p e c i f i c a t ea n ds i m u l a t et h ep r o t o c 0 1 w i t ht h ew o r kt h a th a sb e e nd o n e ，t h e r ea r ef u r t h e rs t u d i e so nt h ec o r r e l a t i v ec o n c e p t s b y d i s c u s s i n gt h em e t h o d st ov a l i d a t et h er e s u l t ，o n eo ft h em e t h o d si sf u r t h e ri m p r o v e d w i t ht h i s i m p r o v e dm e t h o d ，t h ef s ma b o u ta bp r o t o c o li sv a l i d a t e d t h ea d v a n t a g eo ft h em e t h o di s r e v e a l e da f t e rt h ec o m p a r a t i o no ft h ev a l i d a t a t i o nr e s u l t k e y w o r d s ：p r o t o c o le n g i n e e r ；f o r m a lt e c h n i q u e ；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 ；f i n i t es t a t em a c h i n e ；s d l i i 南京邮电大学学位论文独创性声明 本人声明所呈交的学位论文是我个人在导师指导下进行的研究 工作及取得的研究成果。尽我所知，除了文中特别加以标注和致谢的 地方外，论文中不包含其他人已经发表或撰写过的研究成果，也不包 含为获得南京邮电大学或其它教育机构的学位或证书而使用过的材 料。与我一同工作的同志对本研究所做的任何贡献均已在论文中作了 明确的说明并表示了谢意。 研究生签名：难日期：卫牡 南京邮电大学学位论文使用授权声明 南京邮电大学、中国科学技术信息研究所、国家图书馆有权保留 本人所送交学位论文的复印件和电子文档，可以采用影印、缩印或其 他复制手段保存论文。本人电子文档的内容和纸质论文的内容相一 致。除在保密期内的保密论文外，允许论文被查阅和借阅，可以公布 ( 包括刊登) 论文的全部或部分内容。论文的公布( 包括刊登) 授权 南京邮电大学研究生部办理。 研究生签名：平导师签名： 南京邮电大学硕士研究生学位论文第一章绪论 第一章绪论 1 1 论文背景 协议是多个参与者为了完成某个特定的任务，所进行的交互动作和交互信息。所有合 法的参与方( 或实体) 都严格遵从交互动作序列的顺序，在前一步动作没有执行完毕之前， 后面的动作不能执行，只有当所有的动作序列都完成了，协议的目的及所需完成的特定任 务才算完成。协议的三要素：语法、语义、规则。 协议在人类社会和日常生活中经常用到。在通信世界中，协议是通信设备之间或通信 设备与其他设备之间用来通信的规则或语言。 如果从系统相互作用的概念来描述协议的定义，则可以这样来定义协议：对于n 层全 局系统，局部系统之间的相互作用的规则以及他们与外部环境和通道系统相互作用的规则 的总和就是n 层协议。 通信协议是计算机网络和分布式系统中两个或多个实体间相互通信时所必须遵守规则 的集合，是计算机网络的重要组成部分。通信协议是网络能否可靠通信的决定因素。近年 来，随着计算机网络的迅速发展，计算机网络越来越复杂化、大规模化、多样化，新型通 信技术和各类分布式应用纷纷涌现。这意味着协议本身的复杂性。系统的复杂性不但意味 着协议开发的难度加大，而且开发周期长，潜在的错误多。协议开发中的任何一点错误和 缺陷都会给系统的稳定性、可靠性、坚固性、安全性及互通性和互操作性等带来巨大的隐 患。协议的开发过程急需工程化，以便减少协议开发中潜在的错误，提高协议的开发效率， 促进标准化的协议实现。为适应这种形势，一门新的计算机学科协议工程产生了，它 涉及到计算机科学与工程的各个分支。 协议工程是指一体化、形式化的协议开发过程，旨在为协议软件的研制和开发提供一 套工程规范，使不同的人员可以以同一规范进行交流和协作，实现协议软件生产的规范化、 工程化、自动化。协议工程包括协议分析技术、协议的模型技术、协议形式描述技术、协 议验证、协议实现和协议测试等多方面的理论和技术。其中最为关键的是形式化技术，它 是协议工程各个阶段在技术上的衔接纽带，对协议工程的发展起决定性作用。本文将对协 议工程的多种技术作相应的分析和研究，并通过ab 协议为研究对象贯穿始终，每一章节 都有应用于a b 协议的实例，实现了对协议工程的相关理论的应用。对于研究协议工程理 论来说，具有一定的连贯性，有一定的应用价值。 1 2 论文结构 南京邮电大学硕士研究生学位论文 第一章绪论 本文的组织结构如下： 第一章绪论，阐述了协议工程的定义，并对协议工程的一些技术做了简要的介绍。 第二章协议分析技术，分析了构造协议所需涉及的内容，如用户要求、通道性质等。 并对协议的元素进行了相应的讨论，在本章节中以一个具体的协议实例为应用对象，对协 议分析技术做了进一步的研究。 第三章协议模型技术，主要讨论了几种状态机模型，如有限状态机，扩展有限状态机， m o o r e 机，m e a l y 机等。本章节中还研究了状态机与协议的关系，并且通过对状态机的模 型技术的分析，描述了一个具体协议实例的的f s m 模型。 第四章协议形式化描述语言，本章节讨论了几种形式化描述语言，其中主要研究了s d l 形式化描述语言，并且基于t a u 平台上利用s d l 语言技术在实现了对a b 协议的描述仿真。 第五章协议验证技术，形式化验证技术比较多，本章节主要研究了可达性验证技术， 并且在现有技术的基础上，提出了种新的改进技术。还通过改进的方法实现了对a b 协 议状态机的验证，在此基础上阐述了改进方法的优越性。 第六章总结，总结了全文的研究内容。 2 南京邮电大学硕士研究生学位论文第二章协议分析技术 2 1 简介 第二章协议分析技术 一般来讲分析协议包括两种技术：开发一个新的协议和实现具体的协议。对于第一种 含义，开发新的协议，其目标是形成新的协议文本，重点是说明本协议应该具有什么功能， 制定相关的协议元素，形成协议文本，构造一个新的协议。但是从应用角度来看，实现具 体协议的需求大于开发新的协议的需求，所以本文将重点研究实现具体协议的过程。在后 续章节中，除非特别说明，“开发协议 均指实现具体协议。 对于实现具体的协议，其目的就是生成一个软件系统，该软件系统可以实现具体协议 的全部功能或一个功能子集，重点是说明如何实现协议功能。其协议开发过程包括： 口协议分析，包括协议环境分析和协议功能分析。 口协议设计，包括协议机制设计、协议元素设计及协议组织设计。 协议建模阶段，用模型技术来设计一个协议。 协议描述，用一种形式化语言来描述设计结果，包括软件系统结构、模块划分、系 统行为实现细节等。 协议验证，在开发环境下仿真运行协议软件，验证协议的正确性。 协议实现，用某种编程语言实现协议软件系统( 自动生成代码或手工编码) 。 口协议测试，在目标环境下测试协议软件系统。 协议维护，在协议软件的使用过程中不断完善系统。 2 2 通信协议结构 协议系统能够提供大量不同的网络服务。为了应付大型、复杂的网络系统，协议系统 被划分成多个小型的子系统，通常被称为协议层或协议实体。不同的功能被划分到不同的 协议层当中，且不同的功能分开执行。相对于把所有的实体看作一个实体，具有很多优点。 首先一个实体用来应付一个问题，或一个相关问题的集合。所有的实体通过定义好的接口 界面互相联接。这些实体组成了通信协议，通常称作为协议栈。 根据规范说明每个实体必须和同层的协议及相连的实体进行通信，因此这些实体需要 具备相应的界面接口，该接口是用来和同层的协议实体交互信息的，存储在界面接口的数 据方便了定义协议信息和协议行为。在协议工程中，一个接口有两个消息集合：发送消息 集合和接收消息集合。服务接口对应于o s i 的服务访问点( s e r v i c ea c c e s sp o i n t ) ，简 3 南京邮电大学硕士研究生学位论文 第二章协议分析技术 称s a p 。通过对多个现有协议执行的研究，发现协议的执行包括图2 2 1 所示的内容。 图2 2 1 协议结构图 图2 2 1 中在不同的协议栈中包括了四个协议实体。协议实体之间的通信以不同步的方 式进行通信。协议栈之间通过网络的物理连接连接在一起。同一栈中的实体通过消息路径 互相连接。同层的协议实体通过虚消息路径进行连接。消息发送到同一层中，是利用了底 层实体提供的帮助来实现的，因此同层之间的通信是虚通信。 国际标准化组织( i s o ) 定义的开放式互连系统参考模型是一个被人们广泛接受的计算 机模型，该模型称为o s i 模型。o s i 模型把计算机网络协议分成了七层，t c p i p 协议栈把网 络协议分成四层。这里的协议分层是指把n 层协议再分成两个或多个子层，然后再分层设 计。分层的原则是，与用户接口的协议实体和与下层通道接口的协议实体在功能上相互独 立，而且各自的功能都比较复杂。通过划分子层，可以使复杂协议的结构变得清晰，有利 于协议的设计、验证、实现和测试。但划分子层后，由于增加了子层间的通信，协议效率 会受到一些影响。因此当用户对协议的效率要求很高时，应尽可能避免划分子层。协议分 层的例子如数据链路层协议，通常，数据链路层协议都再分成逻辑链路控制( l l c ) 和媒 体访问控制( m a c ) 两个子层。 0 s i 模型在功能上将计算机网络分成七层： 4 一一一一一一一园一同uo 南京邮电大学硕士研究生学位论文第二章协议分析技术 图2 2 2o s i 七层结构 其中1 3 层又称为低层功能，4 - 7 层称为高层功能。这样低层功能是保证 系统之间可靠信息传递，高层功能是一些面向应用的信息处理和通 l 信o 2 3 协议环境分析 无论是设计开发一个新的协议，还是设计实现一个具体协议，都需要从协议的环境分 析入手，只有了解了协议的环境，才能明确协议的功能，协议设计才能进行。协议分析包 括两大部分，协议环境分析和协议功能分析。 为了研究协议环境，必须先建立一个协议模型，如图2 3 1 中n 层协议模型。( n ) 层可 有多个协议实体( a 和b 是其中两个) ，它们怎样分布，各起什么作用等，属于协议工作 模式问题。u s e r l 和u s e r 2 为( n + 1 ) 层协议实体，称之为第n 层协议的用户( 简称( n ) 层 用户) 。( r 1 ) 层协议实体利用( n 1 ) 层协议提供的服务通讯，这种通讯活动在两个( n i ) s a p ( 服 务访问点) 之间构成一个通道，称之为( n 1 ) 层通道。( n ) 层用户的要求、( n 1 ) 层通道的性质 以及( n ) 层协议的工作模式构成( n ) 层协议的环境。 ( n + 1 ) 层 ! 一一 ( n ) 层 - - 。_ - - - - ( n 1 ) 层 ( n ) 层通道 图2 3 1 ( n ) 层协议模型 在这里( n ) 层协议和( n ) 层协议实体( 协议机) ，( n ) 层用户和( n + 1 ) 层协议实体，以及( n - 1 ) 5 堕塞坚皇奎兰堡主翌壅竺堂垡丝茎蔓三皇塑望坌堑垫查 层通道和( n 1 ) 层服务将混用，不作严格区分。 2 3 1 用户要求 n 层用户对n 层协议要求提供的服务可以归纳为以下几个方面： 1 连接管理 ( n ) 层用户可以要求( n ) 层协议提供有连接服务、无连接服务和永久连接服务。并要求( n ) 层协议负责连接的建立、撤消、作废、复位、恢复等管理工作。连接建立过程中，网络资 源的分配和管理，连接合法性和安全性检查，以及目标名地址的转换工作也由( n ) 层协议来 完成。 2 广播与组播 广播是指一个( n ) 层用户发出的数据报，在同一个网络中的其他用户都能够接收到。组 播是指一个或多个( n ) 层用户发出的数据报，在网络中有一组用户可以接收到该数据报，每 个用户可以加入或退出该组。 3 服务认可方式 n 层用户通过服务原语得到( n ) 层协议提供的服务，服务原语的交换时序称为服务认可 方式。可以有三种形式服务认可方式：完全认可式、部分认可式、无认可式。 完全认可式服务需要4 条服务原语： - r e q u e s t ( 请求) i n d i c a t i o n ( 指示) r e s p o n s e ( 响应) c o n f n t n ( 证实) 部分认可式服务需3 条服务原语： r e q u e s t i n d i c a t i o n - c o n f i r m 无认可式服务只需要2 条服务原语： - r e q u e s t i n d i c a t i o n 图2 3 2 给出了三种服务认可方式下服务原语的时序关系。在部分认可式服务中c o n f i r m 可发f l ( n ) 层协议的任何一个地方。如果( n ) 层用户需要进行应答式通讯，就要求完全认可式 服务，但在这种服务认可方式下通信效率较低。无认可式和部分认可式服务可使( n ) 层用户 6 南京邮电大学硕士研究生学位论文第二章协议分析技术 进行异步通讯，获得较高的通讯流量。 ( n + 1 ) 层 i ( n ) 层 ( n + 1 ) 层 二一一 ( n ) 层 ( n + 1 ) 层 i 一一 ( n ) 层 数据指示、数据响应 完全认可方式 n ) - s a p 部分认可方式 n ) - s a p n ) - s a p 尢认司万式 图2 3 2 三种认可方式原语时序 4 通讯方式 用户通讯方式涉及单工半双工全双工，以及同步异步两个方面。 所谓单工通讯方式是指在通讯过程中，只允许一方用户向另一方用户发送数据报文。 所谓半双工通讯方式是指在通讯过程中，通信双方都可以向对方发送数据报文，但在 某一时刻只允许一方向另一方发送数据报文，在这种方式下，n 层协议需要管理“发信权 ， 只有得到“发信权 的用户可以向对方发送数据报文。 所谓全双工通讯方式是指在通讯过程中，通信双方可以同时向对方发送数据报文，这 就要求( n ) 层协议必须在( n ) s a p 上提供并发的收发服务。 所谓同步通讯方式是指( n ) 层用户之间进行应答式通讯。发送方发出数据报文后，要得 到对方的应答数据报文才会发送下一个数据报文。如果采用同步通讯方式，( n ) 层协议可以 免除流控制功能。( n ) 层用户的同步通讯可以通过( n ) 层协议提供的完全认可式服务进行，也 可以由用户自己进行控制。 所谓异步通讯方式是指发送数据的用户可向收方用户发出任意个数据报文，不需要对 方对每个数据报文做出应答。在这种通讯方式下，n 层协议必须施加流控制，否则报文可 7 雨京邮电大学碘士研冗生字位论文第二覃协议分析技术 能丢失。 5 数据形式 用户数据可以有多种形式，它们可能是： 块数据，( n ) 层用户向( n ) 层协议递交整块数据； 流数据，( n ) 层用户向( n ) 层协议递交字符流； 批数据，( n ) 层用户向( n ) 层协议递交大批数据块( 短时间内) ； 优先数据，( r 1 ) 层用户向( n ) 层协议递交的数据有不同优先级别： 中断数据，( n ) 层用户要求( n ) 层协议旁路正常数据的传递，快速将特殊信息发送到对 方，此信息叫中断数据； 紧急数据，同中断数据； 流外信息，( n ) 层用户向n 层协议递交的流数据中夹杂着要求n 层协议截获并作处理 的信息，这种信息称为流外( o u t - o f - b a n d ) 信息： 编码信息，( n ) 层用户要求( n ) 层协议先进行信息编码，然后发送。 6 数据长度 ( n ) 层用户要求传送的块数据的长度以及批数据的数据量可能是任意的。如果数据块过 长，( n ) 层协议需要分段发送。为了应付大量批数据的传送，( n ) 层协议要加宽( n - 1 ) 层通道的 带宽，要进行流量控制和拥塞避免控制，要有足够的数据缓冲区。 7 服务质量( q o s ) 要求 服务质量要求主要包括三个方面，即安全性要求、可靠性要求和性能要求。 8 目标识别 ( n ) 层用户可以以三种形式向( n ) 层协议说明自己的通讯目标： 传地址，说明目标地址； 传名字，说明目标名字； 传参照值( 索引值) ，说明目标的参照( 索引) 值。 ( n ) 层协议必须维持和管理一个地址名字表或地址索引表。 9 其它用户要求 n 层用户的其它可能的要求包括测试、监视、统计、记帐等 2 3 2 通道性质 ( n ) 层中任何两个协议实体通过( n 一1 ) s a p 所形成的数据逻辑通路叫( n 1 ) 层通道。( n ) 层协 议使用的( n 1 ) 层通道的性质对( n ) 层协议的功能是有影响的，这些通道性质可归纳为以下几 8 南京邮电大学硕士研究生学位论文 第二章协议分析技术 个方面： 1 通道形成方式 ( n ) 层协议实体a 和实体b 可用下述三种方法形成( n 1 ) 层通道： ( a ) a 和b 建立并独占条连接，此时( n - 1 ) 层应提供有连接服务，如图2 3 3 ( a ) 所示。 独占通道 图2 3 3 ( a ) 独占连接 ( b ) a 和b 和其它协议实体一起共享一条连接，如图2 3 3 ( b ) 所示。 共享通道 图2 3 3 0 ) 共享连接 ( c ) a 和b 利用( n 一1 ) 层提供的无连接服务进行通讯，如图2 3 3 ( c ) 所示。 圈囡回回 奉奉 ：!：3：!：乡。 无连接通道 图2 3 3 ( c ) 无连接 如果( n 1 ) 层为物理层，a 和b 可独占一条物理信道，或共享一条物理信道。 ( n ) 层协议必须有一个专门负责管理( n 1 ) 层服务访问点接口的模块，该模块的功能取决 于通道形成方式。该模块要负责连接的建立和连接共享控制工作。如果是物理信道，要负 责信道接lit 作及信道共享控制工作。 2 队列性质 一般情况下，( n 1 ) 层通道可看作队列通道，就是说一个数据报文从( n ) 层源端协议实体 发出之后要在( n ) 层以下各层多次存贮转发，每个存贮转发处就存在一个队列。平均队列长 度以及最大队列允许长度是队列的主要性质。平均队列长度影响数据报文的传输时延，平 均队列长度越长，传输时延就越大。而最大队列长度则反映通道承载突发数据的能力，队 列越长，通道的缓冲容量就越大，承载突发数据的能力也就越强。如果队列实际长度达到 最大允许长度，那么后续的数据报文将会丢失。如果( n 1 ) 层通道为物理信道，那么此通道 9 堕塞塑皇奎兰婴主塑茎竺堂垡堡苎 塑三兰堡坚坌堑茎查 有时是非队列性质的。此时数据报文在通道中的时延是固定的，报文不会丢失，并且是有 序的。 3 r t t ( 往返时间) i 册( r o u n dt r i pt i m e ) 定义为报文从( n ) 层源端实体发出到该报文的认可信息回到该 实体所花费的时间。它包括报文从源端实体传送到目标实体所需时间、目标实体收到报文 之后，对报文进行处理然后发出认可信息的时问以及认可报文的传送时间。l m 是( n ) 层协 议的最重要参数之一。 4 数据的可靠性 数据在通道中传送的可靠性包括报文的出错率、报文丢失率、报文重复率、报文顺序 错误率。通道的形成方式与数据可靠性有一定关系。如果通道是利用( n 1 ) 层有连接服务形 成的，或是物理信道，那么报文的传递顺序不会改变。如果通道是利用( n - 1 ) 层的无连接服 务形成，报文的传递顺序就不能保障了。 5 通道可靠性 1 1 层通道可靠性指通道故障( 如断连、复位等) 的发生概率。 6 报文最大长度 通道所接收的最大报文长度，该参数影响( n ) 层协议的报文分割，拼接等功能的施行。 7 工作方式 通道工作方式涉及单t 半双工全双工，以及同步异步两个方面。( n ) 层协议将根据工 作方式提高通道利用率。 2 3 3 工作模式 n 层协议的工作模式涉及如下一些问题。 1 点一点模式和多点模式 ( n ) 层内任意两个协议实体( 如a 和b ) 利用一条( n - 1 ) 层通道通讯，协同完成指定协议 功能。此模式称为点点模式。而两个以上协议实体利用多条通道相互通讯，协同执行 一定任务，此模式称为多点模式。图2 - 3 4 所示为点点模式和多点模式的例子。 1 0 南京邮电大学硕士研究生学位论文第二章协议分析技术 n 层协议 ( n + 1 ) 层 ( n ) 层协议 ( n 一1 ) 层 点一点模式 多点模式 图2 3 4 点一点模式和多点模式 2 主从模式和平衡模式 在点点模式或多点模式中，如果一个协议实体为主控实体，其它实体受主控实体 控制( 称为从实体) ，则此模式为主从模式；如果各协议实体的作用和功能是近似的，控 制上是自治的，则此模式为平衡模式。 3 中转和路由 有时r t 层内两个协议实体不能找到或形成直接通道，此时它们的通讯必须通过中转实 体进行( 如图2 3 5 ) 。如果在( n ) 层内存在多个中转实体，这些中转实体形成一个逻辑网络， 这时就要求每个中转实体要有路由功能。中转实体可以不直接向( n ) 层用户提供服务( 如图 2 3 5 中的实体w ) 。 南京邮电大学硕士研究生学位论文第二章协议分析技术 ( n 一1 ) 层服务不同 w 和r 协议小同 图2 3 5 中转实体 2 4 协议功能分析 完成协议环境分析后，基本上就可以明确协议应该具有哪些功能了。协议功能分析就 是明确协议应该具有的功能。这里要讨论的协议功能是针对整个计算机网络而言，可以具 体到某一层，其协议功能只是这些功能的子集。 1 连接控制管理 该功能负责用户之间连接的建立、维护及释放的管理工作。该功能还包括连接的合法 性检查，密钥交换，q o s 协商，资源分配与回收，连接目标名与地址的翻译等工作。 2 通讯方式管理 对于半双工通讯，( n ) 层协议要进行“发信权管理；对于全双工通讯，( n ) 层协议要 求的其用户能在任意时刻递交s d u 和接收s d u ，具有并发的收发功能。 3 数据发送接收管理 层用户与( n ) 层协议之间传递的数据称为服务数据单元( s d u ) 。而层协议实体之 间传递的数据称为协议数据单元( p d u ) ，数据发送接收管理功能就是要把用户提交的s d u 以p d u 的形式，通过下层通道发送到对端协议实体。在接收端再将p d u 还原成s d u 送 给收端用户。 2 5 协议元素 一般来说，协议由六种元素组成，这六种元素是： l 服务原语和服务原语时序 1 2 堕塞堕皇奎兰堡主堕壅竺兰垡笙茎 箜三兰堡坚坌堑垫查 服务原语是协议与用户的接口( 即服务访问点s a p ) ，用户通过服务原语得到协议提 供的服务。协议实体通过服务原语得到用户的服务要求和返回结果。服务原语主要有四种： 请求、指示、响应和证实。每条服务原语可以带若干参数，通过不同的参数来定义不同的 服务要求。服务原语时序取决于用户要求的服务认可方式，第二章中图2 3 2 给出了三种 服务认可方式下服务原语的时序关系。 2 p d u 格式和p d u 交换时序 对等协议实体之间交换信息均以p d u 为单位，p d u 格式严格定义了信息的内容和含 义，p d u 的格式一般用a s n 1 语言来定义。在设计协议时，除了要定义p d u 格式外，还 必须定义p d u 的交换时序，即规定一方收到某个p d u 后应该回什么p d u 或可以回哪些 p d u 。p d u 的交换时序必须包括正常情况和各种异常情况。m s c ( 消息顺序图) 可以用来 描述各种情况下的p d u 交换时序。 3 协议状态 协议状态分为局部状态和全局状态。局部状态为单个协议实体在某时刻的执行状况， 全局状态为参与执行某种协议功能的所有协议实体状态之总和。 4 协议事件 协议事件分为输入事件和输出事件两大类。协议事件就是协议的输入，协议的输入包 括三个部分：来自本方用户的服务原语，来自对方协议实体的p d u 以及来自内部的定时 器信号( 超时) 。 5 协议变量 协议中用到的各种变量都可以称为协议变量。与其它软件一样，协议软件中的变量也 分全局变量、局部变量和临时变量。设计协议变量时，一般只设计全局变量和局部变量， 临时变量可以在设计和实现过程中根据需要随时添加。设计协议变量就是给出变量名称、 变量的数据类型以及变量的取值范围等。变量名的取名应尽可能与其用途一致。 6 协议行动和谓词 协议动作是指协议在状态转换( 迁移) 过程中执行的操作，协议从一个状态迁移到另 一个状态的过程称为协议过程，协议功能一般通过执行一组协议过程来实现，协议过程由 协议事件驱动，被驱动的过程执行一系列操作，这些操作包括： 输出信息( s d u 和p d u ) 设置定时器( 开始计时) 复位定时器( 停止计时) 修改协议变量 1 3 南京邮电大学硕士研究生学位论文第二章协议分析技术 改变协议状态 执行一系列动作( 操作) 的过程( 函数) 其它操作( 如读、写文件等) 在有些情况下，协议过程中一些协议动作的执行是有条件的，描述这些约束条件的语 句称为谓词。谓词一般用布尔表达式来表示。 2 6 协议分析技术应用实例 2 6 1 协议介绍 这里以a b 协议为例来实现协议分析的过程。a b 协议的应用比较广泛，作为协议分析。 a b 协议是最早的端到端通信协议之一，是大多数协议分析的雏形，具备了协议分析典型 性质，因此本文中就以a b 协议作为研究对象。其框图见图2 4 ，它包括发送放s e n d e r 和 接收方r e c e i v e r ，这两个实体通过通道c h a n e l 进行通讯。 s u s e r r u s e r 图2 4 1a b 协议系统 首先给出如下假设：( i ) a b 协议所使用的通道为永不会断路的全双工通道； ( i i ) 报文在通道中可能丢失，报文内容可能有错，但是重复发送一个报文n 次，至少有次是 正确的；( i i i ) 认可报文不会丢失，不会出错，不会重复。 发方：发方协议实体从发方用户获取个报文，将序号寄存器之值赋给报文，然后向 收方协议实体发出报文。报文发出之后启动超时时钟，等待认可报文。如果在给定时间内 未收到认可报文，重发报文。如果收到认可报文，其序号值与发出报文序号值相同，序号 寄存器的内容按模2 加l 。然后发方实体从发方用户获取下个报文。 收方：收方协议的实体在收到报文之后，如果报文无错误，并且序号和序号寄存器之 值相等，则向发方实体发出认可报文( 认可报文的序号值等于接收报文序号值) ，然后将 1 4 南京邮电大学硕士研究生学位论文第二章协议分析技术 报文递交给收方用户，序号寄存器的内容按模2 加1 ，如果接收的报文有错误，或者序号 不正确，则丢弃报文。 初始：a b 协议启动之后，发方和收方的序号寄存器初始化为0 。 根据前面的协议分析的理论，这里来具体的实现a b 协议。首先分析协议的环境。 2 6 2 协议环境分析 分析协议环境要从用户要求、通道性质和工作模式三个方面来考虑。 ( 1 )用户对a b 协议的要求包括： 永久连接服务，两个终端之间采用物理连接，每次通信不需要建立连接的过程， 也不需要给出通信双方的地址。 采用部分确认方式，通信过程采用三条服务原语：传送文件请求、传送文件指示 和传送文件证实。： 通讯方式采用单工、同步方式，即在一次通信过程中，只允许一方向另一方发送 数据报文。发送方发出一个数据报文后，要等到确认报文后才发送下一个数据报文。 数据形式为流数据( 字符流) ，发送方用户向协议实体提交的数据是文件体( 字符 流) 。 数据长度不受限，即文件长度是不受限制的。 数据报文无校验错、报文不丢失、不重复、顺序正确。 ( 2 )下层通道具有以下特性： a b 协议使用的通道为永不断路的全双工通道。 报文在通道种可能丢失，报文内容可能有错，但是重复发送n 次报文，至少有一 个是正确的。 认可报文不会丢失，不会出错，不会重复。 下层采用物理连接，无需连接建立过程。 ( 3 )a b 协议采用点到点和主从工作模式，由发送方用户启动文件传送过程。 2 6 3 协议功能分析 根据对协议环境的分析，可以明确a b 协议应该具有以下功能： 发送方以同步方式发送数据报文和接收确认报文，接收方以同步方式接收数据报 文和发送确认报文。 在发送端对p d u 加校验和，在接收端进行校验。 对数据报文进行顺序控制和重发控制。 1 s 南京邮电大学硕士研究生学位论文第二章协议分析技术 对文件进行读( 发送方) 和写( 接收方) 操作。 从功能分析可以看出，a b 协议是一个简单协议，只具有前述协议功能的一个子集。事 实上，一般协议都只具有前述协议功能的一个子集。 2 6 。4a b 协议元素设计 l 服务原语及其时序 服务原语是协议与用户的接口( 即服务访问点s a p ) ，用户通过服务原语得到协议提供 的服务。本协议实体需要三条服务原语：u r e q u e s t ( 传送文件请求) 、u i n d i f i c a t i o n ( 传 送文件指示) 、u c o n f i r m ( 传送文件证实) 。其服务结构如下。 2p d u 格式和p d u 交换时序 对等协议实体之间交换信息均以p d u 为单位，p d u 格式严格定义了信息的内容和含义， p d u 的格式一般用a s n 1 语言来定义。在设计协议时，除了要定义p d u 格式外，还必须定 义p d u 的交换时序，即规定一方收到某个p d u 后应该回什么p d u 或可以回哪些p d u 。p d u 的交换时序必须包括正常情况和各种异常情况。 p d u 的格式定义如下： 发送p d u 报文信息d r 1 个字节n 个字节 第一个字节为寄存器的值为0 或1 ，该p d u 的其他字节为传送的报文信息( 字符串) 。 确认包p d u 1 个字节 因 该p d u 由发送方给接收方，其内容为寄存器的值。用来标识接收的报文的寄存器的 值。 3 协议状态 设计a b 协议的状态，首先针对发方协议实体进行设计。对于发送方协议实体，可以设 计以下状态： 1 6 南京邮电大学硕士研究生学位论文第二章协议分析技术 r e a d y 一0 初始状态0 ，等待接接上层发起通信要求，同时向对方实体发送寄存器 标号为0 的报文。 w f a c k 一0 等待0 消息响应状态，接收到标号为0 的相应后，向用户发送确认原语。 r e a d y j 初始状态1 ，等待接上层发起通信要求，同时向对方实体发送寄存器标 号为1 的报文。 w f a c k _ i 等待1 消息响应状态，接收到标号为1 的相应后，向用户发送确认原语。 以上协议状态充分反映了发送方协议实体在协议工作过程中的各种情况。 其状态图为： 图2 4 2 发送实体状态图 对于接收方，分析相似。这里就不再详细说明。 4 协议事件 协议事件就是协议的输入。协议的输入包括三个部分：来自本方用户的服务原语，来 自对方协议实体的p d u ，及来自内部的定时器信号。在协议的p d u 设计中，已经定义了 定时器t 0 。t o 用来监视确认信息的到达。根据前面分析的服务原语和p d u 信息，这里的 输入事件有： u r e q u e s t 传送文件请求原语 u r e s p o n s e 传送文件响应原语 d r报文信息p d u a c k确认信息p d u t o 定时器信息 5 协议变量 协议中用到的各种变量都称为协议变量。这里定义如下几个需要用到的协议变量。 f i l e d a m 字符型，用来表示发送方用户要发送的报文。 6 协议动作和谓词 1 7 南京邮电大学硕士研究生学位论文 第二章协议分析技术 每个协议过程除执行一定的算法外还要根据协议的状态执行一系列的协议动作。协议 动作由输入事件驱使，并受条件的约束，表达这些条件的语句为谓词。 协议的动作很多，如发送p d u 给对等层实体，向上层用户发送服务原语，及设置定时器 等行为。 7a b 协议实体的文本 协议文本描述的是协议元素之间的关系，这里通过表2 1 来形象的描述状态之间的关 系。表2 1 。高 r e a d y _ 0 w f a c k0 r e a d yi w f a c k1 u r e q u e s t w f a e k0w f a c kl 1 a c k 0 r e p l yr e a d y _ l 1 a c k l r e p l y w f a c k0 t ow f a c k0 w f a e k1 1 8 南京邮电大学硕士研究生学位论文 第三章协议模型描述技术 3 1 简介 第三章协议模型描述技术 协议形式化模型是协议分析和设计的核心技术之一。协议的形式化模型有多种：如有 限状态机、p e t r i 网、时序逻辑和进程演算等基于形式化的模型技术。通过这些模型技术 可以实现网络协议的形式化，从而为协议的形式化分析与验证、协议测试以及协议实现等 技术提供良好的基础。同时，协议模型技术也是协议形式化描述语言的基础。本章将重点 研究状态机模型技术。 3 2p e t r i 网技术介绍 p e t r i 网是1 9 6 2 年，由德国的c a p e t r i 在他的博士论文“c o m m u n i c a t i o nw i t h a u t o m a t a ( 用自动机通信) 中首次提出网状结构的信息流模型。p e t r i 的这一工作引起了 美国和欧洲一些科学家的重视，a w h o l t 随后在他的“f i n a lr e p o r to ft h ei n f o r m a t i o n s y s t e mt h e o rp r o j e c t “( 1 9 6 8 ) 和“e v e n t sa n dc o n d i t i o n “( 1 9 7 0 ) 论文中用p e t r i 网 模拟和分析了具有并行分支的系统，并称这种网状结构为p e t r in e t s ，以后这个名字为大 家所接受。 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 r i 网通常表示为一种物理系统极为相近的图形形式，使人们能 够比较容易地学习和理解这种描述语言。p e t r i 网有一套成熟的数学理论工具，建立了许多 分析技术，包括可达性分析、不变量分析( 使用线性代数方法) 、保持特性的变换( 包括化简) 以及网的分解和等价。网的形式基础使网与其他并发模型建立了连接，这对于分布式系统 的描述和分析是很有益的。近几年来，人们的注意力集中在如何将代数的抽象数据类型融 合在高级网结构中。 p e t r i 网作为一种新的模型技术，其功能在不断的发展。但是其应用领域还不是很广 泛，相对于状态机模型来讲，状态机更容易被引用，而且大多数技术都是基于状态机模型 技术的，下面将着重研究状态机理论。 3 3 有限状态机 1 9 南京邮电大学硕士研究生学位论文 第三章协议模型描述技术 3 3 1f s m 的基本定义 有限状态机( f s m ，f i n it es t a t em a c h i n e ) 是一种数学模型。它包括以下几个部分：一