网络协议分析与设计全套教学课件

第1章概述第1章-概述第2章-协议设计1第2章-协议设计2第3章-协议形式化描述技术(1-概述及FSM)第3章-协议形式化描述技术(2-PetriNet)第4章-协议形式描述语言(1-SDL)第5章-协议验证技术第6章-协议验证工具全套可编辑PPT课件2内容提要课程概述1协议2协议工程33课程名称网络协议分析与设计/协议分析与设计网络协议工程网络：三网(计算机网络、电信网络、CATV)，分布式系统/操作系统协议：规定通信实体交换数据的格式以及有关的同步问题。工程：用工程化的方法来开发协议4课程目标为什么开这门课？研讨目标：协议开发中常见的设计技术、形式化描述技术和协议工程学的基本理论立足点：基于最基本的理论，结合最先进的技术，理解最本质的知识。本课程包括：阅读资料、课堂教学、课堂讨论、习题、上机实验、线上等环节。与协议有关的课程比较多，如：计算机网络、数据通信、分布式系统等。这些课程往往描述的是一些被广泛接受并被一些国际标准化组织标准化了的协议。它们并不解释：协议的设计过程、协议为什么正确工作、协议是不是有缺陷。而这些正是本课程要解决的问题。5课程目标(续)内容要求：对协议工程学有一个基本认识重点掌握协议设计技术、形式化描述技术(FSM，SDL)、协议验证技术了解一致性测试技术希望通过本课程的学习，不仅掌握所涉及的协议开发知识，而且锻炼一些基本的科研技能。独立解决具体科研问题的能力科研表达与沟通的能力面对一个并不熟悉的科研领域，可以做到独立查阅资料、确定具体的研究目标、制定实施计划、最终完成一个相对独立的研究。

将已经掌握的科研内容，用精练的语言（口头、书面）表达出来，通过与其他人讨论，更深入地掌握此方面知识。6授课内容概述(第一章)协议设计(第二章)形式化描述技术(FSM,PetriNet,SDL,LOTOS,ESTELLE)(第三、四章)协议验证(第五、六章)协议一致性测试(第七章)7国内相关课程北京邮电大学：协议工程与通信软件协议工程的概念协议模型协议形式化描述技术协议验证技术协议实现和测试技术MSC和SDL语言简介通信软件设计方法与实践清华大学：计算机网络中的形式化方法和协议工程学主要内容：形式化描述方法、一致性测试技术8国内相关课程(Cont.)中国科技大学软件学院：《通信系统软件开发》东南大学，河海大学研究生课程：《计算机网络协议工程》解放军理工大学，华中科技大学，南京邮电学院，云南大学，浙江理工大学等也开设了类似课程9国外相关课程一些国外的大学开设类似课程UniversityofFreiburg:NetworkProtocolDesignandEvaluation

rmatik.uni-freiburg.de/teaching/lecture/protocol-design-s09/slides.htmlLUT(LappeenrantaUniversityofTechnology):CommunicationsSoftwareandArchitecture

http://www2.it.lut.fi/kurssit/02-03/010607000/lectures.htmlUniversityofTwente:ProtocolEngineeringConcordiaUniversity:ProtocolDesignandValidationTelkomUniversity,SchoolofEngineering:ProtocolEngineering10先修课程计算机网络或数据通信操作系统分布式系统11参考书目吴礼发，《网络协议工程》，2011.4，电子工业出版社。HartmutKonig,ProtocolEngineering,2012,SpringerGerardJ.Holzmann,DesignandValidationofComputerProtocols,PrenticeHallAthttp://www.cs.rug.nl/~grl/ar05/spinbook/Book91.html古天龙，蔡国永，《网络协议的形式化分析与设计》，电子工业出版社，2003.6龚正虎，《计算机网络协议工程》，国防科技大学出版社，1993.12R.Lai,A.Jirachiefpattana,

CommunicationProtocolSpecificationandVerification,KluwerAcademicPublishers,1998

1213课时安排课堂：20学时，每周2学时根据需要，可安排部分课时自习，自习时间主要用来完成作业和阅读文献。线上：8学时上机：8学时待定14成绩评定课堂成绩(80%)

考试(70%)：闭卷考勤和作业(10%)：检查完成作业的质量，对知识的理解程度。实验及课程报告(20%)：实验(SPIN)，设计、描述、验证协议，撰写课程报告。课外作业(20%)：检查完成作业的质量，对知识的理解程度。实验及课程报告(80%)：实验(SPIN):设计、描述、验证协议，撰写课程报告。15内容提要课程概述1协议2协议工程316网络协议定义计算机网络不可缺少的组成部分为网络中互相通信的对等实体间进行数据交换而建立的规则、标准或约定，保证实体在计算机网络中有序地交换数据。实体(Entity)是指任何可以发送或接收信息的硬件或软件进程，在大多数情况下，就是一个特定的软件进程。位于不同系统的同一层次内交互的实体，就构成了对等实体。17协议定义(Cont.)英格兰国家物理实验室NPL(NationalPhysicalLaboratory)的R.A.Scantlebury和K.A.Bartlett在一份备忘录(AprotocolforuseintheNPLdatacommunicationsnetwork)中最早将“协议(protocol)”一词用于描述数据通信过程。NPL设计了计算机互联系统，证明了数据包交换思想可行性“协议是关于分布式系统进行信息交换时的一种约定，协议应按照语言的方式进行定义。”基于他们的观点：网络协议就是具有规定文法、语法和语义的语言，其中，文法给出了有效信息的精确格式，语法描述了数据交换的规则，语义规定了可交换信息的词汇及其含义。18协议定义(Cont.)协议三要素(从语言的角度来理解协议)：语法语义同步

