形式化描述技术概述FSM.ppt

《形式化描述技术概述FSM.ppt》由会员分享，可在线阅读，更多相关《形式化描述技术概述FSM.ppt（83页珍藏版）》请在淘文阁 - 分享文档赚钱的网站上搜索。

1、 网网 络络 协协 议议 工工 程程 第第 3 讲：协议形式化描述技术讲：协议形式化描述技术5/17/20231形式化描述技术第第 3 讲：协议形式化描述技术讲：协议形式化描述技术3.1 概述概述3.2 有限状态机有限状态机(FSM)3.3 PetriNet3.4 SDL3.5 Estelle3.6 Lotos3.7 ASN.15/17/20232形式化描述技术形式化描述技术：形式化描述技术：Why?v通信系统行为的复杂性增大了行为描述的难度，人们必须通信系统行为的复杂性增大了行为描述的难度，人们必须借助一种语言或一种技术来准确地描述系统行为。借助一种语言或一种技术来准确地描述系统行为。v在过

2、去，人们习惯使用自然语言进行协议描述（用自然语在过去，人们习惯使用自然语言进行协议描述（用自然语言写协议的规格说明或规范）言写协议的规格说明或规范）优点是：方便、易懂优点是：方便、易懂致命缺点是：不严格、不精确、结构不好、没有描述标准和有二义致命缺点是：不严格、不精确、结构不好、没有描述标准和有二义性性且很难进行协议实现、测试的自动化和协议验证。且很难进行协议实现、测试的自动化和协议验证。不同的人对协议描述的理解不一样导致不同的协议实现之间不能实不同的人对协议描述的理解不一样导致不同的协议实现之间不能实现互连，甚至还会得出错误的协议。现互连，甚至还会得出错误的协议。v解决办法：形式化技术解决办

3、法：形式化技术 FDTs(Formal Description Techniques)5/17/20233形式化描述技术FDTs：Aimsv采用形式描述技术的目的是：采用形式描述技术的目的是：为开发者提供一种分析的方法；为开发者提供一种分析的方法；作为对开发结果验证的基础；作为对开发结果验证的基础；为设计人员和应用人员提供交流途径；为设计人员和应用人员提供交流途径；作为开发文档能在将来再开发时使用。作为开发文档能在将来再开发时使用。v理想的形式描述技术应该既能描述系统的行为特征，又能进行理想的形式描述技术应该既能描述系统的行为特征，又能进行操作：操作：在系统需求分析和设计阶段，它应该是一种描述

4、语言在系统需求分析和设计阶段，它应该是一种描述语言在系统实现阶段它应该是一种编程语言。在系统实现阶段它应该是一种编程语言。v形式描述技术是将协议工程各阶段在技术上衔接起来的纽带，形式描述技术是将协议工程各阶段在技术上衔接起来的纽带，因此它对协议工程的发展起决定性作用。因此它对协议工程的发展起决定性作用。5/17/20234形式化描述技术FDTs：特性：特性v用于协议的用于协议的FDT一般应具有如下重要特性：一般应具有如下重要特性：完整的语法和语义定义完整的语法和语义定义 体系结构、服务和协议的可表达性体系结构、服务和协议的可表达性 协议重要特性协议重要特性(如，无死锁如，无死锁)的可分析性的可

5、分析性 支持复杂协议的管理支持复杂协议的管理(如，构造能力如，构造能力)支持逐步求精的方法支持逐步求精的方法 支持实现独立性支持实现独立性(包括并发性、非确定性和适当的抽象机包括并发性、非确定性和适当的抽象机制制)支持协议生命期的各环节，包括验证、实现和测试支持协议生命期的各环节，包括验证、实现和测试 支持自动或半自动设计、验证、实现和维护方法支持自动或半自动设计、验证、实现和维护方法 应能准确地描述进程交互的各种原语应能准确地描述进程交互的各种原语 5/17/20235形式化描述技术FDTs:Classificationv形式描述模型形式描述模型(FDM)状态变迁模型状态变迁模型有限状态机有

