《协议形式化描述技术1概述及FSM》由会员分享，可在线阅读，更多相关《协议形式化描述技术1概述及FSM（88页珍藏版）》请在金锄头文库上搜索。
1、南京邮电大学南京邮电大学第第 3 章章 协议形式化描述技术协议形式化描述技术1-概述及概述及FSM第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) 内容提要内容提要概述概述1FSM22第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) 形式化描述技术：形式化描述技术：Why?v通信系统行为的复杂性增大了行为描述的难度，人们必须通信系统行为的复杂性增大了行为描述的难度，人们必须借助一种语言或一种技术来准确地描述系统行为。借助一种语言或一种技术来准确地描述系统行为。v在过去，人们习惯使用自然语言进行协议描述用自然语在过去，人们习惯使用自然语言进行协议描
2、述用自然语言写协议的规格说明或标准言写协议的规格说明或标准v优点是：方便、易懂优点是：方便、易懂v致命缺点是：不严格、不精确、结构不好、没有描述标准致命缺点是：不严格、不精确、结构不好、没有描述标准和有二义性和有二义性v且很难进行协议实现、测试的自动化和协议验证。且很难进行协议实现、测试的自动化和协议验证。 v不同的人对协议描述的理解不一样导致不同的协议实现之不同的人对协议描述的理解不一样导致不同的协议实现之间不能实现互连，甚至还会得出错误的协议。间不能实现互连，甚至还会得出错误的协议。 v解决方法：形式化技术解决方法：形式化技术 FDTs (Formal Description Techni
3、ques)3第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) FDTs：Aimsv采用形式描述技术的目的是：采用形式描述技术的目的是：v为开发者提供一种分析的方法；为开发者提供一种分析的方法；v作为对开发结果验证的根底；作为对开发结果验证的根底；v为设计人员和应用人员提供交流途径；为设计人员和应用人员提供交流途径；v作为开发文档能在将来再开发时使用。作为开发文档能在将来再开发时使用。 v理想的形式描述技术应该既能描述系统的行为特征，又能理想的形式描述技术应该既能描述系统的行为特征，又能进行操作：进行操作：v在系统需求分析和设计阶段，它应该是一种描述语言在系统需求分析和设
4、计阶段，它应该是一种描述语言v在系统实现阶段它应该是一种编程语言。在系统实现阶段它应该是一种编程语言。 v形式描述技术是将协议工程各阶段在技术上衔接起来的纽形式描述技术是将协议工程各阶段在技术上衔接起来的纽带，因此它对协议工程的开展起决定性作用。带，因此它对协议工程的开展起决定性作用。 4第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) FDTs：特性：特性v用于协议的用于协议的FDT一般应具有如下重要特性：一般应具有如下重要特性： v完整的语法和语义定义完整的语法和语义定义 v体系结构、效劳和协议的可表达性体系结构、效劳和协议的可表达性 v协议重要特性协议重要特性(如
5、，无死锁如，无死锁)的可分析性的可分析性 v支持复杂协议的管理支持复杂协议的管理(如，构造能力如，构造能力) v支持逐步求精的方法支持逐步求精的方法 v支持实现独立性支持实现独立性(包括并发性、非确定性和适包括并发性、非确定性和适当的抽象机制当的抽象机制) v支持协议生命期的各环节，包括验证、实现和支持协议生命期的各环节，包括验证、实现和测试测试 v支持自动或半自动设计、验证、实现和维护方支持自动或半自动设计、验证、实现和维护方法法 v应能准确地描述进程交互的各种原语应能准确地描述进程交互的各种原语 5第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) FDTs: Cla
6、ssificationv形式描述模型形式描述模型(FDM) (FDM) v状态变迁模型状态变迁模型v有限状态机有限状态机FSM(Finite State Machine)FSM(Finite State Machine)v扩展的有限状态机扩展的有限状态机EFSM(Extended FSM)EFSM(Extended FSM)模型模型v通信有限状态机通信有限状态机CFSM(Communicating FSM)CFSM(Communicating FSM)模型模型vCarl Adam PetriCarl Adam Petri的的PetriPetri网网(PetriNet)(PetriNet)v时态
7、逻辑时态逻辑TL(Temporal Logic)TL(Temporal Logic)v进程代数进程代数(Algebra of Process) (Algebra of Process) v R.Miler R.Miler：通信系统演算：通信系统演算CCS (Calculus of CCS (Calculus of Communication System)Communication System)进程代数据的根底进程代数据的根底v Hoare Hoare：通信顺序进程：通信顺序进程CSP (Communicating CSP (Communicating Sequential Processe
8、s)Sequential Processes)以以CCSCCS为根底为根底6第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) FDTs: Classification (Cont.)v形式描述语言形式描述语言(FDL) (FDL) vISOISO制定的制定的EstelleEstelle和和LOTOS LOTOS vCCITTCCITT制定的制定的SDL SDL vISOISO的的ASN.1(ASN.1(抽象语法记法抽象语法记法) )v对象管理组织对象管理组织OMGOMG制定的统一建模语言制定的统一建模语言UMLUMLvISOISO的抽象测试集描述语言的的抽象测试集描述语
9、言的TTCN TTCN v高级程序设计语言，如高级程序设计语言，如Pascal, C, PL/1Pascal, C, PL/1v便于协议的实现便于协议的实现v大多数比较复杂、分析起来比较困难，且不支大多数比较复杂、分析起来比较困难，且不支持非确定性的描述。持非确定性的描述。 7第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) 模型模型 vs. 语言语言v模型模型含义一：对象或系统的抽象含义一：对象或系统的抽象OSI/RM：网络系统的抽象模型：网络系统的抽象模型含义二：描述对象或系统的方法或技术含义二：描述对象或系统的方法或技术FSMPetriNet8第第3章章 协议形式
10、化描述技术协议形式化描述技术(1概述及概述及FSM) Functions vs. ComputationvFunctions specify only a relation between two sets of variables (input and output)vComputations describe how the output Variables can be derived from the value of the input variables.9第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) Model of ComputationvA MoC
11、 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 a function under a particular interpretation of its constituentsvNot necessarily a bijection (in fact almost never!)vExamples: Finite Stat
12、e Machine, Turing Machine, differential equation10第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) 模型模型 vs. 语言续语言续v形式语言形式语言v具有严格的语法和语义具有严格的语法和语义v可以精确、完全地表述协议的功能、性能及行为可以精确、完全地表述协议的功能、性能及行为等等v以一种或多种数学方法或形式模型为根底以一种或多种数学方法或形式模型为根底vSDL：基于扩展的：基于扩展的FSM和抽象数据类型和抽象数据类型 vEetelle：基于扩展的：基于扩展的FSM，是，是Pascal语言的扩充语言的扩充vLOTOS：基于
13、通信系统演算：基于通信系统演算CCS和抽象数据和抽象数据类型语言类型语言ACT ONE 11第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) 模型模型 vs. 语言续语言续v模型与语言的差异不是很明显。不同文献有不同模型与语言的差异不是很明显。不同文献有不同的说法。的说法。v将模型与语言分开将模型与语言分开v一些文献中的模型在另一些文献中成为语言或相一些文献中的模型在另一些文献中成为语言或相反反v将模型与语言不分，统称为形式化描述技术将模型与语言不分，统称为形式化描述技术v事实上，模型也可以看成是一种形式语言事实上，模型也可以看成是一种形式语言v文法：描述语言的语法结构
14、的形式规那么即语文法：描述语言的语法结构的形式规那么即语法规那么法规那么vTuring 机机(无限自动机无限自动机)的能力相当于的能力相当于0型文法型文法v有限自动机相当于正规文法有限自动机相当于正规文法3型文法型文法v模型是语言的一个实例模型是语言的一个实例(Instance)语义，例语义，例如如C语言编译器是语言编译器是C语言的模型语言的模型12第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) Models Of Computation and languagesvNeed to distinguish between model and languagevLang
15、uage 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 algorithms13第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) FDTs: 小结小结v实际应用时，往往是将多种形式描述技术混合起实际应用时，往往是将多种形式描述
16、技术混合起来使用。来使用。 v例如：将协议中的主要状态用变迁用图形表示例如：将协议中的主要状态用变迁用图形表示( (有有限状态机或限状态机或PetriPetri网网) )，而协议的其他细节那么用，而协议的其他细节那么用高级语言描述。这样使得协议的描述和验证都比高级语言描述。这样使得协议的描述和验证都比较方便。较方便。 14第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) 内容提要内容提要概述概述1FSM215第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) Finite State Machines (FSMs)一、概一、概 述述16第第3章章
17、协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) Finite State Machines (FSMs)inputeventsoutputscurrentstatenextstatestatetransitionfunctionvFinite state machines consist of:Output EventsInput Events (or Signals, or Messages)Transition Functions STATEStatesNEXTSTATECURRENTSTATEINPUTEVENTSOUTPUTSTransitionFunction17第第3
18、章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) Finite State Machine StatesinputeventsoutputscurrentstatenextstatestatetransitionfunctionvCurrent State State which determines the current behavior of the machinevNext State State which will machine have after processing an input event. Next State can be same as cur
19、rentvStart State State in which machine will be when created18第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) FSM TransitionsinputeventsoutputscurrentstatenextstatestatetransitionfunctionvTriggered by input events the FSM moves from one state to other based on the Transition FunctionvTransition Function produc
20、es 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 activity19第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) Finite State Machines (FSMs)二、形式化定义二、形式化定义20第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) FSM: Formal
21、DefinitionvFSM is 5-tuple: FSM = (S, s0, I, , F), wherevS = s0, s1, , sn: 有限状态集合。在任一确定时有限状态集合。在任一确定时刻，刻，FSM只能处于一个确定的状态只能处于一个确定的状态si。vI = a0, a1, , am: 有限输入字符集合。在任一确有限输入字符集合。在任一确定的时刻，定的时刻，FSM只能接收一个确定的输入只能接收一个确定的输入aj。v ：S I S是状态转换函数，如果在某一确定是状态转换函数，如果在某一确定的时刻，的时刻，FSM处于某一状态处于某一状态si S, 并接收一个输并接收一个输入字符入字符
22、aj I，那么下一时刻将处于一个确定的状，那么下一时刻将处于一个确定的状态态 s = (si , aj) S。在这里规定，。在这里规定，s = (s , )，即对任何状态，即对任何状态s，当读入空字符，当读入空字符时，有很状态时，有很状态机不发生任何状态转移。机不发生任何状态转移。vs0 S是初始状态，是初始状态，FSM由此状态开始接收输入由此状态开始接收输入vF S是一个终态集可空，是一个终态集可空，FSM到达终态后不到达终态后不再接收输入再接收输入v确定有限状态机也称为确定有限状态机也称为DFA确定有限自动机确定有限自动机21第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及
23、FSM) Non deterministic FSM (or NFA)vNFSM is 5-tuple: FSM = (S, s0, I, , F), wherevS = s0, s1, , sn: 有限状态集合。在任一确定时有限状态集合。在任一确定时刻，刻，FSM只能处于一个确定的状态只能处于一个确定的状态si。vI = a0, a1, , am: 有限输入字符集合。在任一确有限输入字符集合。在任一确定的时刻，定的时刻，FSM只能接收一个确定的输入只能接收一个确定的输入aj。v ：S I 2S是状态转换函数，如果在某一确是状态转换函数，如果在某一确定的时刻，定的时刻，FSM处于某一状态处于某
24、一状态si S, 并接收一个并接收一个输入字符输入字符aj I，那么下一时刻将处于一个某一个，那么下一时刻将处于一个某一个状态子集状态子集= (si , aj) = p0, p1, , pk(pi S, I=1,2,k)。在这里规定，。在这里规定，s = (s , )，即对任何，即对任何状态状态s，当读入空字符，当读入空字符时，有很状态机不发生任时，有很状态机不发生任何状态转移。何状态转移。vs0 S是初始状态，是初始状态，FSM由此状态开始接收输入由此状态开始接收输入vF S是一个终态集可空，是一个终态集可空，FSM到达终态后不到达终态后不再接收输入再接收输入22第第3章章 协议形式化描述技
25、术协议形式化描述技术(1概述及概述及FSM) FSM: Formal Definition (Cont.)v在一些情况下，如果讨论问题的重点集中在在一些情况下，如果讨论问题的重点集中在FSM的状态集的状态集(S)、输入集、输入集(I)和状态转换函数和状态转换函数( )上。上。这时可用如下两种方式来表示这时可用如下两种方式来表示FSM：FSM = (S, I, )或或FSM = (S, s0, I, )23第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) Finite State Machines (FSMs)三、三、Representation24第第3章章 协议形式化
26、描述技术协议形式化描述技术(1概述及概述及FSM) State Transition DiagramsvUsed to Visually represent an FSMvEmphasis is on identifying states and possible transitionsvCircles represent StatesvArrows represent Transitionsei are inputsxi are outputsS1S2e1/x1e1/x2e2/x4e2/x325第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) FSM Tables (
27、状态转换表状态转换表)vAll inputs, states, state transitions and outputs of a FSM can be listed in a Table formatinputeventsoutputscurrentstatenextstateS1S2S1S2x1x2x3x4S2e1e1e2e2S2S1S1vEach row of the table is one unique combination of Input Events and Current StatevFor complete definition of FSM all Event/Sta
28、te combinations shall be providedvTable is another way to represent an FSM with an emphasis on exploring all Event/State combinations26第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) FSM Table - Compact FormvHere in the top row of the Table has a list of all States while first column has a list of all Input Ev
29、ent.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,S1stateevent27第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) Rocker Switch Examplev Events such as “switch on and “switch off may
30、 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-onSwitch onSwitch onSwitch offSwitch offo
31、noffoffOnOff-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, State OFF - no light emitted28第第3章章
32、 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) 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 dial ano
33、ther subscriber, to be used to pass voice between subscribers and to be able to receive incoming calls.29第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) Telephone StatesvFollowing States can be identifiedIDLE no calls in progress handset is on-hookDIALING handset is off-hook, but call is not in progressRINGING
34、handset is on-hook, 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 call30第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) Telep
35、hone - FSM TableNote 1: if last digit in phone number is dialed lower option shall be selected“/“ Unexpected event, “- No State Change31第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) Telephone - State Transition DiagramIDLEPATHACTIVEDIALINGOff-HookDialing ToneDial DigitRINGINGDial DigitOn-HookOn-HookOff-HookS
36、top RingingThis is Starting stateCall AlertStart Ringing32第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) 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
37、 time-out occurs the timer event will be sent to the FSM. Name of event is typically same as name of timervTimers can be stopped, so timer event is not generated33第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) Telephone FSM Table with TimersNote 1: if last digit in phone number is dialed lower option shall be
38、 selected34第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) Telephone STD with TimersIDLEPATHACTIVEDIALINGOff-HookDialing ToneDial DigitRINGINGDial DigitOn-HookOn-HookOff-HookStop RingingThis is Starting stateCall AlertStart RingingT1Starting/Stopping of the Timersis not visible on STD. 35第第3章章 协议形式化描述技术协议形式化描述
39、技术(1概述及概述及FSM) Finite State Machines (FSMs)四、四、Moore 机机36第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) Moore FSMv前面讨论的前面讨论的FSM和非确定和非确定FSM，可以看成仅接收，可以看成仅接收输入并发生状态改变，但无任何输出的自动机器。输入并发生状态改变，但无任何输出的自动机器。v实际上生活中的许多有限状态系统对于不同的输实际上生活中的许多有限状态系统对于不同的输入信号，除内部状态不断改变外，还不断向系统入信号，除内部状态不断改变外，还不断向系统外部输出各种信号。外部输出各种信号。v具有输出的自动机
40、器模型按照输出的不同分成两具有输出的自动机器模型按照输出的不同分成两类：类：Moore 机：输出与状态有关机：输出与状态有关Mealy机：输出与状态和输入有关机：输出与状态和输入有关37第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) Moore FSM: Formal DefinitionvMoore FSM is 6-tuple: FSM = (S, s0, I, O, , ), whereS = s0, s1, , sn: 有限状态集合。在任一确定时刻，有限状态集合。在任一确定时刻，FSM只能处于一个确定的状态只能处于一个确定的状态si。I = a0, a1, ,
41、 am: 有限有限输入字符输入字符集合。在任一确定的集合。在任一确定的时刻，时刻，FSM只能接收一个确定的输入只能接收一个确定的输入aj。O = b0, b1, , bn: 有限有限输出字符输出字符集合。集合。 ：S I 2S是状态转换函数，如果在某一确定的时是状态转换函数，如果在某一确定的时刻，刻，FSM处于某一状态处于某一状态si S, 并接收一个输入字符并接收一个输入字符aj I，那么下一时刻将处于一个确定的状态，那么下一时刻将处于一个确定的状态 s = (si , aj) S。在这里规定，。在这里规定，s = (s , )，即对任何状态即对任何状态s，当读入，当读入空字符空字符 时，有
42、很状态机不发生任何状态转移。时，有很状态机不发生任何状态转移。s0 S是初始状态，是初始状态，FSM由此状态开始接收输入由此状态开始接收输入 ：S O是输出函数是输出函数38第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) Moore 机：机： Formal DefinitionvMoore机只是在接收输入串的过程中不断改变状机只是在接收输入串的过程中不断改变状态，并且在每个状态上有字符输出。例如：态，并且在每个状态上有字符输出。例如：对于输入串对于输入串a0, a1, , an-1，设：，设： (s0 , a0) = s1, (s1 , a1) = s2, . (sn
43、-1 , an-1) = sn这时输出序列为：这时输出序列为： (s0) (s1) (sn-1)39第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) 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机机
44、M = (S, s0, I, O, , )，在，在该该Moore机中，输出为机中，输出为1的状态为终结状态，输出的状态为终结状态，输出为为0的状态即为非终结状态。的状态即为非终结状态。40第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) Finite State Machines (FSMs)五、五、Mealy 机机41第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) Mealy FSM: Formal DefinitionvMealy FSM is 6-tuple: FSM = (S, s0, I, O, , ), whereS = s0, s
45、1, , sn: 有限状态集合。在任一确定时刻，有限状态集合。在任一确定时刻，FSM只能处于一个确定的状态只能处于一个确定的状态si。I = a0, a1, , am: 有限有限输入字符输入字符集合。在任一确定的集合。在任一确定的时刻，时刻，FSM只能接收一个确定的输入只能接收一个确定的输入aj。O = b0, b1, , bn: 有限有限输出字符输出字符集合。集合。 ：S I 2S是状态转换函数，如果在某一确定的时是状态转换函数，如果在某一确定的时刻，刻，FSM处于某一状态处于某一状态si S, 并接收一个输入字符并接收一个输入字符aj I，那么下一时刻将处于一个确定的状态，那么下一时刻将处
46、于一个确定的状态 s = (si , aj) S。在这里规定，。在这里规定，s = (s , )，即对任何状态即对任何状态s，当读入，当读入空字符空字符 时，有很状态机不发生任何状态转移。时，有很状态机不发生任何状态转移。s0 S是初始状态，是初始状态，FSM由此状态开始接收输入由此状态开始接收输入 ：S I O是输出函数是输出函数42第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) Moore 机：机： Formal DefinitionvMealy机只是在接收输入串的过程中不断改变状态，机只是在接收输入串的过程中不断改变状态，并且字符输出与当前状态有关。例如：并且字
47、符输出与当前状态有关。例如：对于输入串对于输入串a0, a1, , an-1，设：，设： (s0 , a1) = s1, (s1 , a2) = s2, . (sn-1 , an-1) = sn这时输出序列为：这时输出序列为： (s0, a0) (s1 , a1) (sn-1 , an-1)43第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) Mealy 机机 vs. Moore机机vMoore机可看做是机可看做是Mealy机的一个特例，机的一个特例，Why?v对于任何一个对于任何一个Moore机机 M = (S, s0, I, O, , ) :设当输入串为设当输入串为
48、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 的输出为的输出为 为：为： (s0, a0) (s1, a1) (sn-1, an-1) = (s0) (s1) (sn-1)
49、44第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) Mealy机：机：Examplev停止等待协议：停止等待协议：v设甲、乙双方进行半双工通信，甲发信息帧，乙设甲、乙双方进行半双工通信，甲发信息帧，乙回送确认帧。双方约定采用停止等待协议，因此回送确认帧。双方约定采用停止等待协议，因此甲方仅需用甲方仅需用1比特来编号。比特来编号。v将将0号帧和号帧和1号帧分别记为号帧分别记为0和和1。v当收到有过失的帧时，那么丢弃此帧，同时不发当收到有过失的帧时，那么丢弃此帧，同时不发任何应答帧。任何应答帧。v当收到无过失的帧但序号不正确时，要发确认帧，当收到无过失的帧但序号不正确时，
50、要发确认帧，同时要丢弃此帧，不送主机。同时要丢弃此帧，不送主机。v我们还假定收方在准备发送确认帧我们还假定收方在准备发送确认帧ACK时，暂不时，暂不接收外面发来的帧。接收外面发来的帧。 45第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) 停止等待协议：状态变迁表停止等待协议：状态变迁表46第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) 停止等待协议：状态变迁图停止等待协议：状态变迁图12341234等待等待准备发准备发ACK准备发准备发ACK准备发准备发0准备发准备发1期望收期望收1期望收期望收0等待等待发发0发发1收收1收收0发发ACK发发
51、ACK收收ACK收收ACK发发ACK收收1发发ACK收收0甲方甲方乙方乙方超超时时超超时时状态状态符号符号状态状态编号编号状态状态含义含义状态状态变迁变迁输入输入事件事件对某些状态进行了简对某些状态进行了简化。例如，当乙方处化。例如，当乙方处于于“期望收期望收00的状的状态时，假设收到无过态时，假设收到无过失的失的11帧，仍然应领帧，仍然应领先进入先进入“准备发准备发ACKACK状态，然后才发出状态，然后才发出 ACKACK。但这里就将。但这里就将“收收11与与“发发ACKACK合合并成为一个事件。并成为一个事件。 再例如，当乙方处于再例如，当乙方处于“期望收期望收11的状态的状态时，假设收到
52、无过失时，假设收到无过失的的00帧，仍然应领先帧，仍然应领先进入进入“准备发准备发ACKACK状状态，然后才发出态，然后才发出 ACK ACK。但这里就将但这里就将“收收00与与“发发ACKACK合并成为合并成为一个事件。一个事件。 47第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) 停止等待协议：状态变迁图合并停止等待协议：状态变迁图合并v前面描述的甲、乙两方各自的有限状态机实际上并前面描述的甲、乙两方各自的有限状态机实际上并非独立地工作而是协调在一起工作的。如合在一起非独立地工作而是协调在一起工作的。如合在一起用一个有限状态机来描述整个系统，将会更加清楚。用一个有
53、限状态机来描述整个系统，将会更加清楚。但这将导致状态数目将大大增加。但这将导致状态数目将大大增加。Why?Why?v甲方和乙方的状态各有甲方和乙方的状态各有4 4个，个，v而信道上的状态也有而信道上的状态也有4 4个个( (即：信道上传送即：信道上传送00，传，传送送11，传送，传送ACKACK，以及出现过失或帧的丧失，以及出现过失或帧的丧失) )。v这样将总共有这样将总共有43=6443=64种状态，用状态图很难清楚地种状态，用状态图很难清楚地表示出来。表示出来。v解决方法：合并一些状态解决方法：合并一些状态, ,即考虑一些次要的细节即考虑一些次要的细节 48第第3章章 协议形式化描述技术协
54、议形式化描述技术(1概述及概述及FSM) 停止等待协议：状态变迁图合并停止等待协议：状态变迁图合并v状态合并：状态合并：v甲方的状态甲方的状态1 1和状态和状态2 2，状态，状态3 3和状态和状态4 4都可以合并，都可以合并， v乙的状态乙的状态1 1和状态和状态4 4，状态，状态2 2和状态和状态3 3也可进行合并。也可进行合并。v信道的状态是由其内容决定的，例如，如果帧信道的状态是由其内容决定的，例如，如果帧00正在信道上正在信道上( (即，帧已被分地发送出去，局部即，帧已被分地发送出去，局部地被接收，但在目的主机上还未进行处理地被接收，但在目的主机上还未进行处理) )，那，那么信道的状态
55、为帧么信道的状态为帧00。 v整个系统的状态是通信双方两个协议机和信道的整个系统的状态是通信双方两个协议机和信道的所有状态的组合。用所有状态的组合。用3 3个字符个字符 XYZ XYZ 表示整个系统表示整个系统的状态，其中的状态，其中v X = 0 X = 0或或1 1，对应于甲方准备发，对应于甲方准备发00或或1(1(包括发包括发完后等待完后等待ACKACK的状态的状态) )；v Y = 0 Y = 0或或1 1，对应于乙方期望收到，对应于乙方期望收到00或或11；v Z = 0, 1, A Z = 0, 1, A或或 ，对应于信道上传送的是，对应于信道上传送的是00，11，ACK ACK
56、或出现了过失或出现了过失( (包括丧失包括丧失) )。 49第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) 停止等待协议：合并后的状态变迁图停止等待协议：合并后的状态变迁图变迁变迁 意义意义 0 帧丧失或帧出错帧丧失或帧出错 1 收收0，发，发 ACK，送主机，送主机 2 收收 ACK，发，发1 3 收收1，发，发 ACK，送主机，送主机 4 收收 ACK，发，发0 5 收收0，发，发 ACK，不送主机，不送主机 6 收收1，发，发 ACK，不送主机，不送主机 7 超时，发超时，发0 8 超时，发超时，发100000012345678870 0 00 1 01 1 1
57、1 0 11 0 1 1 0 1 0 0 1 0 A0 1 A假设系统一开始处在假设系统一开始处在(000)(000)状态。这表示甲发完状态。这表示甲发完00，乙期望收到，乙期望收到00，而信道上传送的也是，而信道上传送的也是00。在无过失的情况下，系统的状态仅在。在无过失的情况下，系统的状态仅在4 4个状态中循环：个状态中循环：(000)(01A)(111)(10A)(000)(000)(01A)(111)(10A)(000)。如果信道丧失了帧。如果信道丧失了帧00，那么进行从状态，那么进行从状态(000)(000)到状态到状态(00-)(00-)的转换。最终，发送过程超时的转换。最终，发送
58、过程超时( (转换转换7)7)，且系统回到状态，且系统回到状态(000)(000)。确认帧的丧失。确认帧的丧失更为复杂，需要两种转换：更为复杂，需要两种转换：7 7和和5 5，或，或8 8和和6 6，直到修复损坏。从理论上讲，应当共有，直到修复损坏。从理论上讲，应当共有2 22 24 4 = 16= 16种不同的状态。去掉没有意义的组合后，还剩下种不同的状态。去掉没有意义的组合后，还剩下1010种状态，而导致状态变迁的输入事种状态，而导致状态变迁的输入事件共有件共有9 9种种( (标号标号0 0 8)8)。 50第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) 停止等待
59、协议：停止等待协议：Summaryv当描述比较复杂的协议时，状态的数目将急剧增当描述比较复杂的协议时，状态的数目将急剧增加，以致很难用它来清晰地描述协议。加，以致很难用它来清晰地描述协议。 v例如，如果我们将前面描述的半双工通信的停止例如，如果我们将前面描述的半双工通信的停止等待协议改为全双工通信的停止等待协议，那么等待协议改为全双工通信的停止等待协议，那么其状态图就要复杂多了其状态图就要复杂多了51第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) 全双工通信的停止等待协议状态变迁图全双工通信的停止等待协议状态变迁图52第第3章章 协议形式化描述技术协议形式化描述技术(
60、1概述及概述及FSM) Finite State Machines (FSMs)七、七、FSM的简化的简化53第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) FSM的简化的简化v当协议复杂时，状态太多难于描述和理解，如何当协议复杂时，状态太多难于描述和理解，如何减少状态数？减少状态数？状态层次化状态层次化使用原子过程使用原子过程使用协议变量使用协议变量隐藏内部协同事件隐藏内部协同事件简化通道简化通道FSMFSM54第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) Finite State Machines (FSMs)八、八、FSM的错误模型的
61、错误模型55第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) FSM的简化的简化v当协议复杂时，状态太多难于描述和理解，如何当协议复杂时，状态太多难于描述和理解，如何减少状态数？减少状态数？状态层次化状态层次化使用原子过程使用原子过程使用协议变量使用协议变量隐藏内部协同事件隐藏内部协同事件简化通道简化通道FSMFSM56第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) FSM的简化的简化v如何从图中发现协议错误？如何从图中发现协议错误？v使用可达性分析使用可达性分析死锁死锁活锁活锁无限分支无限分支不可达状态不可达状态全局状态全局状态无限分支无限分
62、支死锁死锁不可达状态不可达状态活锁活锁图3-4 有限状态机的错误模型57第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) Finite State Machines (FSMs)九、九、EFSM58第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) Extended Finite State Machines - EFSMv前面介绍的有限状态机模型有两个明显的缺点：前面介绍的有限状态机模型有两个明显的缺点：v第一，第一，FSMFSM不能方便地描述对变量的操作；不能方便地描述对变量的操作；v第二，缺少描述任意数值的传送的能力。第二，缺少描述任意数值的
63、传送的能力。v可以从三个方面对前述根本的可以从三个方面对前述根本的FSMFSM进行扩展：进行扩展： v变量；变量；v用传送整型值的队列来代替传送未定义数据类型用传送整型值的队列来代替传送未定义数据类型的抽象数据对象队列；的抽象数据对象队列；v引入一组操纵变量的算术和逻辑操作符。引入一组操纵变量的算术和逻辑操作符。 59第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) EFSM：Variablesv变量变量(Variables)v一般用一个符号名来表示，它的主要功能是保存变量取值一般用一个符号名来表示，它的主要功能是保存变量取值范围内的某一数值。范围内的某一数值。 v变量
64、与队列的主要区别是变量一次只能保存一个值，可以变量与队列的主要区别是变量一次只能保存一个值，可以将变量取值范围内的任意值赋给该变量，但是我们只能获将变量取值范围内的任意值赋给该变量，但是我们只能获取最后一次赋给变量的值。取最后一次赋给变量的值。 v如果变量的取值范围是有限的，那么变量的参加并没有增如果变量的取值范围是有限的，那么变量的参加并没有增加加FSM的计算能力。的计算能力。 v可以用有限状态机来描述一个具有有限取值范围的变量。可以用有限状态机来描述一个具有有限取值范围的变量。 v变量的引入可以将协议的输入输出动作一般化，即用一组变量的引入可以将协议的输入输出动作一般化，即用一组有限的、有
65、序的值的集合来定义有限的、有序的值的集合来定义I/O动作。集合中的值可以动作。集合中的值可以是变量表达式或者是常量数值。是变量表达式或者是常量数值。 60第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) EFSM: Variables (Cont.)vBenefits of Variables利用协议变量和操纵变量的算术和逻辑操作符，可以利用协议变量和操纵变量的算术和逻辑操作符，可以很好地描述协议动作很好地描述协议动作(对变量进行操作对变量进行操作)、状态变迁上的、状态变迁上的谓词，从而大大丰富了谓词，从而大大丰富了FSM的状态变迁函数的表达能的状态变迁函数的表达能力。
66、力。还可以减少还可以减少FSM的状态空间。的状态空间。 61第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) EFSM: Examples With Variablesv求两个数的最大公约数的过程。过程一开始处于初始状态求两个数的最大公约数的过程。过程一开始处于初始状态q0，等，等待输入变量待输入变量x和和y的值。过程以输出这两个输入的数值的最大公约的值。过程以输出这两个输入的数值的最大公约数结束，共有数结束，共有6个状态。个状态。 当前状态当前状态协议动作协议动作输出状态输出状态 q0输入输入x, y q1 q1x y q2q1x y q3q1x = y q4q2x
67、= x y q1q3y = y x q1q4输出输出x q5q5-将状态变迁条将状态变迁条件件(谓词谓词)、变、变量赋值和量赋值和I/O操操作放在同一列，作放在同一列，统一用协议动统一用协议动作作(Action)来表来表示。示。 62第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) EFSMvFor more complex problems number of states can increase to be unmanageable - this is called State ExplosionvNumber of states can be reduced b
68、y introducing the local variables. They reduce number of states by hiding less important informationvGlobal state of an EFSM is dependant on the explicit State and current value of its variables.vGenerally the information which doesnt have strong impact on behavior shall be represented as a variable
69、63第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) EFSMvEFSM introduce notions of Tasks where values of Variables are assignedDecisions where action (output, new state) depends on the Variable valuevStarting and Stopping of Timers also represents a task in EFSM64第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) Extended FSM
70、s TablevState tables for EFSM processes should include a separate tasks column, as outputs column is used explicitly for messages that shall be sentinputeventsoutputscurrentstatenextstateS1S2S1S2x1x2-x4,x2S2e1e1e2e2S2S1S1taskst1-t3t4S1S2T1, X1,S2t3,S1X2,S2e1e2T4,X4,X2,S1stateevent65第第3章章 协议形式化描述技术协议
71、形式化描述技术(1概述及概述及FSM) Example of Extended FSMv Communication protocol may rely on message acknowledge mechanism to indicate successful transmission of the messageTransmitterReceivermsgmsg_AckmsgUser AUser Bmsg66第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) EFSM Examplev If message is not acknowledged it is re-
72、transmittedTransmitterReceiverMsgMsg_AckmsgUser AUser BmsgMsg1 sec timer expiredMessagelost67第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) EFSM ExamplevIf second re-transmission is not acknowledged an error is indicated to userTransmitterReceiverMsgmsgUser A1 sec timer expiredMessagelostMsg1 sec timer expire
73、dMessagelosterror_Ind68第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) EFSM - States, Eventsv Consider Transmitter - what states can be identifiedIDLE no acknowledge pending, ready to send next messageW4_ACK waiting for acknowledge of next messagevWhat Input Events can be identifiedmsgFrom userMsg_AckFrom Rece
74、ivervWhat Output Events can be identifiedMsgto Receivererror_Indto User69第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) EFSM State TableStateEvent70第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) Equivalent FSM State TableStateEvent71第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) Finite State Machines (FSMs)十、十、Communicating FSM7
75、2第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) Modelling of Complex Systemsv So far we have only considered a single FSMvTypical Telecommunication System to complex to be represented with a single FSM.vAs usually when dealing with complexity we should split a complex problem in a number of smaller components
76、vIn this case we will have number of concurrent FSMs communicating with each othervThe two communication mechanisms for concurrent processes can be categorised into Message Passing and Shared Data73第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) Communicating FSMsv Communicating FSM can bein a single process (
77、task, thread of control)in separate concurrent processes on same microprocessoron separate microprocessors communicating to each otherv Depending how FSMs are co-located different methods of communications are possible (message passing, shared memory, )74第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) Comm. Me
78、chanisms for Concurrent Syst.vMessage passing involves sending and receiving messages through a channelProcessProcessSharedMemoryWriteReadProcessProcessReceiveSendChannelvIn the Shared Memory Approach memory is common to both processes, and they can read and write to the memoryvThe two are equivalen
79、t. We will only consider message passing as more general.75第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) Asynchronous & Synchronous Communicationv There are two approaches to implementing message passing: Synchronous & AsynchronousvIn Synchronous Communication the processes involved in communication are requ
80、ired to participate at the point of communication simultaneously. If Process A attempts to send a message and Process B is not ready to receive it process A must wait until Process B is ready.76第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) Asynchronous CommunicationvIn Asynchronous Communication the processe
81、s involved in communication are not required to participate at the point of communication simultaneously. If Process A attempts to send a message and Process B is not ready to receive it sends it anyway.If process B is ready to receive a message and A has not sent it process B must wait.Asynchronous
82、 communication requires the use of buffers to store messagesvAll of the protocol specification methods studied in this course will be based upon Asynchronous Communication77第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) Asynchronous Communication using FIFOsv In most communicating systems, a FIFO (First In Fi
83、rst Out) discipline is enforced on sending and receiving messages.vDuring a send event the a message is appended to the end of the queue while a receive event removes a message from the front of a queue.vIt is possible to modify the communications channel to provide additional communication construc
84、ts such as priority signals.vTo absorb any delay variation in the communications channel, FIFOs are usually used at the interfaces78第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) Asynchronous Communication using FIFOsProcessProcessFIFO CHANNELFIFO CHANNELSendReceiveReceiveSend79第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述
85、及FSM) Communicating FSMsv Now consider a model for communicating finite state machines.vEach process can be defined by a set of states.vThe process waits in a state for an event to occur.vMessages are received as events by the receiving FSM.vWhen this input event occurs, it transitions to another st
86、ate, and in doing so can send out messages and performs other tasks.vThis model is the model used by the ITU Specification and Description Language (SDL)80第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) Communicating FSMs - ExampleS11S12Receive(Y)/Send(R)Receive(X)/Send(P)S21S22Receive(R)/Send(X)Receive(P)/ Se
87、nd(Y)FSM1FSM2Y81第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) Communicating FSMs - ExampleRYPXFSM1FSM2YAfter receiving event Y FSMs will continue to oscillate indefinitely between their two states82第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) Benefits of the Communicating FSM modelv The overall state of the system c
88、an be described by a vector of all the states of the individual processes.vThe overall system state itself becomes a finite state machine, and thus its behaviour becomes more deterministic.83第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) FSMs - SummaryvMeaning of FSMvDiscrete event processes and finite state
89、machines are key concepts in modelling the dynamic real-time behaviour of telecommunications software.vFSM consist of vStates (Initial, Current and New)vInput EventsvOutput EventsvIn case when “state explosion is an issue extended FSM (EFSM) may be used so some states are replaced by local variables
90、vComplex Telecommunication Systems can be modelled as number of communicating FSMs84第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) Protocol Specification & FSMsvMany Formal protocol methods are based upon Finite State Machines.vThe ITU Specification and Description Language (SDL) is one such formal specificat
91、ion methodvMost protocols defined by ITU after the advent of SDL are described using SDL.vPrior to the introduction of SDL protocols were described using a variety of different methods including natural language.85第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) Protocol Specification & FSMsvEven with the adven
92、t of formal specification languages there still exist ambiguities and incompleteness in the protocol specifications that must be resolved in the software designvEven formally specified protocols may not have been validated sufficiently.vThe standards dont include machine dependent details (like crea
93、te application process) leaving the software designer to fill the gaps in.86第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) FSM: 思考题思考题v画出自动回叫系统的有限状态机状态变迁图。画出自动回叫系统的有限状态机状态变迁图。v 自动加叫：在被呼叫方正忙的情况下，系统继续保自动加叫：在被呼叫方正忙的情况下，系统继续保持对被呼叫方状态的检测，一旦被呼叫方出现空闲状持对被呼叫方状态的检测，一旦被呼叫方出现空闲状态，那么系统将再次对其进行呼叫。过程如下：态，那么系统将再次对其进行呼叫。过程如下：v
94、A呼叫呼叫B，但，但B的的 正忙；正忙；vA按下按下“自动回叫键；自动回叫键；vA听到确认提示，然后放下听到确认提示，然后放下 ；vB回到了空闲状态；回到了空闲状态；vA端的端的 进行特殊的响铃提示，说明进行特殊的响铃提示，说明B已经处于空闲状已经处于空闲状态；态；vA拿起听筒；拿起听筒；v系统自动地再次向系统自动地再次向B发出呼叫；发出呼叫；vB拿起听筒；拿起听筒；vA与与B通话通话87第第3章章 协议形式化描述技术协议形式化描述技术(1概述及概述及FSM) FSM：思考题续：思考题续 需考虑的特殊情况：需考虑的特殊情况：如果有多个用户同时针对同一个目的端使用自动回叫效如果有多个用户同时针对
95、同一个目的端使用自动回叫效劳，将如何处理？劳，将如何处理？当系统检测到目的端空闲，并向发起呼叫的用户响铃提当系统检测到目的端空闲，并向发起呼叫的用户响铃提示时，如果该用户不命起听筒例如改变了主意，不示时，如果该用户不命起听筒例如改变了主意，不再希望与再希望与B通话，那么将如何处理？通话，那么将如何处理？在系统向呼叫发起端进行响铃通知的过程中，如果目的在系统向呼叫发起端进行响铃通知的过程中，如果目的端又重新进行了忙的状态，此时将如果处理？端又重新进行了忙的状态，此时将如果处理？在自动呼叫结束前，如果呼叫发起端希望取消自动呼叫在自动呼叫结束前，如果呼叫发起端希望取消自动呼叫效劳例如挂断了效劳例如挂断了 ，此时系统将如何处理？，此时系统将如何处理？88