19协议定义：语法在语言学中，语法即是语言的结构方法和构成规则，语言组成成分(词、句等)之间以什么样的规则结合而构成语句或语言。网络协议中的语法？网络协议中的语法体现为数据报文中的控制信息(通常在报文的首部)和各种控制报文的结构、格式，即规定报文的长度，报文中划分多少个域(Field)，每个域的名称、数据类型、长度等。其中，报文中各个域的类型、长度及相互间的位置、顺序关系则构成了词法。TCP报文20IP报文2122协议定义：语义网络协议的语义可以理解为协议数据报文中的控制信息和控制报文所约定的含义，即需要完成何种动作，发出何种控制信息以及做出何种响应。例如：IP报文首部控制信息中的目的地址域指明了报文的目的地，接收到此报文的网络节点均将依据该域进行路由选择，因而，规定在首部控制信息中的给定域给出目的节点地址就是一种语义。

23协议定义：语义(Cont.)例如(续)：为实现有连接的传输服务，设计一套连接建立的控制报文。发起方构造一个“请求连接”的协议控制报文，“请求连接”就是该控制报文的语义。接收方收到这个控制报文后，根据已知的格式，分析规定域中的报文类型码，就可了解这个“请求连接”的语义，从而作出“允许连接”或“拒绝连接”的响应。“允许连接”报文和“拒绝连接”报文的语义也是协议约定好的，通信双方通过按一定时序关系交换这些约定语义的控制报文，即可实现建立连接的功能和提供有连接服务。在协议中，常使用的“数据收到确认”报文(ACK报文)、“出错通知”报文、“紧急通知”报文等，均是具有特定语义的协议报文，即协议的组成部分。24协议定义：同步简单地说，同步是指事件发生顺序的详细说明。具体来说，同步是指通信过程中各种控制报文传送的顺序关系，例如“允许连接”或“拒绝连接”报文必须是作为请求连接报文的一种响应来发送，“拆除连接”报文也必须在建立连接后的某种条件下发送，等等。这种控制报文发送的时序关系，也决定了通信双方所处的通信状态(发送状态、接收状态、等待状态等)，所以常用建立通信双方的有限状态机的方法来描述网络协议。在有些文献中，也将这种同步关系视为协议语法的一部分。

SYN-SENTESTAB-LISHEDSYN-RCVDLISTENESTAB-LISHED

用三次握手建立TCP连接的各状态

SYN=1,seq=xACK=1,seq=x+1,ack=y

1CLOSEDCLOSED数据传送主动打开被动打开AB客户服务器SYN=1,ACK=1,seq=y,ack=x

1TCP的连接建立26协议定义：进一步延伸进一步延伸为计算机通信协议。

协议是计算机网络和分布式系统中各种通信实体或进程间相互交换信息时必须遵守的一组规则或约定。网络协议工程中的许多技术和方法均可应用到分布式系统中的进程间通信协议的设计过程中。

27网络体系结构大量的研制经验表明，对于非常复杂的计算机网络协议，应采用层次式结构。在计算机网络中，将计算机网络的各层及其协议的集合，称为网络的体系结构(architecture)。ISO的OSI/RM(开放系统互连/参考模型)IBM的SNA(系统网络体系结构)DEC的DNA(分布式网络体系结构)IETF的TCP/IP28协议标准化Whatarestandards?Standardsaredocumentedagreementscontainingtechnicalspecificationstobeusedconsistentlyasrules,guidelines,ordefinitionsofcharacteristics,toensurethatmaterials,products,processesandservicesarefitfortheirpurpose,contributetomakinglifesimpler,andtoincreasingthereliabilityandeffectivenessofthegoodsandservicesweuseInternationalStandardsNationalStandardsIndustry-widestandardizationisaconditionexistingwithinaparticularindustrialsectorwhenthelargemajorityofproductsorservicesconformtothesamestandards(某个行业范围内统一的标准)29协议标准化(Cont.)WhyPushForStandardization?Theaimistofacilitatetrade,exchangeandtechnologytransferthroughEnhancedproductqualityandreliabilityatareasonableprice.Greatercompatibilityandinteroperabilityofgoodsandservices.Simplificationforimprovedusability.Increaseddistribution(发布)efficiency,andeaseofmaintenanceWithoutStandardization,NsourcesandMdestinationsforinstance,leadstoN*Mprotocolsand2*N*Mimplementations…协议标准化(Cont.)31协议标准化(Cont.)Whatdoesastandardlooklike?-ISOexplainsthemajorcomponentsoftheirstandardsdocuments:Itcanbeanythingfromafourdocumenttoa1000tome(大部头，巨著),includingtwicetheweightofthestandarditselfininformativeannexes.Itmayspecifythetasksthatacertainrangeofequipmentmustbeabletoperform,ordescribeindetailanapparatusanditssafetyfeatures(规定一类设备必须能够执行的任务或者详细描述一个装置和它的安全特征)32协议标准化(Cont.)Whatmakesupastandard?Itmaycontain:SymbolsDefinitionsDiagramsCodesTestmethods33协议标准化(Cont.)协议标准化组织InternationalOrganizationforStandardization(ISO)国际电报电话咨询委员会

