搜索
四、协议的形式描述语言Slide1主要内容形式化方法协议的形式化模型协议的形式描述语言SDLSlide21、形式化方法Slide3形式化方法的引入系统行为的复杂性增大了行为描述的难度，必须借助一种语言或一种技术来准确的描述系统的行为。自然语言具有冗长、不完整、语句容易产生二义性、结构性差和没有描述标准等缺点。国际标准化组织建议用形式化方法来描述复杂的系统。形式化方法使得对通信系统的描述、实现和测试变得容易。Slide4与自然语言相比，形式化方法具有以下的特点：形式化的语法形式化的语义清楚的概念模型界面统一表示强大的表达和描述功能有助于系统的实现和完善形式化方法的特点Slide5形式化方法的最终目的为开发者提供一种分析、设计的方法作为对开发结果进行验证、测试的基础为设计和应用人员提供交流的途径作为开发文档易于今后的维护和再开发Slide62、协议的形式化模型Slide7协议的形式化模型有限状态机（FSM）Petri网时态逻辑TL通信进程演算Slide8有限状态自动机可定义为一个四元系统S，i，E，T，其中：–S：系统状态集，状态数有限；–i：系统初始状态，i∈S;–E：输入字母集；–T：转移函数集，是从SⅹE到S的映射；有限状态自动机（1）有限状态自动机（2）单比特奇偶检验器的有限状态自动机偶奇11Slide900Slide10扩展有限状态自动机（1）扩展有限状态自动机定义为一个四元系统S，i，E，T，其中：–S：系统状态集，状态数有限；–i：系统初始状态，i∈S;–E：输入事件集；–T：转移函数，是从SⅹE到S的映射扩展有限状态自动机（2）转换函数的定义：SiSj∈T，Si，Sj∈S–t=e/p：a；或–t=e/a；或–t=e其中：e∈E，p为谓词，表示条件；a表示动作Slide11t等AK扩展有限状态自动机（3）等待DC等CCDC未连接AKTDTreq/DTCC/TCONconfTDISreq/DR已连接TCONreq/CR传输层协议机Slide12Slide13可通信的扩展有限状态自动机系统的行为通过可通信的扩展有限自动机来描述–系统由扩展的有限状态自动机组成–扩展的有限状态自动机具有与外界通信的能力：输入/输出动作Slide14Petri网Petri网的概念最早是由德国的CarlAdamPetri于1962年提出的。它是一种适合于并发、异步、分布式系统描述与分析的图形数学工具。Petri网已成为网络协议分析和设计的典型形式化模型之一。Slide15时态逻辑（TL）它涉及含有时间信息（现在、过去、将来、之前、之后等）的事件、状态及其关系的命题、谓词和演算。P1=a.(c.NIL+b.NIL)P1=Q2IQ3（选择）（并行）通信进程演算（CCS）是计算机通信系统的基本理论模型，也是许多形式化语言的基础。CCS的基本成分是事件和进程，而进程是通过顺序、选择和并行三个基本算子来定义的。P1=a.b.NILP2=a.b.P2（顺序）Slide173、协议的形式描述语言Slide18ESTELLE为准确描述OSI协议，ISO的FDT（形式描述技术）小组于20世纪80年代初开始进行形式描述语言的开发研究。最初提出了20多种方法，大致可归结为2类：基于有限状态机语言类和基于代数方法语言类。ESTELLE（一种扩充的有限状态机语言）是前一类语言的典型代表。1989年，ISO公布了作为形式描述技术国际标准之一的ESTELLE。ESTELLE是基于扩展的有限状态机，是一种形式化、数学化，并且与具体实现相独立的描述技术。它具有良好的结构和定义，并且具有很强的表达能力，可以完整、一致、简练、准确的描述分布、并行信息处理系统。ESTELLE的特点：基于扩展有限状态机，专为描述协议而设计；是Pascal语言的扩充，是面向协议实现的FDL；模块之间的通信方式为异步通信；对并发、不确定性、超时、异步通信状态转换有较强的表达能力，但对递归、共享通道、同步通信的表示不足；其所描述的协议很容易转换为FSM、Petri网模型，不容易转换成TL、CCS模型。Slide19ISO的FDT（形式描述技术）小组经过8年多时间的努力，于1988年8月完成了作为国际标准的形式描述语言（LOTUS,LanguageofTemporalOrderingSpecification）。LOTOS的基本思想是：外部可观察到的系统行为由一系列的交互作用组成，通过对这些交互作用的时间关系进行定义，从而描述整个系统。LOTOS的特点：基于进程代数CCS和多类代数的FDL；进程通信为同步通信；不是面向协议实现的语言；其所描述的协议很容易转换为CCS模型，也比较容易转换成TL、FSM、Petri网模型。LOTOS的不足之处：无异步通信机制、无清晰的记录型数据结构的描述手段、无常量描述手段、可读性差。LOTOSSlide20SDLSDL（SpecificationandDescriptionLanguage）是ITU-T提出的一种形式化描述语言，由Z.100建议定义。SDL的版本：–SDL-88：是后续版本的基础–SDL-92：引入面向对象的概念–SDL-96：对SDL-92的完善–SDL-2000：对面向对象的特征作了进一步的扩展；引入了其它语言，如ASN.1、ITU-TODL、UML等Slide21SDL的特点可用于需求分析到具体实现的整个开发过程。适应于实时系统基于扩展的有限状态机图形化表示方式，可视性强具有面向对象的特征Slide224、SDLSlide23内容SDL语言概述SDL基本概念SDL中的数据Slide244-1、SDL语言概述Slide25SDL的应用（1）SDL主要应用于电信领域，适用于描述活性离散系统。–活性：是指系统对外来的信号（输入）是有反应（输出）的–离散：是指系统与环境的信息交互不是连续的Slide26SDL的应用（2）既可以用来说明（specification）一个系统应具有的行为（behaviour）；又可以用来描述（description）一个系统实际具有的行为（behaviour）。SDL可用来制作以下文档：–需求说明–ITU-T建议–系统设计说明–系统设计描述–系统测试说明SDL的系统和环境系统环境交互信号SDL系统环境信号SDL系统层次关系系统功能块功能块进程功能块进程进程功能块进程Slide29SDL系统包含关系SDL系统功能块图进程图Slide30SDL中的主要术语代理（agent）系统（system）功能块（block）进程（process）信号（signal）信道（channel）状态（state）实例（instance）过程（procedure）数据类型（sort）进程标识（pid）Slide31SDL文法概述graphicalgrammarabstractgrammarcommontextualgrammarSDL/GRSDL/PRtextualgrammarSlide324-2、SDL基本概念Slide33系统（1）SDL系统：完整地描述一个真实系统或一个真实系统中相对独立的一部分。一个系统可以划分为若干个功能块；功能块之间以及功能块与环境之间用信道相连。系统各功能块之间以及功能块与环境之间可以使用信号通信；信号通过信道来传递。系统的文本域：用来定义信号、信号列表、数据类型、变量等，这些定义包含在文本符内。系统的交互域：描述系统图中功能块的划分情况以及信道的设置情况。Slide34系统（2）Slide35功能块（1）功能块包括一个或多个并发的功能块或进程；功能块文本域定义本功能块内部信号、信号列表、数据类型等内容；功能块的交互域描述本功能块中功能块或进程的组成及交互关系；在功能块图的边界上，要标出与本功能块相连的信道标识。Slide36功能块（2）Slide37功能块（3）Slide38进程（1）进程是系统的基本组成单位，系统的行为主要由进程来描述；进程图中每个进程实例都有一块私有存储空间，记录进程图中定义的变量的数值及实例所处的状态。Slide39进程（2）进程实例一旦被创建，就拥有了一个自己的pid，通过以下四种pid表达式可以得到进程实例的pid：–self返回本进程实例的pid；–sender返回发送最近被消耗信号的进程实例的pid；–parent返回创建本进程实例的进程实例（父进程）的id；–offspring返回最近被本进程创建的进程实例（子进程）的pid。Slide40进程（3）进程中可以定义过程，过程图可被包含在进程图中，也可单独定义。在进程图中用过程符来说明定义关系。如果在进程图中包含了过程符，则在SDL描述中必然有具有相同过程名的过程图存在。过程只能由包含该过程的进程的实例来调用，如果该进程以外的代理实例要调用该过程，就必须把该过程声明为远端过程（remoteprocedure）。proc1‘状态机图’进程（4）usepackagenameprocessprocessnameagentformalparameters‘定义变量等’Slide42过程（1）过程是进程的一部分过程不存在过程实例，它可由包含该过程的进程集的所有实例来调用过程用过程图来定义过程中还可以定义过程过程可以带参数，参数类型有三种：in/out，in，out；过程还可以定义成返回型过程，返回值类型定义跟在形参定义后面过程可以有状态，但过程没有独立的输入队列Slide43过程（2）procedureProc1in/outxinteger,inyinteger-rsltchar‘定义变量、定时器等’‘过程图形域’usepackagenameSlide44过程（3）过程图形域是过程的主体内容，与状态机图形域基本相同，但有以下不同：–起始符不同，过程起始符定义为：–状态机图可以没有终止符，而过程图必须有至少一个返回符，返回符定义为：带表达式的返回符仅用于要求返回值的过程，表达式的值即为本次过程调用的返回值Slide45通信SDL系统的通信手段包括–系统与环境之间或系统中的各代理之间交互信号–远程过程调用–使用远端变量Slide46信道（1）信道是用在代理与代理之间或代理与系统环境或信关之间传递信号的通道。信道分为单向和双向两种，在每个方向上需列出在该方向上传递的所有信号，这些信号用方括号（[]）括起来，标在信道的箭头处。信道分为：–延迟信道：表示信号从源端到目的端要经过一定延迟，延迟时间是不确定的，但信道上的信号仍是有序的–非延迟信道：表示信号从源端发出后直接到达目的地，没有延迟Slide47信道（2）延迟信道（单向）延迟信道（双向）非延迟信道（单向）非延迟信道（双向）Slide48信号（1）信号是SDL系统中代理之间通信的基本单位信号必须在信道中传输要利用信号来通信，必须：–信号定义：在相关代理图的文本域中定义信号；–信号与信道关联：在信道的信号列表域中列出信号，说明信号可以在哪些信道中传递信号可以定义参数，定义过的信号可以用来定义信号列表。信号列表的定义也在文本符中定义。在信道上列出信号和/或信号列表时，信号列表标识符要用圆括号括起来，以区别于信号Slide49信号（2）定义举例signalcall_hkof,call_hkon,dial_number(integer);signalcalled_hkof,called_hkon;Signaltimeout(char,integer);signallistcall_input=call_hkof,call_hkon,dial_number,timeout;signallistcalled_input=called_hkof,called_hkon,timeout;Slide50信号（3）Slide51状态机——开始域（1）每个状态机有且仅有一个开始域开始域由开始符下接迁移过程组成开始符迁移过程：迁移过程由一系列动作组成，如输出信号、变量赋值、调用过程、创建实例等。Slide52状态机——开始域（2）开始域的一般情况最简单的开始域是从开始符直接进入状态transi