6、限状态机FSM(Finite State Machine)扩展的有限状态机扩展的有限状态机EFSM(Extended FSM)模型模型通信有限状态机通信有限状态机C CFSM(Communicating FSM)模型模型Carl Adam Petri的的Petri网网(PetriNet)时态逻辑时态逻辑TL(Temporal Logic)进程代数进程代数(Algebra of Process)R.Miler：通信系统演算通信系统演算CCS(Calculus of Communication System)（进程代数据的基础）（进程代数据的基础）Hoare：通信顺序进程通信顺序进程CSP(Com

7、municating Sequential Processes)（以（以CCS为基础）为基础）5/17/20236形式化描述技术FDTs:Classification(Cont.)v形式描述语言形式描述语言(FDL)ISO制定的制定的Estelle和和LOTOS CCITT制定的制定的SDL ISO的的ASN.1(抽象语法记法抽象语法记法)对象管理组织对象管理组织OMG制定的统一建模语言制定的统一建模语言UMLISO的的抽象测试集描述语言的抽象测试集描述语言的TTCN 高级程序设计语言，如高级程序设计语言，如Pascal,C,PL/1便于协议的实现便于协议的实现大多数比较复杂、分析起来比较困难

8、，且不支持非确大多数比较复杂、分析起来比较困难，且不支持非确定性的描述。定性的描述。5/17/20237形式化描述技术模型模型 vs.语言语言v模型模型含义一：对象或系统的抽象含义一：对象或系统的抽象OSI/RM：网络系统的抽象模型：网络系统的抽象模型含义二：描述对象或系统的方法或技术含义二：描述对象或系统的方法或技术FSMPetriNet5/17/20238形式化描述技术Functions vs.ComputationvFunctions specify only a relation between two sets of variables(input and output)vCompu

9、tations describe how the output Variables can be derived from the value of the input variables.5/17/20239形式化描述技术Model of ComputationvA MoC is a framework in which to express what sequence of actions must be taken to complete a computationvAn instance of a model of computation is a representation of

10、a function under a particular interpretation of its constituentsvNot necessarily a bijection(in fact almost never!)vExamples:Finite State Machine,Turing Machine,differential equation5/17/202310形式化描述技术模型模型 vs.语言（续）语言（续）v形式语言形式语言具有严格的语法和语义具有严格的语法和语义可以精确、完全地表述协议的功能、性能及行为等可以精确、完全地表述协议的功能、性能及行为等以一种或多种数学方

11、法或形式模型为基础以一种或多种数学方法或形式模型为基础SDL：基于扩展的基于扩展的FSM和抽象数据类型和抽象数据类型 Eetelle：基于扩展的：基于扩展的FSM，是，是Pascal语言的扩充语言的扩充LOTOS：基于通信系统演算（：基于通信系统演算（CCS）和抽象数据类型语）和抽象数据类型语言言ACT ONE 5/17/202311形式化描述技术模型模型 vs.语言（续）语言（续）v模型与语言的差别不是很明显。不同文献有不同的说模型与语言的差别不是很明显。不同文献有不同的说法。法。将模型与语言分开将模型与语言分开一些文献中的模型在另一些文献中成为语言或相反一些文献中的模型在另一些文献中成为语

12、言或相反将模型与语言不分，统称为形式化描述技术将模型与语言不分，统称为形式化描述技术v事实上，模型也可以看成是一种形式语言事实上，模型也可以看成是一种形式语言文法：描述语言的语法结构的形式规则（即语法规则）文法：描述语言的语法结构的形式规则（即语法规则）Turing 机机(无限自动机无限自动机)的能力相当于的能力相当于0型文法型文法有限自动机相当于正规文法（有限自动机相当于正规文法（3型文法）型文法）模型是语言的一个实例模型是语言的一个实例(Instance)（语义），例如（语义），例如C语言编语言编译器是译器是C语言的模型语言的模型5/17/202312形式化描述技术Models Of Co

13、mputation and languagesvNeed to distinguish between model and languagevLanguage needs to be expressive enough for application domain(write things once)have semantics in desired MOCvMOC needs to be powerful enough for application domainhave appropriate synthesis and validation algorithms5/17/202313形式