(CCITT)InternationalTelecommunicationsUnion(ITU-T)InternationalFederationforInformationProcessing(IFIP)InternetEngineeringTaskForce(IETF)WorldWideWebConsortium(W3C联盟)AsynchronousTransferModeForum(ATMForum)AmericanNationalStandardsInstitute(ANSI)InstituteofElectricalandElectronicsEngineers(IEEE)AssociationforComputingMachinery(ACM)34ISO是一个涉及范围很广的国际标准开发机构，包括很多政府的或民间的标准研究机构，如美国的国家标准研究所ANSI。成立于1947年。ISO下属多个技术委员会TC(TechnicalCommittees)，TC又由多个分委员会SC(Subcommittees)组成。每个SC下有多个工作组WG(WorkingGroups)。例如，TC97主要负责与计算机有关的标准的制定，TC97/SC6主要处理电信领域的标准，TC97/SC6/WG1则主要负责数据链路协议标准。一个ISO标准从最初的提名到真正发行要经历七个步骤。

35ISO(Cont.)ISO制定的很多标准是与另一个标准化组织，国际电工技术委员会IEC(InternationalElectrotechnicalCommission)，合作制定的。IEC关心的主要是电子和电气工程标准(器材、元件以及测量方法的标准化)。在信息技术领域，虽然IEC强调的是硬件，而ISO强调的是软件，但它们的职能在很多地方有所重叠。1987年由这两个组织联合成立了联合技术委员会JTC，同时ISO的TC97宣告解散。代替旧的ISO的TC97组织是ISO/IECJTC1，而其下属的各分委员会SC的名称仍用原来TC97中的各分委员会的序号。这个委员会负责信息技术领域文档的开发，这些文档最终可能成为ISO及IEC的标准。36ISO(Cont.)ISO制定的与协议有关的著名标准：OSI/RM(ISO7498)，TC97/SC16制定，虽然没有流行，但其中有很多协议被广泛使用形式描述语言LOTOS和Estelle,ISOTC97/SC21/WG1下的2个不同的子工作组分别制定的，它们得到了广泛的应用。

一致性测试序列标准：ISO9646-1(CCITTX.290)一般概念ISO9646-2抽象测试集(suite)规范ISO9646-3树表组合记法TTCN(TreeandTabularCombinedNotation)ISO9646-4测试实现ISO9646-5一致性认证处理对测试实验室及其客户的要求ISO9646-6测试实验室的操作37CCITTandITU-TCCITT(InternationalTelephoneandTelegraphConsultativeCommittee,国际电话与电报顾问委员会)最开始主要从通信的角度考虑一些标准的制定。随着科学技术的发展，通信与信息处理的界限变得比较模糊了。于是，通信与信息处理就都成为CCITT与ISOTC97共同关心的领域。

很多ISO制定的标准，CCITT均有与之相对应的标准。

CCITT的建议书X.200就是开放系统互连参考模型，它与ISO7498基本上是相同的。

CCITT制定的著名标准：X.25形式描述语言SDL(SpecificationandDescriptionLanguage)广泛用于交换系统的描述。

38CCITTandITU-T(Cont.)ITU-T是国际电信联盟ITU(InternationalTelecommunicationUnion)下属的电信标准部，它的成员主要是各国政府组织和得到许可的私人运营商。成立于1993年3月1日，主要任务是制定电话、电报和数据通信接口的技术建议。它取代了原国际电报电话咨询委员会CCITT。人们仍然常常遇到CCITT建议，例如，CCITTX.25，虽然自1993年起这些建议都打上了ITU-T标记。ITU-T的实际工作是在研究组SG(StudyGroup)完成的，通常有400人。为了能够完成工作，研究组又分成了很多工作组WG(WorkingGroup)，然后又再分为专家小组(ExpertTeam)，最后分成特别小组(AdHocGroup)。39IFIP国际信息处理联盟IFIP(InternationalFederationforInformationProcessing)，虽然不直接参与协议的标准化，但它的主要目的之一是作为CCITT和ISO之间沟通的桥梁。IFIP成立于1960年，经常组织一些协议形式化描述与验证方面的国际会议，例如，JointInternationalConferenceonFormalDescriptionTechniquesforDistributedSystemsandCommunicationProtocols(FORTE)andProtocolSpecification,TestingandVerification(PSTV)。40IETF因特网协会ISOC因特网体系结构研究委员会IAB因特网研究指导小组IRSG因特网研究部IRTF因特网工程部IETF因特网工程指导小组IESG领域领域…WGRGWGWGWG……RG…IETF网址：41IETF(Cont.)因特网在制定其标准上很有特色：面向公众。所有技术文档都可从因特网上免费下载，而且任何人都可以用电子邮件随时发表对某个文档的意见或建议。这种方式对因特网的迅速发展影响很大。因特网标准：RFC(RequestForComments)的意思就是“请求评论”。所有的RFC文档都可从因特网上免费下载。

