第3章-协议形式化描述技术(1-概述及FSM).ppt

《第3章-协议形式化描述技术(1-概述及FSM).ppt》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、第3章协议形式化描述技术（1-概述及FSM）内容提要概述1FSM22形式化描述技术：Why?通信系统行为的复杂性增大了行为描述的难度，人们必须借助一种语言或一种技术来准确地描述系统行为。在过去，人们习惯使用自然语言进行协议描述（用自然语言写协议的规格说明或规范）优点是：方便、易懂致命缺点是：不严格、不精确、结构不好、没有描述标准和有二义性且很难进行协议实现、测试的自动化和协议验证。不同的人对协议描述的理解不一样导致不同的协议实现之间不能实现互连，甚至还会得出错误的协议。解决办法：形式化技术FDTs(

2、FormalDescriptionTechniques)3FDTs：Aims采用形式描述技术的目的是：为开发者提供一种分析的方法；作为对开发结果验证的基础；为设计人员和应用人员提供交流途径；作为开发文档能在将来再开发时使用。理想的形式描述技术应该既能描述系统的行为特征，又能进行操作：在系统需求分析和设计阶段，它应该是一种描述语言在系统实现阶段它应该是一种编程语言。形式描述技术是将协议工程各阶段在技术上衔接起来的纽带，因此它对协议工程的发展起决定性作用。4FDTs：特性用于协议的FDT一般应具有如下重要

3、特性：完整的语法和语义定义体系结构、服务和协议的可表达性协议重要特性(如，无死锁)的可分析性支持复杂协议的管理(如，构造能力)支持逐步求精的方法支持实现独立性(包括并发性、非确定性和适当的抽象机制)支持协议生命期的各环节，包括验证、实现和测试支持自动或半自动设计、验证、实现和维护方法应能准确地描述进程交互的各种原语5FDTs:Classification形式描述模型(FDM)状态变迁模型有限状态机FSM(FiniteStateMachine)扩展的有限状态机EFSM(ExtendedFSM)模型通信有

4、限状态机CFSM(CommunicatingFSM)模型CarlAdamPetri的Petri网(PetriNet)时态逻辑TL(TemporalLogic)进程代数(AlgebraofProcess)R.Miler：通信系统演算CCS(CalculusofCommunicationSystem)（进程代数据的基础）Hoare：通信顺序进程CSP(CommunicatingSequentialProcesses)（以CCS为基础）6FDTs:Classification(Cont.)形式描述语言(FD

5、L)ISO制定的Estelle和LOTOSCCITT制定的SDLISO的ASN.1(抽象语法记法)对象管理组织OMG制定的统一建模语言UMLISO的抽象测试集描述语言的TTCN高级程序设计语言，如Pascal,C,PL/1便于协议的实现大多数比较复杂、分析起来比较困难，且不支持非确定性的描述。7模型vs.语言模型含义一：对象或系统的抽象OSI/RM：网络系统的抽象模型含义二：描述对象或系统的方法或技术FSMPetriNet8Functionsvs.ComputationFunctionsspecify

6、onlyarelationbetweentwosetsofvariables(inputandoutput)ComputationsdescribehowtheoutputVariablescanbederivedfromthevalueoftheinputvariables.9ModelofComputationAMoCisaframeworkinwhichtoexpresswhatsequenceofactionsmustbetakentocompleteacomputationAninstanc

7、eofamodelofcomputationisarepresentationofafunctionunderaparticularinterpretationofitsconstituentsNotnecessarilyabijection(infactalmostnever!)Examples:FiniteStateMachine,TuringMachine,differentialequation10模型vs.语言（续）形式语言具有严格的语法和语义可以精确、完全地表述协议的功能、性能及行为等以一

8、种或多种数学方法或形式模型为基础SDL：基于扩展的FSM和抽象数据类型Eetelle：基于扩展的FSM，是Pascal语言的扩充LOTOS：基于通信系统演算（CCS）和抽象数据类型语言ACTONE11模型vs.语言（续）模型与语言的差别不是很明显。不同文献有不同的说法。将模型与语言分开一些文献中的模型在另一些文献中成为语言或相反将模型与语言不分，统称为形式化描述技术事实上，模型也可以看成是一种形式语言文法：描述语言的语法结构的形式规则（即语法规则）Tur