14、化描述技术FDTs:小结小结v实际应用时，往往是将多种形式描述技术混合起来实际应用时，往往是将多种形式描述技术混合起来使用。使用。例如：将协议中的主要状态用变迁用图形表示例如：将协议中的主要状态用变迁用图形表示(有限状态有限状态机或机或Petri网网)，而协议的其他细节则用高级语言描述。，而协议的其他细节则用高级语言描述。这样使得协议的描述和验证都比较方便。这样使得协议的描述和验证都比较方便。5/17/202314形式化描述技术第第 3 讲：协议形式化描述技术讲：协议形式化描述技术3.1 概述概述3.2 有限状态机有限状态机(FSM)3.3 PetriNet3.4 SDL3.5 Estelle

15、3.6 Lotos3.7 ASN.15/17/202315形式化描述技术Finite State Machines(FSMs)一、概一、概 述述5/17/202316形式化描述技术Finite State Machines(FSMs)inputeventsoutputscurrentstatenextstatestatetransitionfunctionvFinite state machines consist of:Output EventsInput Events(or Signals,or Messages)Transition Functions STATEStatesNEXTST

16、ATECURRENTSTATEINPUTEVENTSOUTPUTSTransitionFunction5/17/202317形式化描述技术Finite State Machine StatesinputeventsoutputscurrentstatenextstatestatetransitionfunctionvCurrent State State which determines the current behavior of the machinevNext State State which will machine have after processing an input e

17、vent.Next State can be same as currentvStart State State in which machine will be when created5/17/202318形式化描述技术FSM TransitionsinputeventsoutputscurrentstatenextstatestatetransitionfunctionvTriggered by input events the FSM moves from one state to other based on the Transition FunctionvTransition Fu

18、nction produces the Output and Next State depending on Current State and Input EventvWhile in particular state FSM is not active.It is waiting for an input to perform next activity5/17/202319形式化描述技术Finite State Machines(FSMs)二、形式化定义二、形式化定义5/17/202320形式化描述技术FSM:Formal DefinitionvFSM is 5-tuple:FSM=(S

19、,s0,I,F),whereS=s0,s1,sn:有限状态集合。在任一确定时刻，有限状态集合。在任一确定时刻，FSM只能处于一个确定的状态只能处于一个确定的状态si。I=a0,a1,am:有限输入字符集合。在任一确定的时刻，有限输入字符集合。在任一确定的时刻，FSM只能接收一个确定的输入只能接收一个确定的输入aj。：S I S是状态转换函数，如果在某一确定的时刻，是状态转换函数，如果在某一确定的时刻，FSM处于某一状态处于某一状态si S,并接收一个输入字符并接收一个输入字符aj I，那么下，那么下一时刻将处于一个确定的状态一时刻将处于一个确定的状态 s=(si,aj)S。在这里规定，。在这里

20、规定，s=(s,)，即对任何状态即对任何状态s，当读入空字符，当读入空字符 时，有很状态机时，有很状态机不发生任何状态转移。不发生任何状态转移。s0 S是初始状态，是初始状态，FSM由此状态开始接收输入由此状态开始接收输入F S是一个终态集（可空），是一个终态集（可空），FSM到达终态后不再接收输入到达终态后不再接收输入v确定有限状态机也称为确定有限状态机也称为DFA（确定有限自动机）（确定有限自动机）5/17/202321形式化描述技术Non deterministic FSM(or NFA)vNFSM is 5-tuple:FSM=(S,s0,I,F),whereS=s0,s1,sn:有限

21、状态集合。在任一确定时刻，有限状态集合。在任一确定时刻，FSM只只能处于一个确定的状态能处于一个确定的状态si。I=a0,a1,am:有限输入字符集合。在任一确定的时刻，有限输入字符集合。在任一确定的时刻，FSM只能接收一个确定的输入只能接收一个确定的输入aj。：S I 2S是状态转换函数，如果在某一确定的时刻，是状态转换函数，如果在某一确定的时刻，FSM处于某一状态处于某一状态si S,并接收一个输入字符并接收一个输入字符aj I，那么下，那么下一时刻将处于一个某一个状态子集一时刻将处于一个某一个状态子集=(si,aj)=p0,p1,pk(pi S,I=1,2,k)。在这里规定，。在这里规定