并非所有的RFC文档都是因特网标准，其中只有一小部分最后才能变成标准。42IETF(Cont.)因特网草案建议标准草案标准因特网标准历史的RFC实验的RFC提供信息的RFC因特网草案(InternetDraft)建议标准(ProposedStandard)RFC文档草案标准(DraftStandard)因特网标准(InternetStandard)43W3CWorldWideWebConsortium(万维网联盟)promotestheWebbyproducingspecificationsandreferencesoftware.为解决Web应用中不同平台、技术和开发者带来的不兼容问题，保障Web信息的顺利和完整流通，W3C制定了一系列标准并督促Web应用开发者和内容提供者遵循这些标准。标准的内容包括使用语言的规范，开发中使用的导则和解释引擎的行为，等等W3Cisfundedbyindustrialmembersbutitsproductsarefreelyavailabletoall.TheConsortiumisrunbyMITLCSwithINRIAactingasEuropeanhost

andKeioUniversityinAsia,incollaborationwithCERNwheretheweboriginated.万维网发明者蒂姆·伯纳斯-李(TimBerners-Lee)获得2016年ACM“图灵奖”CERN（欧洲粒子物理研究所）44ATMForumTheAsynchronousTransferModeForumisaworldwideorganization,aimedatpromotingATMwithintheindustryandtheendusercommunity.FormedinOctober1991,withfour(4)members,theATMForummembershipcurrentlyincludesmorethan700companiesrepresentingallsectorsofthecommunicationsandcomputerindustries,aswellasanumberofgovernmentagencies,researchorganizationsandusers.45ANSIFoundedin1918,theAmericanNationalStandardsInstitute(ANSI,美国国家标准化组织),isaprivate,not-for-profitmembershiporganizationthatcoordinatestheU.S.voluntaryconsensusstandardssystemandapprovesAmericanNationalStandards.ANSIconsistsofapproximately1,300nationalandinternationalcompanies,30governmentagencies,20institutionalmembers,and250professional,technical,trade,laborandconsumerorganizations.FamousStad.:ANSIC46IEEETheInstituteofElectricalandElectronicsEngineers(电气和电子工程师协会)istheworld’slargesttechnicalprofessionalsociety(专业技术协会).Anon-profitorganization,IEEEpromotes(促进)thedevelopmentandapplicationofelectrotechnology(电工)

andalliedsciencesforthebenefitofhumanity,theadvancementoftheprofession,andthewell-beingofit’smembers(为了人类的利益，技术的进步，会员的福祉，促进电工和相关科学的发展和应用).FamousStandards:IEEE802series,eg.802.3，802.1147ACMAssociationforComputingMachinery(founded1947，(美国)计算机学会)isaninternationalscientificandeducationalorganizationdedicatedtoadvancingtheart,science,engineering,andapplicationofinformationtechnology(其宗旨在于不断地推动计算机科学与技术的发展),servingbothprofessionalandpublicinterestsbyfosteringtheopeninterchangeofinformationandbypromotingthehighestprofessionalandethicalstandards.SinceitsinceptionACMhasprovideditsmembersandtheworldofcomputerscienceaforumforthesharingofknowledgeondevelopmentsandachievementsnecessarytothefruitfulinterchangeofideas.48ACM(Cont.)OvertheyearsACMhasflourishedalongwiththeindustryitself,playingamajorroleinenrichingthequality,formandfunctionofcomputerusage.ACMformsSpecialInterestGroups(SIGs)whichfocusonspecificareasofcomputerscience.(/sigs)DataCommunication(SIGCOMM)Security,AuditandControl(SIGSAC)ComputerGraphicsandInteractiveTechniques(SIGGRAPH)Hypertext/Hypermedia(SIGLINK)Multimedia(SIGMM)49Obtainingstandarddocuments:Standardsbodiesdistributetheirdocumentsinseveralfileformatsandtodifferentgroupsororganizations.MoststandardsareavailableontheInternetviaFTP,Gopher,ortheWWW.Manysiteshavesearchengineswhichallowuserstoobtaindifferentdocuments,allofwhichpertaintothesamestandard/protocol.50Obtainingstandarddocuments(Cont.)Manystandardsmustbepurchasedbeforeyoumayimplementproductsbasedonthem.However,thedocumentsarefree.Somestandardsbodiesrequirepaymentup-front(预先)

