4协议形式描述语言.ppt
80页
2024/8/101第四章 协议形式描述语言4.14.1引言引言 协议可以用自然语言，程序设计语言，形式描述语言或专用语言描述1 1、用自然语言描述协议特点：、用自然语言描述协议特点： 用自然语言描述的协议可读性好（正因为如此，ISO仍然用自然语言描述并颁布协议标准），但描述不准确，有二义性 更重要的问题是，从自然语言描述的协议到协议的实现从自然语言描述的协议到协议的实现是一个复杂的、效率低的、一致性很差的，必须手工完成的是一个复杂的、效率低的、一致性很差的，必须手工完成的过程过程所谓一致性差是指：对同一个协议，不同的人得出不同的实现版本对自然语言描述的协议进行正确性验证，以及从中导出测试序列的工作，存在同样的问题 2024/8/102第四章 协议形式描述语言2 2、程序设计语言描述协议特点、程序设计语言描述协议特点（1） 用经典的程序设计语言（例如Fortran，C，Pascal）描述协议便于协议的实现2）可读性差3）程序设计语言表述协议并发性、不确定性，以及其他协议性质和协议元素性质的能力较差4）由于程序设计语言描述的协议过多的描述了协议实现细节（有些和实现环境相关），因此它只能作为协议实现规范在小范围内使用，而不能作为协议标准在世界上颁布。
5）用程序设计语言描述的协议对协议验证和测试来说，协议的处理仍然是不方便的 2024/8/103第四章 协议形式描述语言 为了克服自然语言和程序设计语言的缺点，一些大计算机公司使用了专用协议描述语言例如IBM公司的FAPL（Form and Protocol Language）就是一种专为提高IBM公司网络软件（SNA，system Network Architecture）的开发效率而设置的专用语言 2024/8/104第四章 协议形式描述语言3 3、、协议描述语言特点特点 使用形式化协议描述语言有许多优点所谓所谓““形式化形式化””即即““模型化模型化””和和““抽象化抽象化””一种形式描述语言必然基于一种或几种数学模型（如第三章介绍的FSM，Petri网 ，TL和CCS），这就为充分地表述协议的各种特性（并发性，不确定性，时序性，递归性等）为协议验证、协议实现、协议测试和协议转换过程的系统化和自动化提供了良好的基础 由于形式描述语言形式描述语言有很好的数学基础，用它描述的协议在语义上无二义性，同时由于它抽象于具体的协议实现环境，因此它可作为协议标准的描述语言形式描述语言简称FDL（Formal Description Languages） 2024/8/105第四章 协议形式描述语言 FDL的基础是协议模型技术，从这个意义上说，本章是第三章的继续。
然而，从协议模型技术到FDL还有许多工作要做首先，作为一种语言，一种FDL在语法上和语义上必须是一个完整的体系另外，一种FDL往往要对一种模型技术进行扩充，或将几种模型技术拟合在一起，取长补短，使之具有很强的表达能力和应用能力 八十年代以来，计算机科学家已提出许多种FDL，有些是专为协议工程而研制的，有的是为分布（并行）计算以及软件工程而提出的对协议工程来说，由国际标准化组织（对协议工程来说，由国际标准化组织（ISOISO））颁布的颁布的ESTELLEESTELLE和和LOTOSLOTOS，以及国际电报咨询委员会，以及国际电报咨询委员会（（CCITTCCITT）颁布的）颁布的SDLSDL是应用最广的是应用最广的FDLFDL本章重点介绍ESTELLE和LOTOS 2024/8/106第四章 协议形式描述语言4.2 ESTELLE4.2 ESTELLE概述概述 ESTELLEESTELLE是是19891989年年ISOISO公布的基于扩展的有限状态机公布的基于扩展的有限状态机（（EFSM)EFSM)，是一种形式化、数学化、并且与具体实现相独立的，是一种形式化、数学化、并且与具体实现相独立的协议形式化描述语言。
协议形式化描述语言 ESTELLEESTELLE是是PASCALPASCAL语言的扩充语言的扩充 2024/8/107第四章 协议形式描述语言 在在ESTELLEESTELLE中，中，（（1 1））一一个个系系统统被被理理解解成成是是由由许许多多相相互互通通信信的的模模块块分分层层嵌嵌套套而而构成的构成的（（2 2））模模块块之之间间通通过过通通道道进进行行通通信信，，即即通通道道将将一一个个模模块块的的输输出出与另一个模块的输入队列连接起来与另一个模块的输入队列连接起来3 3）通道和模块之间的连接点称为交互点通道和模块之间的连接点称为交互点4 4））模模块块间间的的信信息息传传递递称称为为交交互互每每个个模模块块相相当当于于一一个个有有限限状状态态自自动动机机，，有有限限状状态态集集的的每每个个状状态态迁迁移移或或转转换换都都是是由由于于某某些些输输入入所所触触发发，，状状态态迁迁移移过过程程中中可可能能会会产产生生输输出出这这里里的的输输入入对对应应于于模模块块所所收收到到的的消消息息，，而而输输出出则则对对应应与与模模块块向向其其他他模模块所发送的消息。
块所发送的消息 2024/8/108第四章 协议形式描述语言用ESTELLEESTELLE来描述协议规格时，其整体结构大致如下：来描述协议规格时，其整体结构大致如下：Specification Specification 规格名规格名全局参数（全局参数（Global parameterGlobal parameter））通道（通道（channelschannels））模块头（模块头（Module headersModule headers））模块体（模块体（module bodiesmodule bodies））规格主体（规格主体（Main bodiesMain bodies））EndEnd其中，模块体中最重要的是状态转换（迁移）其中，模块体中最重要的是状态转换（迁移） 2024/8/109第四章 协议形式描述语言形式描述语言形式描述语言ESTELLEESTELLE有以下基本特点：有以下基本特点：1.1.基于扩展的有限状态机（基于扩展的有限状态机（EFSM),EFSM),专为描述协议而设计专为描述协议而设计2.2.ESTELLEESTELLE是是PascalPascal语言的扩充用他描述的协议很容易转换成语言的扩充。
用他描述的协议很容易转换成PascalPascal或或C C代码，因此它是一种面向协议实现的形式描述语言代码，因此它是一种面向协议实现的形式描述语言3.3.模块实例可通过初始化语句动态产生如果协议实现后模块实例对应模块实例可通过初始化语句动态产生如果协议实现后模块实例对应一个进程或任务，那么网络进程或任务也是动态产生的一个进程或任务，那么网络进程或任务也是动态产生的4.4.模块之间的通信方式为异步方式模块之间的通信方式为异步方式5.5.ESTEILEESTEILE对并发、不确定性、超时、异步通信状态有较强的表到能力，对并发、不确定性、超时、异步通信状态有较强的表到能力，但对递归、共享通道、同步通信、协议性质的表现尚缺乏有力的手段但对递归、共享通道、同步通信、协议性质的表现尚缺乏有力的手段6.6.从从ESTEILEESTEILE描述中易于提取协议的描述中易于提取协议的FSMFSM模型或模型或PetriPetri网模型，但是不容易网模型，但是不容易提取提取TLTL和和CCSCCS模型 2024/8/1010第四章 协议形式描述语言 用ESTEILE来描述一个协议，最重要的工作就是构造协议的模块结构和通信机制，主要包括：系统中模块的层次构成，模块的类别、通道和交互点的定义、交互点队列的属性，以及模块和通道的连接问题。
2024/8/1011第四章 协议形式描述语言4.2.14.2.1模块概念模块概念1.1.模块（模块（modulesmodules）） ESTELLE将一个系统看作是由许多相互通讯的模块分层嵌套而构成的系统每个父模块控制对其子模块的创建和销毁，系统的每一级可有许多个模块，每个模块可通过通道以异步方式和其他的模块通讯 2024/8/1012第四章 协议形式描述语言 模块的定义由两部分组成：模块头和模块体组成1）模块头定义（module-head-definition） 每个模块头可对应一个或多个模块体模块头定义包括两个重要部分： ①外部交互点（external interaction points） ②输出变量（exported variables） 2024/8/1013第四章 协议形式描述语言（2）模块体定义（module-body-definition） 模块体定义包括三个主要部分： ①说明部分（declaration -part）②初始化部分（initialization-part）③转换部分（transition-part） 说明部分对模块所使用的通道（channels）、内部交互点（internal interaction points）、数据类型和变量、模块状态、调用的过程和函数进行说明。
初始化部分说明模块初起时各变量和模块状态的初始值 转换部分是模块的关键部分，它按照EFSM定义模块状态转换过程模块描述的非形式结构示意如下： 2024/8/1014第四章 协议形式描述语言Module 模块头——A 模块类别 外部交互点说明 输出变量说明End;Body 模块体-1 for 模块头-A 通道说明； 内部交互点说明； 数据类型和变量说明； 模块状态定义；过程和函数定义；模块初始化部分；状态转换部分；End；Body 模块体-2 for 模块头-A . . .End； 2024/8/1015第四章 协议形式描述语言2 2．模块实例（．模块实例（module instancesmodule instances）） 协议运行时，用ESTELLE定义的一个模块体可同时生成一个或多个模块实例，模块实体并可动态产生和消失同一个模块体的不同模块实例用模块变量（module variables）来标识父模块实例初始化时负责子模块实例的生成例如，Mod varMv-1： 模块头-A；Mv-2： 模块头-A；Initialize Begin Init mv-1 with 模块体-1； Init mv-2 with 模块体-2； ……………………End；这里用变量mv-1表示模块体-1的实例，mv-2标识模块体-2的实例。
2024/8/1016第四章 协议形式描述语言在一个自动回叫系统例子中，共定义三个模块头，每个模块头对应一个模块体，其中模块MA的描述如下：Module MA systemprocess ip P:CA(PartyA)EndBody BA for MA...END 2024/8/1017第四章 协议形式描述语言ESTEILE所定义的一个模块体，在协议运行过程中可同时生成一个或多个实例，模块实例可动态产生和撤销不同模块实例用模块变量来标识（module variables）,在ESTEILE中模块实例的生成部分包括在规格主体部分（main bodyes）中例如在自动回叫系统的例子最后Modvar partyA:MA partyB:MB Agent:MGInitilize begin init partyA with MA; init partyB with MB; init Agent with MG; ……end 这里，首先说明了三个模块变量partyA, partyB, Agent,它们分别对应模块MA, MB, MG,然后初始化部分生成实例。
2024/8/1018第四章 协议形式描述语言3.3.模块类别（模块类别（module classesmodule classes））按模块内容是否包含状态转换部分来说，模块分为：(1) 非活跃模块（inactive modules） 模块体内无状态转换的部分的模块叫做非活跃模块，初始化非活跃模块所产生的模块实例也是非活跃的2) 活跃模块（active modules）模块体包括状态转换部分的模块叫做活跃模块3) 特征模块（attributed modules） 当一个模块头定义有多个模块体定义与之关联时，如果至少有一个模块体内包含状态转换部分，此种模块叫做特征模块 2024/8/1019第四章 协议形式描述语言 按照模块工作方式进行分类，模块定义时，模块类别指明模块的工作方式模块类别指明所定义的模块是n系统进程模块（system process）n系统活动模块（system activity）n进程模块（process）n活动模块（activity） 2024/8/1020第四章 协议形式描述语言(1) 系统进程模块（System process） System process本身可以是特征模块，但它的父模块必须为非特征模块。
它的子模块可是任何类别的模块，父进程必须是system process它的工作方式：父模块优先于子模块，兄弟模块并行（并发）假定一个system process有三个子模块当system process有转换需要执行时，不管子模块是否有转换要执行，system process的转换优先执行当system process无转换要执行时，如果三个子模块都有转换要执行，三个转换并行执行 2024/8/1021第四章 协议形式描述语言(2) 系统活动模块（System activity） System activity本身可以是特征模块，它的父模块必须为非特征模块，并且必须是system process或system activity 它的子模块必须是活动模块（activity）系统活动模块的工作方式是：父模块优先于子模块，父模块优先于子模块，兄弟模模块串行执行（选择是随意得）块串行执行（选择是随意得）假定一个系统活动模块有三个子模块，当系统活动模块本身有转换要执行时，不管子模块是否有转换，它先执行自己的转换当它自己无转换要执行时，如果三个子模块都有转换要执行，则它从三个activity中任选一个转换执行，并且这种选择是不确定的(nondeterminic )。
2024/8/1022第四章 协议形式描述语言（（3 3）进程模块（）进程模块（processprocess）） 它必须为特征模块，它的子模块不能为systemprocess和systemactivity，只能为process它的工作方式和systemprocess相同4 4）） 活动模块（活动模块（activityactivity）） 活动模块必须为特征模块，它的子模块只能为activity它的工作方式和systemactivity相同 2024/8/1023第四章 协议形式描述语言图4.1为一个协议运行时各模块实例的嵌套情况虚线边框为非活跃模块最高层模块为整个协议规范模块（SP） 2024/8/1024第四章 协议形式描述语言(a) 假定 A 无转换要执行 A1 无转换要执行 A11有t11要执行 A12 有t12要执行 A2有t2要执行此时，模块实例A选择执行的转换可能为{t11，t2}或}{t12，t2}b) 假定(a)中有转换要执行，那么A选泽{t1，t2}c) 假定(a)中也无转换要执行，那么A选择t11或t12 。
d) 假定(a)中A有t转换要执行，那么A选择自己的t. 2024/8/1025第四章 协议形式描述语言4.4.模块嵌套规则模块嵌套规则( (module nesting rulesmodule nesting rules) )system process和system activity统称之为系统模块模块嵌套的规则为:(1）系统模块的父模块必须为非特征模块(2)系统模块的子模块必须为特征模块3)同一级可有多个系统模块4)非系统模块的子模块不能为系统模块(5)system process的子模块可以是process或activity；system activity的子模块必须为activity6)process的子模块必须为process，activity的子模块必须为activity7)非活跃模块头定义可以不指明“模块类别” 2024/8/1026第四章 协议形式描述语言5 specification模块用ESTELIE描述一个协议时，描述规格总是从关键词specification开始由specification开始的整个协议描述也是一个模块，它是最高层的模块 Specification模块可以是非活跃模块，也可以是系统模块（systemprocess或systemactivity）.例如：Specification AC;说明了整个规格名称为AC，同时AC也是本规格中的最高层模块。
2024/8/1027第四章 协议形式描述语言4.2.2 模块诵讯模块诵讯1.通道（channels)通道定义包括通道名、通讯角色和各个通讯角色向通道施加交互信息三部分一般情况下，一个通道只有两个通讯角色（一端一个)每个角色向通道发出什么交互信息(即报文名、服务源语名等)，以及各个交互所附带的参数都必须在通道定义中给出例如，ISO传输层的服务访向点（TSAP）可定义为一个通道：channel tsap — type（user，provider）； by user： t一connection — req（source：address — type，...）； t一data — req（user —data：user — data — type，...）；. by provider： t一 connection一ind（source：address — type，...）； t 一 data一ind（user —data：user — data — type，...）；.这里，通讯角色user即为传输层用户，provider即为传渝层协议实体，它们向通道施加的交互信息都是传输层协议的服务源语。
2024/8/1028第四章 协议形式描述语言例2：如果通道为buy,其通信角色有Customer和VendorCustomer向通道施加的交互信息为coin，而vendor向通道施加的交互信息为trinketChannel Buy（customer，vendor）； by customer； coin； by vendor； trinket； 2024/8/1029第四章 协议形式描述语言在3.1.5中自动回叫系统的例子，我们定义两个通道CA、CB，CA用于模块实例PartyA与Agent之间进行通信，CB用于模块实例PartyB与模块实例Agent间的通信Channel CA（PartyA，Agent） by PartyA：ac；answer；hangupa；noanswera； by Agent：busytonea；connect；ringa；Channel CB（PartyB，Agent） by PartyB：answerb；available；busyb； by Agent：checkb； ringb；stopringb； 2024/8/1030第四章 协议形式描述语言2.交互点（interaction points） 一个通道定义二个通讯角色，这不意味着只能有两个模块使用一个通道。
多个模块可扮演同一个通讯角色使用同一个通道一个模块必须定义一个交互点之后才能将它自己与一个通道联系起来如果一个模块要使用父模块定义的通道，它必须在模块头定义中给出交互点定义，这种交互点叫做外部交互点如果一个模块要使用它自己定义的通道，那么它必须在模块定义中给出交互点定义、这种交互点叫做内部交互点交互点简称ip 2024/8/1031第四章 协议形式描述语言3.交互点的约束（ip binding） 一个独立的交互点无通讯能力，只有当两个以上的交互点约束(bind)在一起时，一个交互点的输入事件才能作为输出事件传递到另一个交互点connect语句和attach语句将交互点约束在一起，disconnect和detach解除ip的约束1)connect格式：connect ip — 1 to ip一2ip — 1 to ip一2必须是定义在同一个通道两端的交互点(通讯角色相反)发出connect语句的模块可以将两个子模块的外部ip约束在一起;可以将它自己的两个内部ip约束在一起;可以将它自己的一个内部ip和一个子模块的外部ip约束在一起 2024/8/1032第四章 协议形式描述语言(2)disconnect格式：disconnect ip — 1 或 ip一2 disconnect解除由connect约束在一起的ip。
解除ip — 1的约束也就解除了ip — 2的约束3) attach格式：attach eip to child一eip发出attach语句的模块将它自己的外部ip（eip）和它的一个子模块的外部ip(child -eip)约束在一起eip和child — eip必须是定义在同一个通道同一端的互点(通讯角色相同〕4) detach格式：detach eip或child一eip解除eip或child一eip中任何一个交互点的约束就自动解除另一个ip的约束口 2024/8/1033第四章 协议形式描述语言4．联接端点(connection endpoints) 多个ip利用多条conncet语句和attach语句串行约束在一起可形成一条联接(connection) ,联接两端的ip叫做联接端点联接的主要特征是：进入一个联接端点的输入将自动传递到另一端的联接端点的队列中，中间ip的队列隐藏起来 为了说明通道，交互点约束的概念，举例如下图4.2是一个由四个模块W，X，Y，Z嵌套而成的系统（W，X，Y，Z为模块变量名),a为W的内部ip, b为X的外部ip，c为Y的外部ip, d为Z的外部ip。
通道CH由模块W定义在W的模块体中，channel CH(user, provider)； by user：…… by provider：……ip a：CH(user) individual queue； 2024/8/1034第四章 协议形式描述语言在X的模块中头中ip b：CH(provider) individual queue；在Y的模块中头中ip c：CH(provider) individual queue；在X的模块中头中ip d：CH(provider) individual queue； 2024/8/1035第四章 协议形式描述语言在各自的模块中发出connect或attach语句（图中所示），四个ip形成一条联接，a和d为联接端点从a输入的信息进入d的队列，从d输入的信息进入a的队列如果在Y中发出detach c，那么联接端点改为a和c如果在X中发出detach b，那么联接端点改为a和b，c和d变为非约束ip如果在W中发出disconnect a，那么由b，c和d形成的联接无通讯能力 2024/8/1036第四章 协议形式描述语言5．ip队列（输入队列） 定义ip时必须指明ip的队列性质：common queue或individual queue。
多个模块使用同一个通道时，它们可使用自己的单独队列，也可以共享队列如果定义在通道同一端的ip队列为common queue，那么定义这些ip的模块使用共享队列 2024/8/1037第四章 协议形式描述语言图4.3示出一个特别的例子交互点a，b，e和f的队列为common queue，而c和d的队列为individual如果利用connect语句将a和d约束在一起，b和e约束在一起，c和f约束在一起，那么信息传递特性如下：a的输入事件进入d的单独队列，f的输入时间进入c的单独队列，d和e的输入事件进入a和b的共享队列，b和c的输入事件进入e和f的共享队列 2024/8/10386. 输入和输出 when 语句从ip读一个事件，而output语句往ip输入一个事件格式为：when ip.m(arquments)output ip.m(arquments)这里m(arquments)必须是channel定义中指明交互事件.when语句从ip的队列(FIFO)读出事件,该事件是联接的另一端output语句所输入的事件.由于FIFO队列的原因,输出和输入不是同时发生的,因此模块通讯是异步的 第四章 协议形式描述语言 2024/8/1039第四章 协议形式描述语言4.2.3 4.2.3 状态转换的描述状态转换的描述 状态转换部分是模块中最重要的部分.模块状态转换的描述基于扩展有限状态机模型(EESM),其描述直观明了：1 1、描述语句、描述语句 trans 表示状态转换群开始,一个模块体可有多个状态转换群.when ip.m 从ip读一个事件from A 转换发生前的状态为Ato B 转换发生后的状态Bprovided E 转换的条件,E为布尔表达式delay(E1,E2) 转换至少延迟单位时间,最多单位时间.单位时间的大小 在全局specification语句中说明priority E 转换的优先级为E,E为布尔表达式.any var do 当内容相同的一组转换存在,而变量var值不同时,可用 此语句缩短转换的描述. 2024/8/1040第四章 协议形式描述语言例如:trans when ip.m from A any x:1……3 do provided E(x) to C begin S1;S2;… end;这里any语句把X=1,X=2和X=3时三个转换合成一个简练的转换.如果不用any语句,上述描述必须重复三次,每次转换中的provided语句不同,其它相同. S1,S2,….为转换所执行的事件或过程(包括output语句). 2024/8/1041第四章 协议形式描述语言2 2 转换的选择和执行转换的选择和执行转换可分成三种状态:(1) Enabled: 如果when,from和provided语句得到满足,该转换变成enabled状态.(2) Fireable:如果delay和priority语句得到满足,那么一个enabled转换变成fireable状态.如果无delay和priority语句.那么enabled状态和fireable状态相同.(3) Offered:对于某个模块实例来说,它和它的子模块中可能存在多个fireable转换,模块将选择一个或多个转换交付执行,被交付执行的转换叫做offered转换.模块怎样选择fireable转换取决于模块本身类别和子模块的结构.选择按4.2.1所述的原则先父后子,process并行,activity串行. 被交付的转换怎样执行在协议实现中解决,ESTELLE只认为交付的转换就一定执行. 2024/8/1042第四章 协议形式描述语言4.2.4 AB4.2.4 AB协议的协议的ESTELLEESTELLE描述描述 本节所描述的整体AB协议系统(类别为system process)如图4.4所示.系统中存在多个AB协议模块实例(类别为process),每个AB协议对应一个用户模块实例(类别为process).所有AB协议模块实例共享一个网络模块实例(类别process).用户模块实例和网络模块实例为外部模块(external),它们由其它ESTELLE文本描述. 2024/8/1043第四章 协议形式描述语言图4.4 AB协议系统 2024/8/1044第四章 协议形式描述语言 系统定义两个通道:U—access—point和N—access—point.前者为AB协议模块与用户模块的接口,后者为AB协议模块和网络模块的接口。
接口(通道之间)的通讯原语示于图4.4中. AB协议模块既是sender也是receiver.为了缩小状态转换部分的篇幅,（1）AB协议模块作为sender只定义了两个状态:ESTAB(初始状态),ACK—WAIT(等待认可报文),（2）作为receiver没有定义状态.（3）多个用户实例和多个AB协议模块实例用数字标识. 2024/8/1045第四章 协议形式描述语言 Sender用Source_id标识它自己，并由Send-request和data-request的参数destination决定如果有n个用户，那么通道N-access-point两端各定义n个ip,并用n个connect语句约束在一起 2024/8/1046第四章 协议形式描述语言示例程序： 2024/8/1047 2024/8/1048 2024/8/1049 2024/8/1050 2024/8/1051 2024/8/1052第四章 协议形式描述语言4.2.5 ESTELLE4.2.5 ESTELLE的特点与应用方法的特点与应用方法 ESTELLE的基本特点可归纳如下：(1) 基于扩充有限状态机(EFSM)的FDL，专为协议描述而设计。
·模块实例可通过初始化语句动态产生如果协议实现后模块实例对应于一个进程或任务，那么网络进程或任务也是动态产生的2) 模块通讯为异步通讯3) ESTELLE是pascal语言的扩充，用ESTELLE描述的协议容易转换成pascal或C代码因此，它是一种面向协议实砚的FDL4) ESTELLE对并发、不确定性、超时、异步通讯状态转换有较强的表达能力，但对递归、共享通道（广播通道）、同步通讯、协议性质（如不变性等）的表示缺少有力的手段 2024/8/1053第四章 协议形式描述语言用ESTELLE描述的协议易于提取FSM模型和Petri网模型，但不容易提取转变成TL和CCS模型 用ESTELLE描述一个协议，最重要的工作(也是第一步工作)就是构造协议的模块结构和通讯机制系统由多少层模块构成？每个模块应该是什么类别(类别决定了工作方式)？定义多少通道和交互点？交互点队列属于哪种？它们约束成什么样联接？这些问题必须作出周密安排；否则将影响协议实现后执行效率，例如应该定义为system process类别的模块定义system activity之后，并行性就会失去论文[3]给出了ISO传输层协议的ESTELLE描述。
是一篇很好的参考资料 2024/8/1054第四章 协议形式描述语言4.3 LOTOS4.3 LOTOS概述概述 LOTOS 的基本思想是： 外部可观察到的系统行为由一系列的交互作用组成， 通过对这些交互作用的时间关系进行定义， 从而描述整个系统在定义这些交互作用的时间关系时，不是采用时序逻辑的方式，而是基于进程代数的方法 LOTOS 规 格（ specification ）主要包括数据类型的定义和进程的定义两个部分，其整体结构大致如下 ： SPECIFICATION 规格名 全局类型定义 进程定义 ENDSPEC LOTOS 具有如下基本特点 1.LOTOS 是基于进程代数 CCS 和多类代数 (Many-Sorted Algebra) 的 FDL ，是一种为适应协议工程、分布处理和并行处理技术的要求而产生的语言2.进程通信为同步通信3.LOTOS 不是面向协议实现的语言例如，它只是在抽象数据类型定义中给出协议内部操作的性质说明，而没有给出操作怎样实施的说明从而，在将 LOTOS 描述的协议转变成程序设计语言（如 C,Pascal ） 代码时需要做许多工作。
4.用 LOTOS 描述的协议很容易转换成 CCS 或 CSP 模型，也比较容易转换成 TL, FSM 或 Petri 网模型5.LOTOS 的不足之处体现在以下几个方面无异步通信机制，无清晰的记录型数据结构的描述手段，无常量描述手段，可读性差等 2024/8/1055第四章 协议形式描述语言 4.3.1 4.3.1 进程定义进程定义 LOTOS将一个系统看做多个相互作用的子进程组成的进程，每个子进程又是由多个子进程构成进程定义为：process process-id [gate-list] (parameter-list):noexit:=
2024/8/1056第四章 协议形式描述语言 2024/8/1057第四章 协议形式描述语言图 3-8 具有门径 a～g 的进程 P 2024/8/1058第四章 协议形式描述语言进程 Max3 的空间表示 LOTOS 进程中定义的典型结构 2024/8/1059第四章 协议形式描述语言4.3.2 4.3.2 行为算子行为算子 多个协议事件和行为表达式可用行为算子组合成新的行为表达式1.行动前辍(action-prefix) 行动前缀(用符号”;”)说明进程顺序执行事件的行为，它对应于CCS的“.”算子例如：2.选择(choice) 选择(用符号”[]”)说明进程从多个行为表达式中选择一个去执行的行为，它对应于CCS的“+”算子例如：B1[]B2 表示选择B1或B2执行 a;B进程执行事件a之后，执行行为表达式Bg?x:t;B进程执行事件g?x:t之后，执行行为表达式B这里g?x:t为一个输入事件：从作用点g输入一个事件(数据)，将它放入类型为t的变量x中g!E;BE为数值表达式，进程执行事件g!E之后，执行行为表达式Bg!E为输出事件：将数值表达式E之值输出到作用点g。
2024/8/1060第四章 协议形式描述语言3.并行(parallelism) 并行算子说明进程并行执行多个行为表达式的行为，它对应于CCS的“|”算子LOTOS的并行算子有三种形式：4.串行( sequentiality ) 串行算子(用符号“>>”)说明进程执行一个行为表达式之后“使能”另一个行为表达式的行为，它是CCS顺序算子变种S1和S2(参见3.5)例如：B1>>B2如果B1成功结束使能B2 B1|[a1,a2,…,an]|B2B1和B2通过门径a1,a2,…,an并行B1||B2B1和B2通过它们的所有事件并行，这是前种形式的特例B1|||B2B1和B2独立并行这是CCS并行算子变种P1(参见3.5)，即B1和B2和之间无交互作用，它们和它们的环境(即父进程)有交互作用一般情况下，B1和B2相同 2024/8/1061第四章 协议形式描述语言5.5.作废作废(disruption)(disruption) 作废算子(用符号“|>”表示)说明进程在后个行为表达式的事件发生时停止并且作废前个行为表达式的行为，它类似于CCS的并行算子变种 (参见3.5)例如：B1|>B2执行B1时如果B2有事件发生，作废B1，执行B2。
6.6.隐藏隐藏(hide)(hide) 隐藏算子说明进程执行并行算子时隐藏内部协同事件的行为，它和CCS在利用扩展规则时限止协同事件的效果相同隐藏算子的形式为：Hide a in Ba为内部事件，B行为表达式7. 7. 看守看守(guard)(guard) 看守表达式说明一个行为表达式是否执行的条件，其形式为：[cond]->B cond为条件表达式或谓词，B为行为表达式cond为真，执行B 2024/8/1062第四章 协议形式描述语言8. 8. 终止终止(termination)(termination) 表示进程的终止有两个关键词：exit和stop exit成功结束； stop 停止进程活动9.9.内部事件内部事件 一个进程的内部事件用“I”表示，不确定性选择也用“I”表示例如：I;a;A []I;b;B 为了说明上述算子以及LOTOS语言的能力，我们举一个双缓冲通道的例子图4.5中进程two-slot-buffer[i,o]为两个单缓冲进程buffer[i,m]和buffer[m,o]并行组合而成，事件m为它们协同事件，系统定义如下： 2024/8/1063第四章 协议形式描述语言exam1:process two-slot-buffer[i,o]:= hide m in buffer[i,m]|[m]|buffer[m,o]where process buffer[input,output]:=input;output; buffer[input,output] endprocendproc 2024/8/1064第四章 协议形式描述语言上述LOTOS的进程定义可化作CCS表达形式。
将two-slot-buffer[i,o]记作P，buffer[i,m]记作A，buffer[m,o]记作B，那么双缓冲通道表示为：(1)式等效于hide语句(hide m等效于/m)，A和B的定义包括在process buffer[input,output]定义中利用CCS的扩展规则，(1)式变成： 2024/8/1065（4）式和（5）式就是外部观察者所见到的双缓冲通道的特征4）式和（5）式反过来用LOTOS描述成互相嵌套的进程(exam2)Exam2:Process two-slot-buffer[i,o]:= i;Q[i,o]endprocprocess Q[i,o]:= o;two-slot-buffer[i,o] []i;o;Q[i,o]Endproc我们已用CCS的代数变换法则证明了exam1和exam2是完全观察等价的第四章 协议形式描述语言 2024/8/1066第四章 协议形式描述语言4.3.3 抽象数据模型 与程序设计语言无关的数据模型叫做抽象数据模型，它描述一类具体的数据类型（由不同的程序设计语言实现的）的数学模型。
例如逻辑值“真”或“假”，程序设计语言可实现为{true,false}或{T,F}或{0,1}又例如，两数相加可表示为plus(a,b),或(a+b)，或(ab+)等不同形式抽象数据类型由数据目标或载体(data objects，或data carriers)集合和与之相关的操作定义以及操作性质说明形成数学上，一种抽象数据类型就是一种代数Exam3: Type nat-number is Sort nat Opns o:0->nat Succ: nat -> nat Endtype 这里，关键词type之后的nat-number为定义名(definition name),而sorts之后nat为类型名一个定义引用其他定义时用定义名，说明一个变量的类型时用类型名关键词opns的表达式说明可施加于该类型的操作，nat-number定义的是自然数类型nat，可施加于nat类型数据的操作是o和succo操作的含义是：0是自然数类型;succ操作的含义是：自然数类型的数的后继数（successor）也是自然数类型.上面的Opns操作只是声明了个操作，同时指明了各操作从定义域到值域的关系。
2024/8/1067第四章 协议形式描述语言一个定义引用另外一个定义的目的有两个：对一个已有的类型进行扩充，或将几个定义合成一个新定义Exam4：Type enrich-nat-number is nat-number withOpns _+_:nat,nat->natEqns forall x,y:natOfsort natx+0=x;x+succ(y)=succ(x+y);endtype这里，enrich-nat-number是nat-number的扩充，类型名仍然是nat，opns之后_+_定义了一个扩充的操作“+”，它是二元操作；自然数+自然数仍然是自然数关键词eqns说明自然数三个操作（0，succ,+）的性质关键词forall说明对于所有自然数x和y,关键词ofsort说明等式两边的数据类型 2024/8/1068第四章 协议形式描述语言为了进一步理解抽象数据类型的定义方法，举自然数队列为例Exam5：Type nat-number-queue is nat-number with Sorts queue Opns create:->queue add:nat,queue->queue first:queue->nat Eqns forall x,y;nat,z:queue Ofsort nat first(create)=0; first(add(x,create))=x; first(add(x,add(y,z)))=first(add(x,z))Endtype这里，nat-number-queue仍然是nat-number的扩充，但是，它定义了一个新的数据类型queue，queue有三种操作：创建队列（create），往队列里增加一个元素（add），从队列里取出第一个元素（first）。
每种队列操作的输入参数类型和输出参数类型都有明确定义，操作的性质由eqns后的等式说明，等式两边的数据类型为nat（由ofsort nat说明）变量的类型以及参数类型用“：”说明，例如x:nat, y:queue 2024/8/1069第四章 协议形式描述语言4.3.4 门径（gates）LOTOS引入了门径的概念门径就是协同事件发生点，或两个进程同步通讯点在ISO/OSI模型中，各层协议的服务访问点（如tsap nsap）就是一个门径门径的定义包括多个通讯变量的定义和输入、输出参数的定义，例如ISO传输层服务访问点（tsap）的门径定义如下：tsap: t_addr:t-addr-sort Tcep-id:tcep-id-sort …. …. …. TCONreq|TCONind|……这里，t-addr是门径内的通讯变量（类型为t-addr-sort），Tcep-id也是通讯变量（类型为tcep-id-sort），而TCONreq和TCONind等是输入输出参数 2024/8/1070第四章 协议形式描述语言 进程从门径变量输入用“？”操作符，向门径变量发送用“！”操作符。
输入输出操作必须采用g?x:t和和g!y的形式，g为门径名，x和y变量名，t为变量类型，LOTOS允许同一个门径内的多个变量的读写组合在一起，例如：tsap ?t-addr ?tcep-id!TCONreq;门径是两个进程的同步通讯点，同步必须遵守下述规则：（1）各个进程向门径输入或输出数据类型和顺序必须和门径定义的一致例如，当我们定义一个包含三个变量的门径a，下面的进程A和B向门径a输入和输出遵守了此项规则，a: x:integer y:string z:Boolean进程A a ?xa:integer ?ya:string !’true’进程B a !(3+5) !’this is a text’ ?’yes:Boolean; 2024/8/1071第四章 协议形式描述语言(2)两个进程通过同一个门径变量可进行“数值匹配（value matching）”、“数值传递（value passing）”和“数值生成（value generation）”三种交互作用。
下面给出进程A和B进行三种交互作用的情况数值生成时，两个进程变量x和y的值由门径定义决定 交互方式 进程A 进程B 同步条件 结果 数值匹配 g!E1 g!E2 数值相等（E1=E2） 同步 数值传递 g!E g?x:t E为t类型数值 x=E 数值生成 g?x:t g?y:u 类型一致(t=u) x=y=….. 2024/8/1072第四章 协议形式描述语言（3）一个进程对门径进行读时，可施行条件接收例如，a?xa:integer[xa<3]表示进程从门径a接收数据放入变量xa时，只有当xa<3时施行读操作。
4）多个进程可对同一门径进行输入、输出操作，但是，协同事件在哪一对进程之间发生是不确定的一个进程所利用的门径必须出现在进程定义的gate-list中（参见4.3.1）两个进程并行组合时要说明两个进程的协同事件（即门径），必要时隐藏这些门径例如在exam1中，行为表达式Hide m in buffer[i,m]|[m]|buffer[m,o]说明门径m为协同事件，并加以隐藏门径i 和o 不能隐藏 2024/8/1073第四章 协议形式描述语言4.3.5 AB协议的LOTOS描述 我们仍然以图4.4所示的AB协议系统为例给出一个LOTOS的应用示范，4.2.4用ESTELLE描述了AB协议全系统，这里我们只用LOTOS描述AB协议实体一个AB协议实体（AB—entity）由两个独立的进程（p—sender | eceiver ）并行组合（用“|||”算子）而成p—sender为发送进程，它调用q—sender,receiver为接收进程这三个进程是按3.5.4所给出AB协议的CCS描述定义的，S对应于p—sender，对应于q—sender,R对应于receiver 2024/8/1074第四章 协议形式描述语言数据类型seq—sort包含两个操作（int和inc）,x=init(x)和init(x)是等价的表达式，x=inc(x)和inc(x)是等价表达式。
数据类型Ndata—sort包含八种操作AB协议实体的内部过程几乎全部包含在这两个数据类型中time—sort 是一个特殊的数据类型，stop 使之停止工作，start使之启动Td—sort的两个操作（DATA和ACK）的结果就是报文类型标识号（DATA=1，ACK=2）Uprim—sort和Nprim—sort的定义类似门径Uap为user和AB—entity的接口，对应于ESTELLE描述中通道U—access—point(参见4.2.4)，那里的服务原语名和参数在这里变成三个门径变量门径Nap对应于ESTELLE描述中的N—access—point. 2024/8/1075第四章 协议形式描述语言程序示例 2024/8/1076第四章 协议形式描述语言 2024/8/1077第四章 协议形式描述语言 2024/8/1078第四章 协议形式描述语言 2024/8/1079第四章 协议形式描述语言4.3.6 LOTOS 的特点与应用方法 LOTOS的基本特点可归纳如下：1. LOTOS是基于进程代数CCS和多类代数（many—sorted algebra）的FDL，是一种适应协议工程，分布处理和并行处理技术的要求而产生的语言。
2. 进程通讯为同步通讯3. LOTOS不是面向协议实现的语言例如，它只是抽象数据类型定义中给出协议内部操作（报文的装配encode,顺序寄存器的操作inc等）的性质说明，而没有给出操作怎样实施的说明，这样，将LOTOS描述的协议转变成程序设计语言（c.pascal）代码需要做许多工作4.将LOTOS描述的协议很容易转换CCS或CSP模型，也比较容易转换TL，FSM或Petrinet模型5.总言之，LOTOS是一种面向协议验证技术的抽象级别较高FDLLOTOS以附录的形式给出比较完整的协议验证规则，这是别的FDL所不及的地方 2024/8/1080第四章 协议形式描述语言6. LOTOS的不足之处体现在几个方面：无异步通讯机制、无清晰的记录型数据结构的描述手段、无常量描述手段、可读性差等等用LOTOS描述协议的最好方法是：首先构造协议CCS模型，然后根据CCS模型进行LOTOS描述（4.3.5的AB协议的LOTOS描述是按3.5.4中AB协议CCS模型进行的）使用LOTOS应注意下述事项：（1）进程定义只给出进程的可观察行为的描述（例如，对门径的输入、输出，进程的调用等），进程的内部操作（例如，顺序计数器的加，报文的装配等）嵌入在进程调用的参数表和门径的输入，输出表中。
2）内部事件（例如，超时事件）用“I”表示3）CCS算子转换成LOTOS算子时，应根据情况将CCS的基本算子变成对应的变种算子4）门径的输入、输出操作是LOTOS描述的关键部分之一，请注意4.3.4所述的规则。
