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

2019年12月2日星期一,形式化描述技术,3-1,网络协议工程,第3讲：协议形式化描述技术,2019年12月2日星期一,形式化描述技术,3-2,第3讲：协议形式化描述技术,3.1概述3.2有限状态机(FSM)3.3PetriNet3.4SDL3.5Estelle3.6Lotos3.7ASN.1,2019年12月2日星期一,形式化描述技术,3-3,形式化描述技术：Why?,通信系统行为的复杂性增大了行为描述的难度，人们必须借助一种语言或一种技术来准确地描述系统行为。在过去，人们习惯使用自然语言进行协议描述（用自然语言写协议的规格说明或规范）优点是：方便、易懂致命缺点是：不严格、不精确、结构不好、没有描述标准和有二义性且很难进行协议实现、测试的自动化和协议验证。不同的人对协议描述的理解不一样导致不同的协议实现之间不能实现互连，甚至还会得出错误的协议。解决办法：形式化技术FDTs(FormalDescriptionTechniques),2019年12月2日星期一,形式化描述技术,3-4,FDTs：Aims,采用形式描述技术的目的是：为开发者提供一种分析的方法；作为对开发结果验证的基础；为设计人员和应用人员提供交流途径；作为开发文档能在将来再开发时使用。理想的形式描述技术应该既能描述系统的行为特征，又能进行操作：在系统需求分析和设计阶段，它应该是一种描述语言在系统实现阶段它应该是一种编程语言。形式描述技术是将协议工程各阶段在技术上衔接起来的纽带，因此它对协议工程的发展起决定性作用。,2019年12月2日星期一,形式化描述技术,3-5,FDTs：特性,用于协议的FDT一般应具有如下重要特性：完整的语法和语义定义体系结构、服务和协议的可表达性协议重要特性(如，无死锁)的可分析性支持复杂协议的管理(如，构造能力)支持逐步求精的方法支持实现独立性(包括并发性、非确定性和适当的抽象机制)支持协议生命期的各环节，包括验证、实现和测试支持自动或半自动设计、验证、实现和维护方法应能准确地描述进程交互的各种原语,2019年12月2日星期一,形式化描述技术,3-6,FDTs:Classification,形式描述模型(FDM)状态变迁模型有限状态机FSM(FiniteStateMachine)扩展的有限状态机EFSM(ExtendedFSM)模型通信有限状态机CFSM(CommunicatingFSM)模型CarlAdamPetri的Petri网(PetriNet)时态逻辑TL(TemporalLogic)进程代数(AlgebraofProcess)R.Miler：通信系统演算CCS(CalculusofCommunicationSystem)（进程代数据的基础）Hoare：通信顺序进程CSP(CommunicatingSequentialProcesses)（以CCS为基础）,2019年12月2日星期一,形式化描述技术,3-7,FDTs:Classification(Cont.),形式描述语言(FDL)ISO制定的Estelle和LOTOSCCITT制定的SDLISO的ASN.1(抽象语法记法)对象管理组织OMG制定的统一建模语言UMLISO的抽象测试集描述语言的TTCN高级程序设计语言，如Pascal,C,PL/1便于协议的实现大多数比较复杂、分析起来比较困难，且不支持非确定性的描述。,2019年12月2日星期一,形式化描述技术,3-8,模型vs.语言,模型含义一：对象或系统的抽象OSI/RM：网络系统的抽象模型含义二：描述对象或系统的方法或技术FSMPetriNet,2019年12月2日星期一,形式化描述技术,3-9,Functionsvs.Computation,Functionsspecifyonlyarelationbetweentwosetsofvariables(inputandoutput)ComputationsdescribehowtheoutputVariablescanbederivedfromthevalueoftheinputvariables.,2019年12月2日星期一,形式化描述技术,3-10,ModelofComputation,AMoCisaframeworkinwhichtoexpresswhatsequenceofactionsmustbetakentocompleteacomputationAninstanceofamodelofcomputationisarepresentationofafunctionunderaparticularinterpretationofitsconstituentsNotnecessarilyabijection(infactalmostnever!)Examples:FiniteStateMachine,TuringMachine,differentialequation,2019年12月2日星期一,形式化描述技术,3-11,模型vs.语言（续）,形式语言具有严格的语法和语义可以精确、完全地表述协议的功能、性能及行为等以一种或多种数学方法或形式模型为基础SDL：基于扩展的FSM和抽象数据类型Eetelle：基于扩展的FSM，是Pascal语言的扩充LOTOS：基于通信系统演算（CCS）和抽象数据类型语言ACTONE,2019年12月2日星期一,形式化描述技术,3-12,模型vs.语言（续）,模型与语言的差别不是很明显。不同文献有不同的说法。将模型与语言分开一些文献中的模型在另一些文献中成为语言或相反将模型与语言不分，统称为形式化描述技术事实上，模型也可以看成是一种形式语言文法：描述语言的语法结构的形式规则（即语法规则）Turing机(无限自动机)的能力相当于0型文法有限自动机相当于正规文法（3型文法）模型是语言的一个实例(Instance)（语义），例如C语言编译器是C语言的模型,2019年12月2日星期一,形式化描述技术,3-13,ModelsOfComputationandlanguages,NeedtodistinguishbetweenmodelandlanguageLanguageneedstobeexpressiveenoughforapplicationdomain(writethingsonce)havesemanticsindesiredMOCMOCneedstobepowerfulenoughforapplicationdomainhaveappropriatesynthesisandvalidationalgorithms,2019年12月2日星期一,形式化描述技术,3-14,FDTs:小结,实际应用时，往往是将多种形式描述技术混合起来使用。例如：将协议中的主要状态用变迁用图形表示(有限状态机或Petri网)，而协议的其他细节则用高级语言描述。这样使得协议的描述和验证都比较方便。,2019年12月2日星期一,形式化描述技术,3-15,第3讲：协议形式化描述技术,3.1概述3.2有限状态机(FSM)3.3PetriNet3.4SDL3.5Estelle3.6Lotos3.7ASN.1,2019年12月2日星期一,形式化描述技术,3-16,FiniteStateMachines(FSMs),一、概述,2019年12月2日星期一,形式化描述技术,3-17,FiniteStateMachines(FSMs),inputevents,outputs,currentstate,nextstate,state,transitionfunction,Finitestatemachinesconsistof:,OutputEvents,InputEvents(orSignals,orMessages),TransitionFunctions,STATE,States,NEXTSTATE,CURRENTSTATE,INPUTEVENTS,OUTPUTS,TransitionFunction,2019年12月2日星期一,形式化描述技术,3-18,FiniteStateMachineStates,CurrentStateStatewhichdeterminesthecurrentbehaviorofthemachineNextStateStatewhichwillmachinehaveafterprocessinganinputevent.NextStatecanbesameascurrentStartStateStateinwhichmachinewillbewhencreated,2019年12月2日星期一,形式化描述技术,3-19,FSMTransitions,inputevents,outputs,currentstate,nextstate,state,transitionfunction,TriggeredbyinputeventstheFSMmovesfromonestatetootherbasedontheTransitionFunctionTransitionFunctionproducestheOutputandNextStatedependingonCurrentStateandInputEventWhileinparticularstateFSMisnotactive.Itiswaitingforaninputtoperformnextactivity,2019年12月2日星期一,形式化描述技术,3-20,FiniteStateMachines(FSMs),二、形式化定义,2019年12月2日星期一,形式化描述技术,3-21,FSM:FormalDefinition,FSMis5-tuple:FSM=(S,s0,I,F),whereS=s0,s1,sn:有限状态集合。在任一确定时刻，FSM只能处于一个确定的状态si。I=a0,a1,am:有限输入字符集合。在任一确定的时刻，FSM只能接收一个确定的输入aj。：SIS是状态转换函数，如果在某一确定的时刻，FSM处于某一状态siS,并接收一个输入字符ajI，那么下一时刻将处于一个确定的状态s=(si,aj)S。在这里规定，s=(s,)，即对任何状态s，当读入空字符时，有很状态机不发生任何状态转移。s0S是初始状态，FSM由此状态开始接收输入FS是一个终态集（可空），FSM到达终态后不再接收输入确定有限状态机也称为DFA（确定有限自动机）,2019年12月2日星期一,形式化描述技术,3-22,NondeterministicFSM(orNFA),NFSMis5-tuple:FSM=(S,s0,I,F),whereS=s0,s1,sn:有限状态集合。在任一确定时刻，FSM只能处于一个确定的状态si。I=a0,a1,am:有限输入字符集合。在任一确定的时刻，FSM只能接收一个确定的输入aj。：SI2S是状态转换函数，如果在某一确定的时刻，FSM处于某一状态siS,并接收一个输入字符ajI，那么下一时刻将处于一个某一个状态子集=(si,aj)=p0,p1,pk(piS,I=1,2,k)。在这里规定，s=(s,)，即对任何状态s，当读入空字符时，有很状态机不发生任何状态转移。s0S是初始状态，FSM由此状态开始接收输入FS是一个终态集（可空），FSM到达终态后不再接收输入,2019年12月2日星期一,形式化描述技术,3-23,FSM:FormalDefinition(Cont.),在一些情况下，如果讨论问题的重点集中在FSM的状态集(S)、输入集(I)和状态转换函数()上。这时可用如下两种方式来表示FSM：FSM=(S,I,)或FSM=(S,s0,I,),2019年12月2日星期一,形式化描述技术,3-24,FiniteStateMachines(FSMs),三、Representation,2019年12月2日星期一,形式化描述技术,3-25,StateTransitionDiagrams(状态转换图),UsedtoVisuallyrepresentanFSMEmphasisisonidentifyingstatesandpossibletransitionsCirclesrepresentStatesArrowsrepresentTransitionseiareinputsxiareoutputs,2019年12月2日星期一,形式化描述技术,3-26,FSMTables(状态转换表),Allinputs,states,statetransitionsandoutputsofaFSMcanbelistedinaTableformat,EachrowofthetableisoneuniquecombinationofInputEventsandCurrentStateForcompletedefinitionofFSMallEvent/StatecombinationsshallbeprovidedTableisanotherwaytorepresentanFSMwithanemphasisonexploringallEvent/Statecombinations,2019年12月2日星期一,形式化描述技术,3-27,FSMTable-CompactForm,HereinthetoprowoftheTablehasalistofallStateswhilefirstcolumnhasalistofallInputEvent.TableFieldontheintersectionrepresentsthetransitionfunctionfortheState,EventcombinationEachfieldcontainslistofoutputsandnextstate,2019年12月2日星期一,形式化描述技术,3-28,RockerSwitchExample,Eventssuchas“switchon”and“switchoff”maycausethemachinetochangestate,asinthestatediagrambelowforalightwitharockerswitch.,Someeventsdontcauseastatetransitionatall,asinattemptingtoturnonalightthatisalreadyon.Behaviourofthesystemineachstatehastobedefined:StateON-lightisemittedoutofbulb,StateOFF-nolightemitted,2019年12月2日星期一,形式化描述技术,3-29,FSMExample-Telephone,WhatarepossiblestatesWhatarepossibleeventsCreateFSMTableCreateStateTransitionDiagramWhenwemodelanobjectweconsiderbehaviorwhichisofinterestforus.Inthiscasewewillconsiderabilityofphonetobeusedtodialanothersubscriber,tobeusedtopassvoicebetweensubscribersandtobeabletoreceiveincomingcalls.,2019年12月2日星期一,形式化描述技术,3-30,TelephoneStates,FollowingStatescanbeidentifiedIDLEnocallsinprogresshandsetison-hookDIALINGhandsetisoff-hook,butcallisnotinprogressRINGINGhandsetison-hook,incomingcallalertPATHACTIVEhandsetinoff-hookandcallisinprogressRelevanteventsare:off-hookUsertakeshandsetoff-hookon-hookUserplaceshandseton-hookdialdigitUserdialsdigitcallalertExchangealertsphone-incomingcall,2019年12月2日星期一,形式化描述技术,3-31,Telephone-FSMTable,Note1:iflastdigitinphonenumberisdialedloweroptionshallbeselected,“/“Unexpectedevent,“-”NoStateChange,2019年12月2日星期一,形式化描述技术,3-32,Telephone-StateTransitionDiagram,DialDigit,DialDigit,On-Hook,On-Hook,ThisisStartingstate,2019年12月2日星期一,形式化描述技术,3-33,Timers&FSMs,Sometimesthereisaneedtoperformsomeactionsaftersomeperiodoftime.ForthatpurposetimersareusedTimerscanbestartedspecifyingamountoftimebeforetime-outwillhappenWhentime-outoccursthetimereventwillbesenttotheFSM.NameofeventistypicallysameasnameoftimerTimerscanbestopped,sotimereventisnotgenerated,2019年12月2日星期一,形式化描述技术,3-34,TelephoneFSMTablewithTimers,Note1:iflastdigitinphonenumberisdialedloweroptionshallbeselected,2019年12月2日星期一,形式化描述技术,3-35,TelephoneSTDwithTimers,DialDigit,DialDigit,On-Hook,On-Hook,ThisisStartingstate,T1,Starting/StoppingoftheTimersisnotvisibleonSTD.,2019年12月2日星期一,形式化描述技术,3-36,FiniteStateMachines(FSMs),四、Moore机,2019年12月2日星期一,形式化描述技术,3-37,MooreFSM,前面讨论的FSM和非确定FSM，可以看成仅接收输入并发生状态改变，但无任何输出的自动机器。实际上生活中的许多有限状态系统对于不同的输入信号，除内部状态不断改变外，还不断向系统外部输出各种信号。具有输出的自动机器模型按照输出的不同分成两类：Moore机：输出与状态有关Mealy机：输出与状态和输入有关,2019年12月2日星期一,形式化描述技术,3-38,MooreFSM:FormalDefinition,MooreFSMis6-tuple:FSM=(S,s0,I,O,),whereS=s0,s1,sn:有限状态集合。在任一确定时刻，FSM只能处于一个确定的状态si。I=a0,a1,am:有限输入字符集合。在任一确定的时刻，FSM只能接收一个确定的输入aj。O=b0,b1,bn:有限输出字符集合。：SI2S是状态转换函数，如果在某一确定的时刻，FSM处于某一状态siS,并接收一个输入字符ajI，那么下一时刻将处于一个确定的状态s=(si,aj)S。在这里规定，s=(s,)，即对任何状态s，当读入空字符时，有很状态机不发生任何状态转移。s0S是初始状态，FSM由此状态开始接收输入：SO是输出函数,2019年12月2日星期一,形式化描述技术,3-39,Moore机：FormalDefinition,Moore机只是在接收输入串的过程中不断改变状态，并且在每个状态上有字符输出。例如：对于输入串a0,a1,an-1，设：(s0,a0)=s1,(s1,a1)=s2,.(sn-1,an-1)=sn这时输出序列为：(s0)(s1)(sn-1),2019年12月2日星期一,形式化描述技术,3-40,Moore机vs.有限状态机,有限状态机可看做是Moore机的一个特例，Why?对于任何一个有限状态机M=(S,s0,I,F):引入输出字符集合O=0,1，并定义S到O的映射为：对于sF,(s)=1；对于sF,(s)=0这样得到一个Moore机M=(S,s0,I,O,)，在该Moore机中，输出为1的状态为终结状态，输出为0的状态即为非终结状态。,2019年12月2日星期一,形式化描述技术,3-41,FiniteStateMachines(FSMs),五、Mealy机,2019年12月2日星期一,形式化描述技术,3-42,MealyFSM:FormalDefinition,MealyFSMis6-tuple:FSM=(S,s0,I,O,),whereS=s0,s1,sn:有限状态集合。在任一确定时刻，FSM只能处于一个确定的状态si。I=a0,a1,am:有限输入字符集合。在任一确定的时刻，FSM只能接收一个确定的输入aj。O=b0,b1,bn:有限输出字符集合。：SI2S是状态转换函数，如果在某一确定的时刻，FSM处于某一状态siS,并接收一个输入字符ajI，那么下一时刻将处于一个确定的状态s=(si,aj)S。在这里规定，s=(s,)，即对任何状态s，当读入空字符时，有很状态机不发生任何状态转移。s0S是初始状态，FSM由此状态开始接收输入：SIO是输出函数,2019年12月2日星期一,形式化描述技术,3-43,Moore机：FormalDefinition,Mealy机只是在接收输入串的过程中不断改变状态，并且字符输出与当前状态有关。例如：对于输入串a0,a1,an-1，设：(s0,a1)=s1,(s1,a2)=s2,.(sn-1,an-1)=sn这时输出序列为：(s0,a0)(s1,a1)(sn-1,an-1),2019年12月2日星期一,形式化描述技术,3-44,Mealy机vs.Moore机,Moore机可看做是Mealy机的一个特例，Why?对于任何一个Moore机M=(S,s0,I,O,):设当输入串为a0,a1,an-1时，其输出序列为：(s0)(s1)(sn)，其中si和ai-1满足：(si-1,ai-1)=si，1in引入：SI到O的映射：(si-1,ai-1)=(si-1,ai-1)=(si),1in这样得到一个Mealy机M=(S,s0,I,O,)，对于输入串a0,a1,an-1，Mealy机M的输出为为：(s0,a0)(s1,a1)(sn-1,an-1)=(s0)(s1)(sn-1),2019年12月2日星期一,形式化描述技术,3-45,Mealy机：Example,停止等待协议：设甲、乙双方进行半双工通信，甲发信息帧，乙回送确认帧。双方约定采用停止等待协议，因此甲方仅需用1比特来编号。将0号帧和1号帧分别记为0和1。当收到有差错的帧时，则丢弃此帧，同时不发任何应答帧。当收到无差错的帧但序号不正确时，要发确认帧，同时要丢弃此帧，不送主机。我们还假定收方在准备发送确认帧ACK时，暂不接收外面发来的帧。,2019年12月2日星期一,形式化描述技术,3-46,停止等待协议：状态变迁表,2019年12月2日星期一,形式化描述技术,3-47,停止等待协议：状态变迁图,1234,1234,等待,准备发ACK,准备发ACK,准备发0,准备发1,期望收1,期望收0,等待,发0,发1,收1,收0,发ACK,发ACK,收ACK,收ACK,发ACK,收1,发ACK,收0,甲方,乙方,超时,超时,状态符号,状态编号,状态含义,状态变迁,输入事件,对某些状态进行了简化。例如，当乙方处于“期望收0”的状态时，若收到无差错的1帧，仍然应当先进入“准备发ACK”状态，然后才发出ACK。但这里就将“收1”与“发ACK”合并成为一个事件。,再例如，当乙方处于“期望收1”的状态时，若收到无差错的0帧，仍然应当先进入“准备发ACK”状态，然后才发出ACK。但这里就将“收0”与“发ACK”合并成为一个事件。,2019年12月2日星期一,形式化描述技术,3-48,停止等待协议：状态变迁图合并,前面描述的甲、乙两方各自的有限状态机实际上并非独立地工作而是协调在一起工作的。如合在一起用一个有限状态机来描述整个系统，将会更加清楚。但这将导致状态数目将大大增加。Why?甲方和乙方的状态各有4个，而信道上的状态也有4个(即：信道上传送0，传送1，传送ACK，以及出现差错或帧的丢失)。这样将总共有43=64种状态，用状态图很难清楚地表示出来。解决办法：合并一些状态,即考虑一些次要的细节,2019年12月2日星期一,形式化描述技术,3-49,停止等待协议：状态变迁图合并,状态合并：甲方的状态1和状态2，状态3和状态4都可以合并，乙的状态1和状态4，状态2和状态3也可进行合并。信道的状态是由其内容决定的，例如，如果帧0正在信道上(即，帧已被分地发送出去，部分地被接收，但在目的主机上还未进行处理)，则信道的状态为帧0。整个系统的状态是通信双方两个协议机和信道的所有状态的组合。用3个字符XYZ表示整个系统的状态，其中X=0或1，对应于甲方准备发0或1(包括发完后等待ACK的状态)；Y=0或1，对应于乙方期望收到0或1；Z=0,1,A或，对应于信道上传送的是0，1，ACK或出现了差错(包括丢失)。,2019年12月2日星期一,形式化描述技术,3-50,停止等待协议：合并后的状态变迁图,变迁意义0帧丢失或帧出错1收0，发ACK，送主机2收ACK，发13收1，发ACK，送主机4收ACK，发05收0，发ACK，不送主机6收1，发ACK，不送主机7超时，发08超时，发1,0,0,0,0,0,0,1,2,3,4,5,6,7,8,8,7,000,010,111,101,10,11,01,00,10A,01A,假设系统一开始处在(000)状态。这表示甲发完0，乙期望收到0，而信道上传送的也是0。在无差错的情况下，系统的状态仅在4个状态中循环：(000)(01A)(111)(10A)(000)。如果信道丢失了帧0，则进行从状态(000)到状态(00-)的转换。最终，发送过程超时(转换7)，且系统回到状态(000)。确认帧的丢失更为复杂，需要两种转换：7和5，或8和6，直到修复损坏。从理论上讲，应当共有224=16种不同的状态。去掉没有意义的组合后，还剩下10种状态，而导致状态变迁的输入事件共有9种(标号08)。,2019年12月2日星期一,形式化描述技术,3-51,停止等待协议：Summary,当描述比较复杂的协议时，状态的数目将急剧增加，以致很难用它来清晰地描述协议。例如，如果我们将前面描述的半双工通信的停止等待协议改为全双工通信的停止等待协议，则其状态图就要复杂多了,2019年12月2日星期一,形式化描述技术,3-52,全双工通信的停止等待协议状态变迁图,2019年12月2日星期一,形式化描述技术,3-53,FiniteStateMachines(FSMs),六、EFSM,2019年12月2日星期一,形式化描述技术,3-54,ExtendedFiniteStateMachines-EFSM,前面介绍的有限状态机模型有两个明显的缺点：第一，FSM不能方便地描述对变量的操作；第二，缺少描述任意数值的传送的能力。可以从三个方面对前述基本的FSM进行扩展：变量；用传送整型值的队列来代替传送未定义数据类型的抽象数据对象队列；引入一组操纵变量的算术和逻辑操作符。,2019年12月2日星期一,形式化描述技术,3-55,EFSM：Variables,变量(Variables)一般用一个符号名来表示，它的主要功能是保存变量取值范围内的某一数值。变量与队列的主要区别是变量一次只能保存一个值，可以将变量取值范围内的任意值赋给该变量，但是我们只能获取最后一次赋给变量的值。如果变量的取值范围是有限的，则变量的加入并没有增加FSM的计算能力。可以用有限状态机来描述一个具有有限取值范围的变量。变量的引入可以将协议的输入输出动作一般化，即用一组有限的、有序的值的集合来定义I/O动作。集合中的值可以是变量表达式或者是常量数值。,2019年12月2日星期一,形式化描述技术,3-56,EFSM:Variables(Cont.),BenefitsofVariables利用协议变量和操纵变量的算术和逻辑操作符，可以很好地描述协议动作(对变量进行操作)、状态变迁上的谓词，从而大大丰富了FSM的状态变迁函数的表达能力。还可以减少FSM的状态空间。,2019年12月2日星期一,形式化描述技术,3-57,EFSM:ExamplesWithVariables,求两个数的最大公约数的过程。过程一开始处于初始状态q0，等待输入变量x和y的值。过程以输出这两个输入的数值的最大公约数结束，共有6个状态。,将状态变迁条件(谓词)、变量赋值和I/O操作放在同一列，统一用协议动作(Action)来表示。,2019年12月2日星期一,形式化描述技术,3-58,EFSM,Formorecomplexproblemsnumberofstatescanincreasetobeunmanageable-thisiscalledStateExplosionNumberofstatescanbereducedbyintroducingthelocalvariables.TheyreducenumberofstatesbyhidinglessimportantinformationGlobalstateofanEFSMisdependantontheexplicitStateandcurrentvalueofitsvariables.Generallytheinformationwhichdoesnthavestrongimpactonbehaviorshallberepresentedasavariable,2019年12月2日星期一,形式化描述技术,3-59,EFSM,EFSMintroducenotionsofTaskswherevaluesofVariablesareassignedDecisionswhereaction(output,newstate)dependsontheVariablevalueStartingandStoppingofTimersalsorepresentsataskinEFSM,2019年12月2日星期一,形式化描述技术,3-60,ExtendedFSMsTable,StatetablesforEFSMprocessesshouldincludeaseparatetaskscolumn,asoutputscolumnisusedexplicitlyformessagesthatshallbesent,2019年12月2日星期一,形式化描述技术,3-61,ExampleofExtendedFSM,Communicationprotocolmayrelyonmessageacknowledgemechanismtoindicatesuccessfultransmissionofthemessage,Transmitter,Receiver,msg,msg_Ack,msg,UserA,UserB,msg,2019年12月2日星期一,形式化描述技术,3-62,EFSMExample,Ifmessageisnotacknowledgeditisre-transmitted,Transmitter,Receiver,Msg,Msg_Ack,msg,UserA,UserB,msg,Msg,1sectimerexpired,Messagelost,2019年12月2日星期一,形式化描述技术,3-63,EFSMExample,Ifsecondre-transmissionisnotacknowledgedanerrorisindicatedtouser,Transmitter,Receiver,Msg,msg,UserA,1sectimerexpired,Messagelost,Msg,1sectimerexpired,Messagelost,error_Ind,2019年12月2日星期一,形式化描述技术,3-64,EFSM-States,Events,ConsiderTransmitter-whatstatescanbeidentifiedIDLEnoacknowledgepending,readytosendnextmessageW4_ACKwaitingforacknowledgeofnextmessageWhatInputEventscanbeidentifiedmsgFromuserMsg_AckFromReceiverWhatOutputEventscanbeidentifiedMsgtoReceivererror_IndtoUser,2019年12月2日星期一,形式化描述技术,3-65,EFSMStateTable,State,Event,2019年12月2日星期一,形式化描述技术,3-66,EquivalentFSMStateTable,State,Event,2019年12月2日星期一,形式化描述技术,3-67,FiniteStateMachines(FSMs),七、CommunicatingFSM,2019年12月2日星期一,形式化描述技术,3-68,ModellingofComplexSystems,SofarwehaveonlyconsideredasingleFSMTypicalTelecommunicationSystemtocomplextoberepresentedwithasingleFSM.AsusuallywhendealingwithcomplexityweshouldsplitacomplexprobleminanumberofsmallercomponentsInthiscasewewillhavenumberofconcurrentFSMscommunicatingwitheachotherThetwocommunicationmechanismsforconcurrentprocessescanbecategorisedintoMessagePassingandSharedData,2019年12月2日星期一,形式化描述技术,3-69,CommunicatingFSMs,CommunicatingFSMcanbeinasingleprocess(task,threadofcontrol)inseparateconcurrentprocessesonsamemicroprocessoronseparatemicroprocessorscommunicatingtoeachotherDependinghowFSMsareco-locateddifferentmethodsofcommunicationsarepossible(messagepassing,sharedmemory,),2019年12月2日星期一,形式化描述技术,3-70,Comm.MechanismsforConcurrentSyst.,Messagepassinginvolvessendingandreceivingmessagesthroughachannel,IntheSharedMemoryApproachmemoryiscommontobothprocesses,andtheycanreadandwritetothememory,Thetwoareequivalent.Wewillonlyconsidermessagepassingasmoregeneral.,2019年12月2日星期一,形式化描述技术,3-71,Asynchronous&SynchronousCommunication,Therearetwoapproachestoimplementingmessagepassing:Synchronous&AsynchronousInSynchronousCommunicationtheprocessesinvolvedincommunicationarerequiredtoparticipateatthepointofcommunicationsimultaneously.IfProcessAattemptstosendamessageandProcessBisnotreadytoreceiveitprocessAmustwaituntilProcessBisready.,2019年12月2日星期一,形式化描述技术,3-72,AsynchronousCommunication,InAsynchronousCommunicationtheprocessesinvolvedincommunicationarenotrequiredtoparticipateatthepointofcommunicationsimultaneously.IfProcessAattemptstosendamessageandProcessBisnotreadytoreceiveitsendsitanyway.IfprocessBisreadytoreceiveamessageandAhasnotsentitprocessBmustwait.AsynchronouscommunicationrequirestheuseofbufferstostoremessagesAlloftheprotocolspecificationmethodsstudiedinthiscoursewillbebaseduponAsynchronousCommunication,2019年12月2日星期一,形式化描述技术,3-73,AsynchronousCommunicationusingFIFOs,Inmostcommunicatingsystems,aFIFO(FirstInFirstOut)disciplineisenforcedonsendingandreceivingmessages.Duringasendeventtheamessageisappendedtotheendofthequeuewhileareceiveeventremovesamessagefromthefrontofaqueue.Itispossibletomodifythecommunicationschanneltoprovideadditionalcommunicationconstructssuchasprioritysignals.Toabsorbanydelayvariationinthecommunicationschannel,FIFOsareusuallyusedattheinterfaces,2019年12月2日星期一,形式化描述技术,3-74,AsynchronousCommunicationusingFIFOs,2019年12月2日星期一,形式化描述技术,3-75,CommunicatingFSMs,Nowconsideramodelforcommunicatingfinitestatemachines.Eachprocesscanbedefinedbyasetofstates.Theprocesswaitsinastateforaneventtooccur.MessagesarereceivedaseventsbythereceivingFSM.Whenthisinputeventoccurs,ittransitionstoanotherstate,andindoingsocansendoutmessagesandperformsothertasks.ThismodelisthemodelusedbytheITUSpecificationandDescriptionLanguage(SDL),2019年12月2日星期一,形式化描述技术,3-76,CommunicatingFSMs-Example,Receive(Y)/Send(R),Receive(X)/Send(P),Receive(R)/Send(X),Receive(P)/Send(Y),FSM1,FSM2,Y,2019年12月2日星期一,形式化描述技术,3-77,CommunicatingFSMs-Example,AfterreceivingeventYFSMswillcontinuetooscillateindefinitelybe