beforeyouarepermittedaccesstothestandardsdocuments.Stillotherstandardsbodiestakeanopenapproachwheredocumentsareentirelyfreetoreadersandimplementationvendors(RFCs).51Obtainingstandarddocuments(Cont.)DocumentFormats:Text/ASCII-mostpopularformat.Postscript-requiresapostscriptprinterorTeX/LaTeXtoview.WordforWindows-MicrosoftWindowseditor.HTML-browseabledocumentswithlinkstootherreferences.PDF-AdobeAcrobathyper-linkformat.52Obtainingstandarddocuments(Cont.)DocumentLanguages:Mostinternationalstandardsbodiesoffertheirdocumentswritteninpopularspokenlanguages(大多数国际标准化组织所提供的文档一般用多种流行的口语编写),including:EnglishFrenchSpanishNationallanguageoftheorganization’sorigin.53IndustryControlandAcceptanceCommonlyintoday’scomputerindustry,theacceptanceofproductsarefacilitatedbytheconformancetoandsupportofstandards(与标准一致性和对标准的支持能够提高产品的接受程度).Mostproductsbecomeobsoleteiftheyareonlybasedonproprietaryspecificationsanddonotsupportstandards.Ifacompanymaintainscontroloverthemajorityofproductsbasedonaparticulartechnology,thatcompanycanusuallydictate(主宰)thedirectionoftheindustryandanystandardstofollow.54内容提要课程概述1协议2协议工程355ProtocolEngineering：Why?网络类型的多样性应用的多样性网络系统的多样性导致在协议方面的体现多样性分布性异步性并发性不稳定性复杂性正确性完备性安全性可移植性标准化导致用直觉的工程方法不能保证协议的协议工程(ProtocolEngineering)软件工程的经验上个世纪七十年代末人们开始用形式化的方法描述通信协议。1981年，在软件工程思想的基础上，Piatkowski首先提出了“协议工程(PE,ProtocolEngineering)”的概念协议工程学用形式化方法描述协议设计和维护中的各个过程，它是以协议软件为研究对象的软件工程，而且建立了一套比一般软件工程方法更为严格、更为数学化的理论和方法。协议工程过程集成化(Integrated)、形式化(Formal)的协议开发过程目的是减少协议开发过程中潜在的错误，提高协议开发的效率，促进协议标准化的发展。56ProtocolEngineering:What?Piatkowski,T.F.(1981).Anengineeringdisciplinefordistributedprotocolsystems.Proc.IFIPWorkshoponProtocolTesting—TowardsProof?,pp.177–215.在以往的协议开发过程中，各个阶段并不互相衔接，各个阶段的研究人员完成自己的工作就不再管其他的工作。协议设计者凭自己的经验和智慧设计出协议，用自然语言进行描述，经过他人审定或模拟之后，就予以公布。其他的人只有在感兴趣时才采用某种方法和理论对协议进行验证。协议实现者往往根据自己的环境和要求修改协议，协议实现之后不考虑实现与协议规范是否一致。协议的测试往往由协议实现者自己进行，这实际上是一种程序调试。57ProtocolEngineering:What?所谓“集成化”，就是指协议描述、验证、实现和测试等技术前后衔接。所谓“形式化”，就是指用形式描述技术FDT(FormalDescriptionTechnique)贯穿协议开发的各个阶段。利用形式化描述语言FDL(FormalDescriptionLanguage)对协议进行形式化描述FDL以一种或多种形式化描述技术为基础，有严格的语法和语义定义，抽象于具体的实现，可以符号执行，可以转换、翻译成程序设计语言。当进行形式化描述后，协议的验证、自动实现、测试就可以在一个集成化的协议工程系统中进行。58ProtocolEngineering:What?协议工程过程中协议的表现形式：59ProtocolEngineering:Procedure非形式化协议规范形式化协议规范形式化描述与机器无关的源代码实现代码(产品)编译产品测试器测试序列发生器一致性测试性能分析模拟验证设计用户需求说明实现60PEActivities:Design我们的定义：根据协议的需求说明构造协议的非形式描述文本(经过非形式的验证分析)称为协议设计；而将“协议的设计、形式描述、验证、实现、测试、运行”这一全过程称为“协议开发”，即协议开发是指协议工程活动的全过程。

其它定义：将协议设计定义为“从协议的需求说明到协议的形式描述，并经过严格验证和性能分析”这一过程，或定义为协议工程活动的全过程，即相当于“协议开发”。

包括：协议环境分析、协议的功能设计、协议组织形式的确定、协议元素的构造、协议文本的编制等。61PEActivities:Design(Cont.)协议设计涉及到很多技术，如差错控制、流量控制、连接管理、路由选择等。协议设计还必须遵循一些基本原则，如结构化、模块化等。

协议设计阶段的结果是非形式描述协议文本。协议设计质量的好坏是直接关系到开发出来的协议性能、功能是否能满足用户需求的一个重要因素。课程的重点内容62PEActivities:FormalDescrpt.通信系统行为的复杂性增大了行为描述的难度，人们必须借助一种语言或技术来准确地描述系统行为。在过去，人们习惯使用自然语言进行协议描述(用自然语言写协议的规格说明或规范)，优点是：方便、易懂、表达能力强致命缺点是：不严格、不精确、结构不好、没有描述标准和有二义性不同的人对协议描述的理解不一样导致不同的协议实现之间不能实现互连，甚至还会得出错误的协议。

且很难进行协议验证、协议实现和测试的自动化。

解决办法：形式化技术FDT(FormalDescriptionTechnique)63PEActivities:FormalDescrpt.采用形式描述技术的最终目的是：为开发者提供一种分析的方法；作为对开发结果验证的基础；为设计人员和应用人员提供交流途径；作为开发文档能在将来再开发时使用。

理想的形式描述技术应该既能描述系统的行为特征，又能进行操作：在系统需求分析和设计阶段，它应该是一种描述语言在系统实现阶段它应该是一种编程语言。形式描述技术是将协议工程各阶段在技术上衔接起来的纽带，因此，它对协议工程的发展起决定性作用。64形式描述模型