22、，s=(s,)，即对任何状态即对任何状态s，当读入空字符，当读入空字符 时，有很状态机不发生任何状态转移。时，有很状态机不发生任何状态转移。s0 S是初始状态，是初始状态，FSM由此状态开始接收输入由此状态开始接收输入F S是一个终态集（可空），是一个终态集（可空），FSM到达终态后不再接收输入到达终态后不再接收输入5/17/202322形式化描述技术FSM:Formal Definition(Cont.)v在一些情况下，如果讨论问题的重点集中在在一些情况下，如果讨论问题的重点集中在FSM的的状态集状态集(S)、输入集、输入集(I)和状态转换函数和状态转换函数()上。这上。这时可用如下两种方式

23、来表示时可用如下两种方式来表示FSM：FSM=(S,I,)或或FSM=(S,s0,I,)5/17/202323形式化描述技术Finite State Machines(FSMs)三、三、Representation5/17/202324形式化描述技术State Transition Diagrams(状态转换图状态转换图)vUsed to Visually represent an FSMvEmphasis is on identifying states and possible transitionsvCircles represent StatesvArrows represent Tr

24、ansitionsei are inputsxi are outputsS1S2e1/x1e1/x2e2/x4e2/x35/17/202325形式化描述技术FSM Tables(状态转换表状态转换表)vAll inputs,states,state transitions and outputs of a FSM can be listed in a Table formatinputeventsoutputscurrentstatenextstateS1S2S1S2x1x2x3x4S2e1e1e2e2S2S1S1vEach row of the table is one unique com

25、bination of Input Events and Current StatevFor complete definition of FSM all Event/State combinations shall be providedvTable is another way to represent an FSM with an emphasis on exploring all Event/State combinations5/17/202326形式化描述技术FSM Table-Compact FormvHere in the top row of the Table has a

26、list of all States while first column has a list of all Input Event.vTable Field on the intersection represents the transition function for the State,Event combinationvEach field contains list of outputs and next stateS1S2X1,S2X3,S1X2,S2e1e2X4,S1stateevent5/17/202327形式化描述技术Rocker Switch Examplev Eve

27、nts such as“switch on”and“switch off”may cause the machine to change state,as in the state diagram below for a light with a rocker switch.offonswitch on/make click soundswitch on/stay quietswitch off/make click soundswitch off/stay quietinputeventsoutputscurrentstatenextstateonoffonoff-clickclick-on

28、Switch onSwitch onSwitch offSwitch offonoffoffOnOff-click,offclick,onSwitch onSwitch off-stateeventvSome events dont cause a state transition at all,as in attempting to turn on a light that is already on.vBehaviour of the system in each state has to be defined:State ON-light is emitted out of bulb,S

29、tate OFF-no light emitted5/17/202328形式化描述技术FSM Example-TelephonevWhat are possible statesvWhat are possible events vCreate FSM TablevCreate State Transition DiagramvWhen we model an object we consider behavior which is of interest for us.vIn this case we will consider ability of phone to be used to

30、dial another subscriber,to be used to pass voice between subscribers and to be able to receive incoming calls.5/17/202329形式化描述技术Telephone StatesvFollowing States can be identifiedIDLE no calls in progress handset is on-hookDIALING handset is off-hook,but call is not in progressRINGINGhandset is on-h

31、ook,incoming call alertPATH ACTIVEhandset in off-hook and call is in progressvRelevant events are:off-hookUser takes handset off-hookon-hookUser places handset on-hookdial digitUser dials digitcall alertExchange alerts phone-incoming call5/17/202330形式化描述技术Telephone-FSM TableNote 1:if last digit in p

32、hone number is dialed lower option shall be selected“/“Unexpected event,“-”No State Change5/17/202331形式化描述技术Telephone-State Transition DiagramIDLEPATHACTIVEDIALINGOff-HookDialing ToneDial DigitRINGINGDial DigitOn-HookOn-HookOff-HookStop RingingThis is Starting stateCall AlertStart Ringing5/17/202332

