《协议形式化描述技术（1-概述及fsm）》由会员分享，可在线阅读，更多相关《协议形式化描述技术（1-概述及fsm）（88页珍藏版）》请在金锄头文库上搜索。
1、第 3 章 协议形式化描述技术 （1-概述及FSM）,2,内容提要,概述,1,FSM,2,3,形式化描述技术：Why?,通信系统行为的复杂性增大了行为描述的难度，人们必须借助一种语言或一种技术来准确地描述系统行为。 在过去，人们习惯使用自然语言进行协议描述（用自然语言写协议的规格说明或规范） 优点是：方便、易懂 致命缺点是：不严格、不精确、结构不好、没有描述标准和有二义性 且很难进行协议实现、测试的自动化和协议验证。 不同的人对协议描述的理解不一样导致不同的协议实现之间不能实现互连，甚至还会得出错误的协议。 解决办法：形式化技术 FDTs (Formal Description Techniq
2、ues),4,FDTs：Aims,采用形式描述技术的目的是： 为开发者提供一种分析的方法； 作为对开发结果验证的基础； 为设计人员和应用人员提供交流途径； 作为开发文档能在将来再开发时使用。 理想的形式描述技术应该既能描述系统的行为特征，又能进行操作： 在系统需求分析和设计阶段，它应该是一种描述语言 在系统实现阶段它应该是一种编程语言。 形式描述技术是将协议工程各阶段在技术上衔接起来的纽带，因此它对协议工程的发展起决定性作用。,5,FDTs：特性,用于协议的FDT一般应具有如下重要特性： 完整的语法和语义定义 体系结构、服务和协议的可表达性 协议重要特性(如，无死锁)的可分析性 支持复杂协议的
3、管理(如，构造能力) 支持逐步求精的方法 支持实现独立性(包括并发性、非确定性和适当的抽象机制) 支持协议生命期的各环节，包括验证、实现和测试 支持自动或半自动设计、验证、实现和维护方法 应能准确地描述进程交互的各种原语,6,FDTs: Classification,形式描述模型(FDM) 状态变迁模型 有限状态机FSM(Finite State Machine) 扩展的有限状态机EFSM(Extended FSM)模型 通信有限状态机CFSM(Communicating FSM)模型 Carl Adam Petri的Petri网(PetriNet) 时态逻辑TL(Temporal Logic
4、) 进程代数(Algebra of Process) R.Miler：通信系统演算CCS (Calculus of Communication System)（进程代数据的基础） Hoare：通信顺序进程CSP (Communicating Sequential Processes)（以CCS为基础）,7,FDTs: Classification (Cont.),形式描述语言(FDL) ISO制定的Estelle和LOTOS CCITT制定的SDL ISO的ASN.1(抽象语法记法) 对象管理组织OMG制定的统一建模语言UML ISO的抽象测试集描述语言的TTCN 高级程序设计语言，如Pasc
5、al, C, PL/1 便于协议的实现 大多数比较复杂、分析起来比较困难，且不支持非确定性的描述。,8,模型 vs. 语言,模型 含义一：对象或系统的抽象 OSI/RM：网络系统的抽象模型 含义二：描述对象或系统的方法或技术 FSM PetriNet,9,Functions vs. Computation,Functions specify only a relation between two sets of variables (input and output) Computations describe how the output Variables can be derived f
6、rom the value of the input variables.,10,Model of Computation,A MoC is a framework in which to express what sequence of actions must be taken to complete a computation An instance of a model of computation is a representation of a function under a particular interpretation of its constituents Not ne
7、cessarily a bijection (in fact almost never!) Examples: Finite State Machine, Turing Machine, differential equation,11,模型 vs. 语言（续）,形式语言 具有严格的语法和语义 可以精确、完全地表述协议的功能、性能及行为等 以一种或多种数学方法或形式模型为基础 SDL：基于扩展的FSM和抽象数据类型 Eetelle：基于扩展的FSM，是Pascal语言的扩充 LOTOS：基于通信系统演算（CCS）和抽象数据类型语言ACT ONE,12,模型 vs. 语言（续）,模型与语言的差别
8、不是很明显。不同文献有不同的说法。 将模型与语言分开 一些文献中的模型在另一些文献中成为语言或相反 将模型与语言不分，统称为形式化描述技术 事实上，模型也可以看成是一种形式语言 文法：描述语言的语法结构的形式规则（即语法规则） Turing 机(无限自动机)的能力相当于0型文法 有限自动机相当于正规文法（3型文法） 模型是语言的一个实例(Instance)（语义），例如C语言编译器是C语言的模型,13,Models Of Computation and languages,Need to distinguish between model and language Language needs
9、 to be expressive enough for application domain (write things once) have semantics in desired MOC MOC needs to be powerful enough for application domain have appropriate synthesis and validation algorithms,14,FDTs: 小结,实际应用时，往往是将多种形式描述技术混合起来使用。 例如：将协议中的主要状态用变迁用图形表示(有限状态机或Petri网)，而协议的其他细节则用高级语言描述。这样使得
10、协议的描述和验证都比较方便。,15,内容提要,概述,1,FSM,2,16,Finite State Machines (FSMs),一、概 述,17,Finite State Machines (FSMs),input events,outputs,current state,next state,state,transition function,Finite state machines consist of:,Output Events,Input Events (or Signals, or Messages),Transition Functions,STATE,States,NEX
11、T STATE,CURRENT STATE,INPUT EVENTS,OUTPUTS,Transition Function,18,Finite State Machine States,Current State State which determines the current behavior of the machine Next State State which will machine have after processing an input event. Next State can be same as current Start State State in whic
12、h machine will be when created,19,FSM Transitions,input events,outputs,current state,next state,state,transition function,Triggered by input events the FSM moves from one state to other based on the Transition Function Transition Function produces the Output and Next State depending on Current State
13、 and Input Event While in particular state FSM is not active. It is waiting for an input to perform next activity,20,Finite State Machines (FSMs),二、形式化定义,21,FSM: Formal Definition,FSM is 5-tuple: FSM = (S, s0, I, , F), where S = s0, s1, , sn: 有限状态集合。在任一确定时刻，FSM只能处于一个确定的状态si。 I = a0, a1, , am: 有限输入字符
14、集合。在任一确定的时刻，FSM只能接收一个确定的输入aj。 ：S I S是状态转换函数，如果在某一确定的时刻，FSM处于某一状态si S, 并接收一个输入字符aj I，那么下一时刻将处于一个确定的状态 s = (si , aj) S。在这里规定，s = (s , )，即对任何状态s，当读入空字符时，有很状态机不发生任何状态转移。 s0 S是初始状态，FSM由此状态开始接收输入 F S是一个终态集（可空），FSM到达终态后不再接收输入 确定有限状态机也称为DFA（确定有限自动机）,22,Non deterministic FSM (or NFA),NFSM is 5-tuple: FSM = (
15、S, s0, I, , F), where S = s0, s1, , sn: 有限状态集合。在任一确定时刻，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)。在这里规定，s = (s , )，即对任何状态s，当读入空字符时，有很状态机不发生任何状态转移。 s0 S是初始状态
16、，FSM由此状态开始接收输入 F S是一个终态集（可空），FSM到达终态后不再接收输入,23,FSM: Formal Definition (Cont.),在一些情况下，如果讨论问题的重点集中在FSM的状态集(S)、输入集(I)和状态转换函数()上。这时可用如下两种方式来表示FSM： FSM = (S, I, )或 FSM = (S, s0, I, ),24,Finite State Machines (FSMs),三、Representation,25,State Transition Diagrams,Used to Visually represent an FSM Emphasis is on identifying states and possible transitions Circles represent States Arrows represent Transitions ei are in