有限状态机FSM(FiniteStateMachine)Petri网(PetriNet)时态逻辑TL(TemporalLogic)通信系统演算CCS(CalculusofCommunicationSystem)通信顺序进程CSP(CommunicatingSequentialProcesses)形式文法FG(FormalGrammar)

形式描述语言

CCITT制定的SDLISO制定的Estelle和LOTOS对象管理组织OMG制定的统一建模语言UML课程的重点内容PEActivities:FormalDescrpt.65PEActivities:VV协议验证(VerificationandValidation)技术和形式描述技术是同步发展的在进行协议实现之前还要进行以下两项工作：在语法和语义方面进行验证；进行计算机模拟。

协议的验证主要内容包括：可达性分析死锁和活锁检测协议的有界性和完整性检查协议的动作序列检查通道溢出检查等

66PEActivities:VV(Cont.)验证方法主要有两类：模型检查(ModelChecking)最常见方法：可达性分析，它包括状态穷举，状态随机枚举，状态概率枚举等方法重要问题：状态空间爆炸证明(Proving)用推理演算方法严密地证明协议的各种性质其他方法：模拟(Simulation)通过一些模拟试验来测试协议的各种性质67PEActivities:Implementation协议实现是指由协议规范到协议的可执行目标代码的过程协议的实现必须满足协议规范的要求，以及针对具体应用需要提供附加机制协议实现的自动化是协议工程的目的之一，但完全自动化几乎是不可能的。协议不是针对某种机器或者某种特定环境而设计的，而且协议实现者还要处理很多协议设计中没有说明的技术问题通过形式化描述技术可实现半自动化，两个步骤：第一步利用翻译程序将协议的形式描述文本转换成与机器无关的源代码(程序设计语言，如C语言)手工编写与机器有关的、在协议规范中没有描述的问题的处理代码。协议实现不在本课程的讨论范围68PEActivities:Testing测试是指验证协议的实现，一般主要考虑两个方面：

协议一致性测试(conformancetesting)。即检测新协议实现是否能满足该协议规范所规定的规则。

对协议实现的评价。分析协议实现的其他性质，如性能参数等。

协议一致性测试是协议工程活动中重要的一环。如果协议实现不能通过一致性测试，则表明该协议实现与其它通过一致性测试的协议实现不能在同一个全局系统中很好地协调工作。

互操作测试vs.一致性测试协议一致性测试要做到两点：彻底性和标准化“彻底性”是指必须彻底测试所实现的协议,“标准化”是指使用的测试集必须是标准的。

69PEActivities:ConformanceTesting一致性测试的基础：FDT一致性测试要解决两个问题：测试系统设计：重点解决测试方法和测试系统的体系结构问题测试序列的产生：解决测试的“彻底性”和“标准化”问题，以及测试序列的自动生成和形式化描述问题。

测试序列生成器可以产生各种可能发生的情况组合，以测试所实现的协议是否在各种正常和非正常情况下均能正确工作。

国际标准化组织ISO发布了“开放系统互连一致性测试方法和框架(ISO9646)”来指导一致性测试工作，并为许多常用的标准协议制订了相应的一致性测试序列。

协议工程中技术难度最大，业界又很需要。70PEActivities:PerformaceTesting协议的性能主要包括吞吐量和时延

协议的性能分析目的是改善协议机制，提高执行效率。

可用数学分析方法和模拟方法来进行，两者都基于排队论和概率论

本课程不涉及此课题

71PEActivities:Maintenance协议维护(Maintenance)是指对已运行的协议的修改、补充等，故协议的维护可能包含协议设计、协议的验证和分析、协议测试，以及协议实现等多项任务。良好的设计有助于降低维护成本。72参考以下PPT介绍的有关协议工程概念的不同观点，供参考73ProtocolEngineering:Another74ProtocolEngineering:Another(Cont.)75协议开发过程(

FerreiraPires)ProtocolengineeringUser

requirementsService

specificationProtocol

specificationProtocol

implementationCoursesDesignof

TelematicssystemsProtocolimplementationProtocol

designService

design76思考题1-1试论“软件工程”与“协议工程”的关系。1-3从你所知的网络协议中选择一个，来简要说明该协议的三要素。第2章协议设计