33、形式化描述技术Timers&FSMsv Sometimes there is a need to perform some actions after some period of time.For that purpose timers are usedvTimers can be started specifying amount of time before time-out will happenvWhen time-out occurs the timer event will be sent to the FSM.Name of event is typically same as

34、 name of timervTimers can be stopped,so timer event is not generated5/17/202333形式化描述技术Telephone FSM Table with TimersNote 1:if last digit in phone number is dialed lower option shall be selected5/17/202334形式化描述技术Telephone STD with TimersIDLEPATHACTIVEDIALINGOff-HookDialing ToneDial DigitRINGINGDial

35、DigitOn-HookOn-HookOff-HookStop RingingThis is Starting stateCall AlertStart RingingT1Starting/Stopping of the Timersis not visible on STD.5/17/202335形式化描述技术Finite State Machines(FSMs)四、四、Moore 机机5/17/202336形式化描述技术Moore FSMv前面讨论的前面讨论的FSM和非确定和非确定FSM，可以看成仅接收输，可以看成仅接收输入并发生状态改变，但无任何输出的自动机器。入并发生状态改变，但无任何

36、输出的自动机器。v实际上生活中的许多有限状态系统对于不同的输入实际上生活中的许多有限状态系统对于不同的输入信号，除内部状态不断改变外，还不断向系统外部信号，除内部状态不断改变外，还不断向系统外部输出各种信号。输出各种信号。v具有输出的自动机器模型按照输出的不同分成两类：具有输出的自动机器模型按照输出的不同分成两类：Moore 机：输出与状态有关机：输出与状态有关Mealy机：输出与状态和输入有关机：输出与状态和输入有关5/17/202337形式化描述技术Moore FSM:Formal DefinitionvMoore FSM is 6-tuple:FSM=(S,s0,I,O,),whereS

37、=s0,s1,sn:有限状态集合。在任一确定时刻，有限状态集合。在任一确定时刻，FSM只能处于一个确定的状态只能处于一个确定的状态si。I=a0,a1,am:有限有限输入字符输入字符集合。在任一确定的时刻，集合。在任一确定的时刻，FSM只能接收一个确定的输入只能接收一个确定的输入aj。O=b0,b1,bn:有限有限输出字符输出字符集合。集合。：S I 2S是状态转换函数，如果在某一确定的时刻，是状态转换函数，如果在某一确定的时刻，FSM处于某一状态处于某一状态si S,并接收一个输入字符并接收一个输入字符aj I，那么下，那么下一时刻将处于一个确定的状态一时刻将处于一个确定的状态 s=(si,

38、aj)S。在这里规定，。在这里规定，s=(s,)，即对任何状态即对任何状态s，当读入空字符，当读入空字符 时，有很状态机时，有很状态机不发生任何状态转移。不发生任何状态转移。s0 S是初始状态，是初始状态，FSM由此状态开始接收输入由此状态开始接收输入：S O是输出函数是输出函数5/17/202338形式化描述技术Moore 机：机：Formal DefinitionvMoore机只是在接收输入串的过程中不断改变状态，机只是在接收输入串的过程中不断改变状态，并且在每个状态上有字符输出。例如：并且在每个状态上有字符输出。例如：对于输入串对于输入串a0,a1,an-1，设：，设：(s0,a0)=s

39、1,(s1,a1)=s2,.(sn-1,an-1)=sn这时输出序列为：这时输出序列为：(s0)(s1)(sn-1)5/17/202339形式化描述技术Moore 机机 vs.有限状态机有限状态机v有限状态机可看做是有限状态机可看做是Moore机的一个特例，机的一个特例，Why?v对于任何一个有限状态机对于任何一个有限状态机 M=(S,s0,I,F):引入输出字符集合引入输出字符集合 O=0,1，并定义，并定义S到到O的映射的映射 为：为：对于对于 s F,(s)=1；对于；对于s F,(s)=0v这样得到一个这样得到一个Moore机机 M=(S,s0,I,O,)，在，在该该Moore机中，输

