形式化描述技术概述FSM

《形式化描述技术概述FSM》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、网络协议工程第3讲：协议形式化描述技术8/18/20211形式化描述技术第3讲：协议形式化描述技术3.1概述3.2有限状态机(FSM)3.3PetriNet3.4SDL3.5Estelle3.6Lotos3.7ASN.18/18/20212形式化描述技术形式化描述技术：Why?通信系统行为的复杂性增大了行为描述的难度，人们必须借助一种语言或一种技术来准确地描述系统行为。在过去，人们习惯使用自然语言进行协议描述（用自然语言写协议的规格说明或规范）优点是：方便、易懂致命缺点是：不严格、不精确、结构不好、没有

2、描述标准和有二义性且很难进行协议实现、测试的自动化和协议验证。不同的人对协议描述的理解不一样导致不同的协议实现之间不能实现互连，甚至还会得出错误的协议。解决办法：形式化技术FDTs(FormalDescriptionTechniques)8/18/20213形式化描述技术FDTs：Aims采用形式描述技术的目的是：为开发者提供一种分析的方法；作为对开发结果验证的基础；为设计人员和应用人员提供交流途径；作为开发文档能在将来再开发时使用。理想的形式描述技术应该既能描述系统的行为特征，又能进行操作：在系统需求分

3、析和设计阶段，它应该是一种描述语言在系统实现阶段它应该是一种编程语言。形式描述技术是将协议工程各阶段在技术上衔接起来的纽带，因此它对协议工程的发展起决定性作用。8/18/20214形式化描述技术FDTs：特性用于协议的FDT一般应具有如下重要特性：完整的语法和语义定义体系结构、服务和协议的可表达性协议重要特性(如，无死锁)的可分析性支持复杂协议的管理(如，构造能力)支持逐步求精的方法支持实现独立性(包括并发性、非确定性和适当的抽象机制)支持协议生命期的各环节，包括验证、实现和测试支持自动或半自动设计、验证

4、、实现和维护方法应能准确地描述进程交互的各种原语8/18/20215形式化描述技术FDTs:Classification形式描述模型(FDM)状态变迁模型有限状态机FSM(FiniteStateMachine)扩展的有限状态机EFSM(ExtendedFSM)模型通信有限状态机CFSM(CommunicatingFSM)模型CarlAdamPetri的Petri网(PetriNet)时态逻辑TL(TemporalLogic)进程代数(AlgebraofProcess)R.Miler：通信系统演算CCS(C

5、alculusofCommunicationSystem)（进程代数据的基础）Hoare：通信顺序进程CSP(CommunicatingSequentialProcesses)（以CCS为基础）8/18/20216形式化描述技术FDTs:Classification(Cont.)形式描述语言(FDL)ISO制定的Estelle和LOTOSCCITT制定的SDLISO的ASN.1(抽象语法记法)对象管理组织OMG制定的统一建模语言UMLISO的抽象测试集描述语言的TTCN高级程序设计语言，如Pascal,C

6、,PL/1便于协议的实现大多数比较复杂、分析起来比较困难，且不支持非确定性的描述。8/18/20217形式化描述技术模型vs.语言模型含义一：对象或系统的抽象OSI/RM：网络系统的抽象模型含义二：描述对象或系统的方法或技术FSMPetriNet8/18/20218形式化描述技术Functionsvs.ComputationFunctionsspecifyonlyarelationbetweentwosetsofvariables(inputandoutput)Computationsdescribeho

7、wtheoutputVariablescanbederivedfromthevalueoftheinputvariables.8/18/20219形式化描述技术ModelofComputationAMoCisaframeworkinwhichtoexpresswhatsequenceofactionsmustbetakentocompleteacomputationAninstanceofamodelofcomputationisarepresentationofafunctionunderapartic

8、ularinterpretationofitsconstituentsNotnecessarilyabijection(infactalmostnever!)Examples:FiniteStateMachine,TuringMachine,differentialequation8/18/202110形式化描述技术模型vs.语言（续）形式语言具有严格的语法和语义可以精确、完全地表述协议的功能、性能及行为等以一种或多种数学方法