（1-协议模型）78内容提要协议设计概述1协议模型279协议设计概述协议设计的含义协议设计是一件很困难的事情Example:ClaytonTunnelProtocolExample:蓝军与白军作战问题80协议例子-ClaytonTunnelProtocolEngland,ClaytonTunnel:1.5英里1841,WilliamCookeTelegraph（电报）insteadofOpticaltelegraphforRailwayTunnelProtection,节省成本（只需1/10）和提高速度。Purpose:avoidthatmorethanonetrainisinthetunnelatthesametimeFirstlyusedonseverallinesoftheGreatWesternRailwaysinEngland.1842年，Cooke“火车可以无所畏惧地行驶，而无论其时间是否正确，也不管其是否在正确的轨道上，因为在使用该系统后，其速率总可以及时地降下来，从而避免碰撞”8181ClaytonTunnelProtocol-电报(Telegraph)基本原理，1753，C.M给Scots杂志的信中描述了一个使用一些平行电线来通信的电子电报。1830，英国MichaelFaraday和美国JosephHenry发现了电磁感应1837，WilliamCooke利用电流来使处在接收端磁场中的罗盘指针发生偏转，从而得到信号。1837年6月12日，第一个电报系统的专利，“五磁针信号系统”。82ClaytonTunnelProtocolsemaphoreswithblock-intervalsystem(空闲/阻塞信号系统)turntoredautomaticallyasatrainpassessettogreenbyhandafterwardsredandwhiteflagstoreplacemalfunctioningsemaphoresignalmenonbothendslinkedbytelegraphiclinemalfunctionofblock-intervalsystemsignalledbyabell83ClaytonTunnelProtocol：报文(Messages)Message:TT:TraininTunnelTF:TunnelisFreeTL:HastheTrainlefttheTunnel?84ClaytonTunnelProtocol：差错控制ErrorFreeFunctioningtrainenterstunnel,signalmanAsendsTTtoBtrainleavesthetunnel,BsendsTFtoAAsetssemaphoretogreenbyhandUnderErrorSituationtrainenterstunnel,AsendsTTtoBbellrings,Ashowsredflagtonexttraintrainleavesthetunnel,BsendsTFtoAAshowswhiteflagtonexttrain85ClaytonTunnelProtocol：事故(Accident)OnedayinAugust1861atClaytonTunnel...train-1enterstunnel,block-intervalsystemfails(failstosetthesignaltored),sothebellwarnssignalmanA,ThenAsendsTTtoB,thenfetchestheredflagtowarnthenexttrain.train-2comestoofast,andcouldnotstopintime,hasalreadypassedthegreensignal.“Fortunately”,itsdrivercatchesaglimpseoftheredflagjustintimeasheentersthetunnel.train-3seestheredflagandstopsbeforethetunnelentrance.86ClaytonTunnelProtocol：事故(Accident)AsendsanotherTTtoB(fortrain-2)Bdoesnotunderstandsecond

TTBecausetheprotocoldidnotaccountforthisevent,sothemeaningoftwosubsequentTThadnotbeenspecified.AsendsTL(hasthetrainleftthetunnel?)toB87ClaytonTunnelProtocol：事故(Accident)Bseestrain-1andsendsTFAthinkstrain-2leftthetunnelandshowswhiteflagtotrain-3train-2hadseenredflagbefore,isafraidandtriesto

returntopositionA

aftersomedeliberation.88ClaytonTunnelProtocol：事故(Accident)Resulttrain-3andtrain-2crashed:21peoplediedand176gotinjuredThesetofinstructionsgiventothesignalmenwasincomplete,whichleadstotheaccident89ClaytonTunnelProtocol：LessonsAhistorianofrailwaydisasters(Nock,1967)：

“Onecanalmosthearthesamecommentbeingmadetimeaftertime.‘Icouldnotimaginethatcouldeverhappen.’Yetbitterexperienceshowedthatitcould,andgraduallytheregulationsandrailwayengineeringpracticewereelaborated.”Protocol:UsedUndernormalcircumstancesandthatallowedforasaferecoveryfromunexpectedevents.90ClaytonTunnelProtocol：Lessons(Cont.)EventhemostsimpleprotocolsmaycontainerrorsProtocolsmustbefullyverifiedbeforetheyareputinoperationtechniquestostructure,design,analyzeandverifyprotocolsarenecessary91一个简单的网络协议(蓝军与白军)谢希仁教授《计算机网络》的一道作业题：蓝军与白军作战，蓝军占据两个山顶，白军驻扎在这两个山之间的山谷。其力量对比是：一个山顶上的蓝军打不过白军，但两个山顶的蓝军协同作战则可战胜白军。一个山顶上的蓝军拟于次日正午向白军发起攻击。于是发送电文给另一山顶上的友军。但通信线路很不好，电文出错或丢失的可能性较大。因此要求收到电文的友军必须送回一个确认电文。但此确认电文也可能出错或丢失。试问能否设计出一种协议使得蓝军能够实现协同作战因而一定(即100%)取得胜利？92明日正午进攻明日正午进攻如果情况如上所述，次日蓝军1和蓝军2的协同进攻必定获胜。但情况并非如此简单。因为所发的报文可能会丢失。明日正午进攻丢失!白军蓝军1蓝军2因此蓝军1必须在收到蓝军2的确认后才能进攻93明日正午进攻确认明日正午进攻确认因此，收到报文后必须加以确认但这个确认报文也可能丢失：确认丢失!白军蓝军1蓝军2故蓝军2必须要收到蓝军1发出的对此“确认”的确认，才能知道发送出的确认是否被蓝军1正确收到。94明日正午进攻确认明日正午进攻确认因此蓝军1收到确认报文后应发送对此“确认”的确认。对“确认”的确认对“确认”的确认蓝军1无法知道最后发送的这个确认是否被蓝军2收到，仍需收到蓝军2发来的确认才行！白军蓝军1蓝军295白军蓝军1蓝军2协议必须能够应付所有的（而不是部分的）不利情况，像这样简单的问题居然无法设计出一种协议来解决。96内容提要协议设计概述1协议模型2法律上的(dejure)国际标准开放系统互联参考模型OSI/RM并没有得到市场的认可。非国际标准TCP/IP现在获得了最广泛的应用。TCP/IP常被称为事实上的(defacto)国际标准。两种网络模型OSI/RM的7个层次98层号中文名称英文名称英文缩写7应用层ApplicationLayerA6表示层PresentationLayerP5会话层SessionLayerS4传输层TransportLayerT3网络层NetworkLayerN2数据链路层DataLinkLayerDL1物理层PhysicalLayerPHTCP/IP99对应OSITCP/IPTCP/IP主要协议高层（5-7）应用层TELNET,FTP,SMTP,DNS,HTTPNFS,SNMP传输层（4）传输层