40、出为机中，输出为1的状态为终结状态，输出的状态为终结状态，输出为为0的状态即为非终结状态。的状态即为非终结状态。5/17/202340形式化描述技术Finite State Machines(FSMs)五、五、Mealy 机机5/17/202341形式化描述技术Mealy FSM:Formal DefinitionvMealy FSM is 6-tuple:FSM=(S,s0,I,O,),whereS=s0,s1,sn:有限状态集合。在任一确定时刻，有限状态集合。在任一确定时刻，FSM只能处于一个确定的状态只能处于一个确定的状态si。I=a0,a1,am:有限有限输入字符输入字符集合。在任一确

41、定的时刻，集合。在任一确定的时刻，FSM只能接收一个确定的输入只能接收一个确定的输入aj。O=b0,b1,bn:有限有限输出字符输出字符集合。集合。：S I 2S是状态转换函数，如果在某一确定的时刻，是状态转换函数，如果在某一确定的时刻，FSM处于某一状态处于某一状态si S,并接收一个输入字符并接收一个输入字符aj I，那么下，那么下一时刻将处于一个确定的状态一时刻将处于一个确定的状态 s=(si,aj)S。在这里规定，。在这里规定，s=(s,)，即对任何状态即对任何状态s，当读入空字符，当读入空字符 时，有很状态机时，有很状态机不发生任何状态转移。不发生任何状态转移。s0 S是初始状态，是

42、初始状态，FSM由此状态开始接收输入由此状态开始接收输入：S I O是输出函数是输出函数5/17/202342形式化描述技术Moore 机：机：Formal DefinitionvMealy机只是在接收输入串的过程中不断改变状态，机只是在接收输入串的过程中不断改变状态，并且字符输出与当前状态有关。例如：并且字符输出与当前状态有关。例如：对于输入串对于输入串a0,a1,an-1，设：，设：(s0,a1)=s1,(s1,a2)=s2,.(sn-1,an-1)=sn这时输出序列为：这时输出序列为：(s0,a0)(s1,a1)(sn-1,an-1)5/17/202343形式化描述技术Mealy 机机

43、vs.Moore机机vMoore机可看做是机可看做是Mealy机的一个特例，机的一个特例，Why?v对于任何一个对于任何一个Moore机机 M=(S,s0,I,O,):设当输入串为设当输入串为a0,a1,an-1时，其输出序列为：时，其输出序列为：(s0)(s1)(sn)，其中，其中si 和和ai-1 满足：满足：(si-1,ai-1)=si，1 i n 引入：引入：S I 到到O的映射的映射 ：(si-1,ai-1)=(si-1,ai-1)=(si),1 i n v这样得到一个这样得到一个Mealy机机 M=(S,s0,I,O,)，对于，对于输入串输入串a0,a1,an-1，Mealy机机M

44、 的输出为的输出为 为：为：(s0,a0)(s1,a1)(sn-1,an-1)=(s0)(s1)(sn-1)5/17/202344形式化描述技术Mealy机：机：Examplev停止等待协议：停止等待协议：设甲、乙双方进行半双工通信，甲发信息帧，乙回送确设甲、乙双方进行半双工通信，甲发信息帧，乙回送确认帧。双方约定采用停止等待协议，因此甲方仅需用认帧。双方约定采用停止等待协议，因此甲方仅需用1比比特来编号。特来编号。将将0号帧和号帧和1号帧分别记为号帧分别记为0和和1。当收到有差错的帧时，则丢弃此帧，同时不发任何应答当收到有差错的帧时，则丢弃此帧，同时不发任何应答帧。帧。当收到无差错的帧但序号

45、不正确时，要发确认帧，同时当收到无差错的帧但序号不正确时，要发确认帧，同时要丢弃此帧，不送主机。要丢弃此帧，不送主机。我们还假定收方在准备发送确认帧我们还假定收方在准备发送确认帧ACK时，暂不接收外时，暂不接收外面发来的帧。面发来的帧。5/17/202345形式化描述技术停止等待协议：状态变迁表停止等待协议：状态变迁表5/17/202346形式化描述技术停止等待协议：状态变迁图停止等待协议：状态变迁图12341234等待等待准备发准备发ACK准备发准备发ACK准备发准备发0准备发准备发1期望收期望收1期望收期望收0等待等待发发0发发1收收1收收0发发ACK发发ACK收收ACK收收ACK发发AC