TCPUDP网络层（3）网际层IGMPICMP

IP

ARPRARP

低层（1-2）网络接口层可使用各种物理网络OSI/RM、TCP/IP模型100应用层表示层会话层传输层网络层数据链路层物理层应用层传输层IP层网络接口层OSI的概念清楚、理论也较完整，但它既复杂又不实用TCP/IP简洁实用应用层传输层网络层数据链路层物理层综合OSI和TCP/IP的优点OSI/RMProblems只要遵循OSI标准，一个系统就可以和位于世界上任何地方的、也遵循这同一标准的其他任何系统进行通信。在市场化方面OSI却失败了。OSI的层次划分并也不太合理，有些功能在多个层次中重复出现。

OSI标准的制定周期太长，因而使得按OSI标准生产的设备无法及时进入市场；OSI的专家们在完成OSI标准时没有商业驱动力；OSI的协议实现起来过分复杂，且运行效率很低；101102OSI/RMProblemsTannenbaum:BadtechnologyBadtimingBadimplementationBadpolitics103BadtechnologyModelandprotocolflawedBoundariessomewhatarbitraryTopthreelayersneverquiteresolved

(application,presentation,session)Whysevenlayers?ManyfundamentalissuescanbeaddressedatmultiplelayersReliabilityFlowcontrolSecurityAddressing/namingStandardizedbeforeimplementedDesignbycommitteew/oimplementationvs.designbyimplementors/researchers/engineers104Timing:It’simportantforstandardsMITD.Clark‘s“apocalypse(启示)ofthetwoelephants”(/~jabsher/apoc_eleph/apoc_eleph.html)ThebestperiodforstandardizationisbetweenburstofresearchandburstofmarketingTheperiodisveryshort105BadtimingMITD.Clark‘s“apocalypse(启示)ofthetwoelephants”Technologyactivityvs.timetostandardizationTCP/IPalreadyentrenchedbymid/lateeightiesOSI/RMisputupintheburstofmarketingofTCP/IP106BadimplementationsComplexity

huge&slowimplementations(考虑大而全，要全部实现就笨拙且效率低)Competition(BSDTCP/IP)wasgood,free,andeasytodeploy107BadpoliticsPushedbyEuropeanCommunityandU.S.governmentNegativeimageofgovernmentdictatingstandardsRemember“ClipperChip”TheClipperchipwasachipsetthatwasdevelopedandpromotedbytheU.S.NationalSecurityAgencyasanencryptiondevicetobeadoptedbytelecommunicationscompaniesforvoicetransmission.Itwasannouncedin1993andby1996wasentirelydefunct.TCP/IP2004年度图灵奖授与文顿·G·瑟夫和罗伯特·E·卡恩。1974年5月，罗伯特·卡恩和温特·瑟夫在IEEE期刊上发表了题为《关于分组交换的网络通信协议(AProtocolforPacketNetworkIntercommunication）》的论文，提出了使用传输控制协议TCP(TransmissionControlProtocol）和网际互连协议IP(InternetProtocol）来实现计算机网络之间的互连。108109TCP/IP:FeaturesLayeringnotstrict-onlywhereappropriateCandefinenewabstractionsontopofanyexistingprotocolIP/UDPprovidessimple“sendapacket”svcEx:RPC,DNS,IPphone,etc.Hourglass(沙漏)shapeIPcenterpiece(核心),commondenominatorDesignandimplementationgohand-in-handIETFrequirestwoindependent,interoperableimplementationsbeforestandardizationThe“dogma(教义)”:

Werejectkings,presidents,andvoting.Webelieveinroughconsensus(共识)andworkingcode.D.ClarkTCP/IP模型110应用层运输层网际层网络接口层主机A主机B路由器网络

2网络

1应用层运输层网际层网络接口层网际层网络接口层4321路由器在转发分组时最高只用到网络层而没有使用运输层和应用层。111TCP报文IP数据报MAC帧应用层数据首部首部尾部首部链路层及以下使用硬件地址硬件地址网络层及以上使用IP地址IP地址TCP/IP模型112HA1HA5HA4HA3HA6主机H1主机H2路由器R1硬件地址路由器R2HA2IP1IP2局域网局域网局域网通信的路径H1→经过R1转发→再经过R2转发→H2查找路由表查找路由表TCP/IP模型两台主机之间的数据传输，总是在一段一段的链路上传送的113IP1HA1HA5HA4HA3HA6HA2IP6主机H1主机H2路由器R1IP层上的互联网MAC