46、K收收1发发ACK收收0甲方甲方乙方乙方超超时时超超时时状态状态符号符号状态状态编号编号状态状态含义含义状态状态变迁变迁输入输入事件事件对某些状态进行了简化。对某些状态进行了简化。例如，当乙方处于例如，当乙方处于“期期望收望收0”的状态时，若的状态时，若收到无差错的收到无差错的1帧，仍帧，仍然应当先进入然应当先进入“准备发准备发ACK”状态，然后才发出状态，然后才发出 ACK。但这里就将。但这里就将“收收1”与与“发发ACK”合并合并成为一个事件。成为一个事件。再例如，当乙方处于再例如，当乙方处于“期望收期望收1”的状态时，的状态时，若收到无差错的若收到无差错的0帧，帧，仍然应当先进入仍然应当

47、先进入“准备准备发发ACK”状态，然后才发状态，然后才发出出 ACK。但这里就将。但这里就将“收收0”与与“发发ACK”合合并成为一个事件。并成为一个事件。5/17/202347形式化描述技术停止等待协议：状态变迁图合并停止等待协议：状态变迁图合并v前面描述的甲、乙两方各自的有限状态机实际上并非前面描述的甲、乙两方各自的有限状态机实际上并非独立地工作而是协调在一起工作的。如合在一起用一独立地工作而是协调在一起工作的。如合在一起用一个有限状态机来描述整个系统，将会更加清楚。但这个有限状态机来描述整个系统，将会更加清楚。但这将导致状态数目将大大增加。将导致状态数目将大大增加。Why?甲方和乙方的状

48、态各有甲方和乙方的状态各有4 4个，个，而信道上的状态也有而信道上的状态也有4 4个个(即：信道上传送即：信道上传送00，传送，传送11，传送传送ACKACK，以及出现差错或帧的丢失，以及出现差错或帧的丢失)。这样将总共有这样将总共有4 43 3=64=64种状态，用状态图很难清楚地表示出来。种状态，用状态图很难清楚地表示出来。v解决办法：合并一些状态解决办法：合并一些状态,即考虑一些次要的细节即考虑一些次要的细节 5/17/202348形式化描述技术停止等待协议：状态变迁图合并停止等待协议：状态变迁图合并v状态合并：状态合并：甲方的状态甲方的状态1 1和状态和状态2 2，状态，状态3 3和状

49、态和状态4 4都可以合并，都可以合并，乙的状态乙的状态1 1和状态和状态4 4，状态，状态2 2和状态和状态3 3也可进行合并。也可进行合并。信道的状态是由其内容决定的，例如，如果帧信道的状态是由其内容决定的，例如，如果帧00正在信道正在信道上上(即，帧已被分地发送出去，部分地被接收，但在目的主即，帧已被分地发送出去，部分地被接收，但在目的主机上还未进行处理机上还未进行处理)，则信道的状态为帧，则信道的状态为帧00。整个系统的状态是通信双方两个协议机和信道的所有状态整个系统的状态是通信双方两个协议机和信道的所有状态的组合。的组合。用用3个字符个字符 XYZ 表示整个系统的状态，其中表示整个系统

50、的状态，其中 X=0或或1，对应于甲方准备发，对应于甲方准备发0或或1(包括发完后等包括发完后等待待ACK的状态的状态)；Y=0或或1，对应于乙方期望收到，对应于乙方期望收到0或或1；Z=0,1,A或或 ，对应于信道上传送的是，对应于信道上传送的是0，1，ACK 或出现了差错或出现了差错(包括丢失包括丢失)。5/17/202349形式化描述技术停止等待协议：合并后的状态变迁图停止等待协议：合并后的状态变迁图变迁变迁 意义意义 0 帧丢失或帧出错帧丢失或帧出错 1 收收0，发，发 ACK，送主机，送主机 2 收收 ACK，发，发1 3 收收1，发，发 ACK，送主机，送主机 4 收收 ACK，发