4协议形式描述语言

《4协议形式描述语言》由会员分享，可在线阅读，更多相关《4协议形式描述语言（80页珍藏版）》请在金锄头文库上搜索。

1、2024/8/81第四章 协议形式描述语言4.14.1引言引言 协议可以用自然语言，程序设计语言，形式描述语言或专用语言描述。1 1、用自然语言描述协议特点：、用自然语言描述协议特点： 用自然语言描述的协议可读性好（正因为如此，ISO仍然用自然语言描述并颁布协议标准），但描述不准确，有二义性。 更重要的问题是，从自然语言描述的协议到协议的实现从自然语言描述的协议到协议的实现是一个复杂的、效率低的、一致性很差的，必须手工完成的是一个复杂的、效率低的、一致性很差的，必须手工完成的过程过程。所谓一致性差是指：对同一个协议，不同的人得出不同的实现版本。对自然语言描述的协议进行正确性验证，以及从中导出测

2、试序列的工作，存在同样的问题。2024/8/82第四章 协议形式描述语言2 2、程序设计语言描述协议特点、程序设计语言描述协议特点（1） 用经典的程序设计语言（例如Fortran，C，Pascal）描述协议便于协议的实现。（2）可读性差。（3）程序设计语言表述协议并发性、不确定性，以及其他协议性质和协议元素性质的能力较差。（4）由于程序设计语言描述的协议过多的描述了协议实现细节（有些和实现环境相关），因此它只能作为协议实现规范在小范围内使用，而不能作为协议标准在世界上颁布。（5）用程序设计语言描述的协议对协议验证和测试来说，协议的处理仍然是不方便的。2024/8/83第四章 协议形式描述语言

3、为了克服自然语言和程序设计语言的缺点，一些大计算机公司使用了专用协议描述语言。例如IBM公司的FAPL（Form and Protocol Language）就是一种专为提高IBM公司网络软件（SNA，system Network Architecture）的开发效率而设置的专用语言2024/8/84第四章 协议形式描述语言3 3、协议描述语言特点特点 使用形式化协议描述语言有许多优点。所谓所谓“形式化形式化”即即“模型化模型化”和和“抽象化抽象化”。一种形式描述语言必然基于一种或几种数学模型（如第三章介绍的FSM，Petri网 ，TL和CCS），这就为充分地表述协议的各种特性（并发性，不确定

4、性，时序性，递归性等）为协议验证、协议实现、协议测试和协议转换过程的系统化和自动化提供了良好的基础。 由于形式描述语言形式描述语言有很好的数学基础，用它描述的协议在语义上无二义性，同时由于它抽象于具体的协议实现环境，因此它可作为协议标准的描述语言。形式描述语言简称FDL（Formal Description Languages） 2024/8/85第四章 协议形式描述语言 FDL的基础是协议模型技术，从这个意义上说，本章是第三章的继续。然而，从协议模型技术到FDL还有许多工作要做。首先，作为一种语言，一种FDL在语法上和语义上必须是一个完整的体系。另外，一种FDL往往要对一种模型技术进行扩充，

5、或将几种模型技术拟合在一起，取长补短，使之具有很强的表达能力和应用能力。 八十年代以来，计算机科学家已提出许多种FDL，有些是专为协议工程而研制的，有的是为分布（并行）计算以及软件工程而提出的。对协议工程来说，由国际标准化组织（对协议工程来说，由国际标准化组织（ISOISO）颁布的颁布的ESTELLEESTELLE和和LOTOSLOTOS，以及国际电报电话咨询委员会，以及国际电报电话咨询委员会（CCITTCCITT）颁布的）颁布的SDLSDL是应用最广的是应用最广的FDLFDL。本章重点介绍ESTELLE和LOTOS。2024/8/86第四章 协议形式描述语言4.2 ESTELLE4.2 ES

6、TELLE概述概述 ESTELLEESTELLE是是19891989年年ISOISO公布的基于扩展的有限状态机公布的基于扩展的有限状态机（EFSM)EFSM)，是一种形式化、数学化、并且与具体实现相独立的，是一种形式化、数学化、并且与具体实现相独立的协议形式化描述语言。协议形式化描述语言。 ESTELLEESTELLE是是PASCALPASCAL语言的扩充语言的扩充2024/8/87第四章 协议形式描述语言 在在ESTELLEESTELLE中，中，（1 1）一一个个系系统统被被理理解解成成是是由由许许多多相相互互通通信信的的模模块块分分层层嵌嵌套套而而构成的构成的（2 2）模模块块之之间间通通

7、过过通通道道进进行行通通信信，即即通通道道将将一一个个模模块块的的输输出出与另一个模块的输入队列连接起来。与另一个模块的输入队列连接起来。（3 3）通道和模块之间的连接点称为交互点。）通道和模块之间的连接点称为交互点。（4 4）模模块块间间的的信信息息传传递递称称为为交交互互。每每个个模模块块相相当当于于一一个个有有限限状状态态自自动动机机，有有限限状状态态集集的的每每个个状状态态迁迁移移或或转转换换都都是是由由于于某某些些输输入入所所触触发发，状状态态迁迁移移过过程程中中可可能能会会产产生生输输出出。这这里里的的输输入入对对应应于于模模块块所所收收到到的的消消息息，而而输输出出则则对对应应与

8、与模模块块向向其其他他模模块所发送的消息。块所发送的消息。2024/8/88第四章 协议形式描述语言用ESTELLEESTELLE来描述协议规格时，其整体结构大致如下：来描述协议规格时，其整体结构大致如下：Specification Specification 规格名规格名全局参数（全局参数（Global parameterGlobal parameter）通道（通道（channelschannels）模块头（模块头（Module headersModule headers）模块体（模块体（module bodiesmodule bodies）规格主体（规格主体（Main bodiesMain

9、 bodies）EndEnd其中，模块体中最重要的是状态转换（迁移）其中，模块体中最重要的是状态转换（迁移）2024/8/89第四章 协议形式描述语言形式描述语言形式描述语言ESTELLEESTELLE有以下基本特点：有以下基本特点：1.1.基于扩展的有限状态机（基于扩展的有限状态机（EFSM),EFSM),专为描述协议而设计。专为描述协议而设计。2.2.ESTELLEESTELLE是是PascalPascal语言的扩充。用他描述的协议很容易转换成语言的扩充。用他描述的协议很容易转换成PascalPascal或或C C代码，因此它是一种面向协议实现的形式描述语言。代码，因此它是一种面向协议实现

10、的形式描述语言。3.3.模块实例可通过初始化语句动态产生。如果协议实现后模块实例对应模块实例可通过初始化语句动态产生。如果协议实现后模块实例对应一个进程或任务，那么网络进程或任务也是动态产生的。一个进程或任务，那么网络进程或任务也是动态产生的。4.4.模块之间的通信方式为异步方式。模块之间的通信方式为异步方式。5.5.ESTEILEESTEILE对并发、不确定性、超时、异步通信状态有较强的表到能力，对并发、不确定性、超时、异步通信状态有较强的表到能力，但对递归、共享通道、同步通信、协议性质的表现尚缺乏有力的手段。但对递归、共享通道、同步通信、协议性质的表现尚缺乏有力的手段。6.6.从从ESTE

11、ILEESTEILE描述中易于提取协议的描述中易于提取协议的FSMFSM模型或模型或PetriPetri网模型，但是不容易网模型，但是不容易提取提取TLTL和和CCSCCS模型。模型。2024/8/810第四章 协议形式描述语言 用ESTEILE来描述一个协议，最重要的工作就是构造协议的模块结构和通信机制，主要包括：系统中模块的层次构成，模块的类别、通道和交互点的定义、交互点队列的属性，以及模块和通道的连接问题。2024/8/811第四章 协议形式描述语言4.2.14.2.1模块概念模块概念1.1.模块（模块（modulesmodules） ESTELLE将一个系统看作是由许多相互通讯的模块分

12、层嵌套而构成的系统。每个父模块控制对其子模块的创建和销毁，系统的每一级可有许多个模块，每个模块可通过通道以异步方式和其他的模块通讯。2024/8/812第四章 协议形式描述语言 模块的定义由两部分组成：模块头和模块体组成。（1）模块头定义（module-head-definition） 每个模块头可对应一个或多个模块体。模块头定义包括两个重要部分： 外部交互点（external interaction points） 输出变量（exported variables）。2024/8/813第四章 协议形式描述语言（2）模块体定义（module-body-definition）。 模块体定义包括三

13、个主要部分： 说明部分（declaration -part）初始化部分（initialization-part）转换部分（transition-part）。 说明部分对模块所使用的通道（channels）、内部交互点（internal interaction points）、数据类型和变量、模块状态、调用的过程和函数进行说明。 初始化部分说明模块初起时各变量和模块状态的初始值。 转换部分是模块的关键部分，它按照EFSM定义模块状态转换过程。模块描述的非形式结构示意如下：2024/8/814第四章 协议形式描述语言Module 模块头A 模块类别 外部交互点说明 输出变量说明End;Body 模

14、块体-1 for 模块头-A 通道说明； 内部交互点说明； 数据类型和变量说明； 模块状态定义；过程和函数定义；模块初始化部分；状态转换部分；End；Body 模块体-2 for 模块头-A . . .End；2024/8/815第四章 协议形式描述语言2 2模块实例（模块实例（module instancesmodule instances） 协议运行时，用ESTELLE定义的一个模块体可同时生成一个或多个模块实例，模块实体并可动态产生和消失。同一个模块体的不同模块实例用模块变量（module variables）来标识。父模块实例初始化时负责子模块实例的生成。例如，Mod varMv-1：

15、 模块头-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/816第四章 协议形式描述语言在一个自动回叫系统例子中，共定义三个模块头，每个模块头对应一个模块体，其中模块MA的描述如下：Module MA systemprocess ip P:CA(PartyA)EndBody BA for MA.END2024/8/817第四章 协议形式描述语言ESTEILE所定义的一个模块体，在协议运行过程中可同时生成

16、一个或多个实例，模块实例可动态产生和撤销。不同模块实例用模块变量来标识（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

17、/8/818第四章 协议形式描述语言3.3.模块类别（模块类别（module classesmodule classes）按模块内容是否包含状态转换部分来说，模块分为：(1) 非活跃模块（inactive modules） 模块体内无状态转换的部分的模块叫做非活跃模块，初始化非活跃模块所产生的模块实例也是非活跃的。(2) 活跃模块（active modules）模块体包括状态转换部分的模块叫做活跃模块。(3) 特征模块（attributed modules） 当一个模块头定义有多个模块体定义与之关联时，如果至少有一个模块体内包含状态转换部分，此种模块叫做特征模块。 2024/8/819第四章

18、协议形式描述语言 按照模块工作方式进行分类，模块定义时，模块类别指明模块的工作方式。模块类别指明所定义的模块是n系统进程模块（system process）n系统活动模块（system activity）n进程模块（process）n活动模块（activity）。2024/8/820第四章 协议形式描述语言(1) 系统进程模块（System process） System process本身可以是特征模块，但它的父模块必须为非特征模块。它的子模块可是任何类别的模块，父进程必须是system process。它的工作方式：父模块优先于子模块，兄弟模块并行（并发）。假定一个system proce

19、ss有三个子模块。当system process有转换需要执行时，不管子模块是否有转换要执行，system process的转换优先执行。当system process无转换要执行时，如果三个子模块都有转换要执行，三个转换并行执行。2024/8/821第四章 协议形式描述语言(2) 系统活动模块（System activity） System activity本身可以是特征模块，它的父模块必须为非特征模块，并且必须是system process或system activity 。它的子模块必须是活动模块（activity）。系统活动模块的工作方式是：父模块优先于子模块，父模块优先于子模块，兄弟

20、模模块串行执行（选择是随意得）块串行执行（选择是随意得）。假定一个系统活动模块有三个子模块，当系统活动模块本身有转换要执行时，不管子模块是否有转换，它先执行自己的转换。当它自己无转换要执行时，如果三个子模块都有转换要执行，则它从三个activity中任选一个转换执行，并且这种选择是不确定的(nondeterminic )。2024/8/822第四章 协议形式描述语言（3 3）进程模块（）进程模块（processprocess） 它必须为特征模块，它的子模块不能为systemprocess和systemactivity，只能为process。它的工作方式和systemprocess相同。（4 4

21、） 活动模块（活动模块（activityactivity） 活动模块必须为特征模块，它的子模块只能为activity。它的工作方式和systemactivity相同。2024/8/823第四章 协议形式描述语言图4.1为一个协议运行时各模块实例的嵌套情况。虚线边框为非活跃模块。最高层模块为整个协议规范模块（SP）。2024/8/824第四章 协议形式描述语言(a) 假定 A 无转换要执行 A1 无转换要执行 A11有t11要执行 A12 有t12要执行 A2有t2要执行此时，模块实例A选择执行的转换可能为t11，t2或t12，t2。(b) 假定(a)中有转换要执行，那么A选泽t1，t2。(c)

22、 假定(a)中也无转换要执行，那么A选择t11或t12 。(d) 假定(a)中A有t转换要执行，那么A选择自己的t.2024/8/825第四章 协议形式描述语言4.4.模块嵌套规则模块嵌套规则( (module nesting rulesmodule nesting rules) )system process和system activity统称之为系统模块。模块嵌套的规则为:(1）系统模块的父模块必须为非特征模块(2)系统模块的子模块必须为特征模块。(3)同一级可有多个系统模块。(4)非系统模块的子模块不能为系统模块(5)system process的子模块可以是process或activi

23、ty；system activity的子模块必须为activity。(6)process的子模块必须为process，activity的子模块必须为activity。(7)非活跃模块头定义可以不指明“模块类别”。2024/8/826第四章 协议形式描述语言5 specification模块用ESTELIE描述一个协议时，描述规格总是从关键词specification开始。由specification开始的整个协议描述也是一个模块，它是最高层的模块。 Specification模块可以是非活跃模块，也可以是系统模块（systemprocess或systemactivity）.例如：Specifi

24、cation AC;说明了整个规格名称为AC，同时AC也是本规格中的最高层模块。2024/8/827第四章 协议形式描述语言4.2.2 模块诵讯模块诵讯1.通道（channels)通道定义包括通道名、通讯角色和各个通讯角色向通道施加交互信息三部分。一般情况下，一个通道只有两个通讯角色（一端一个)。每个角色向通道发出什么交互信息(即报文名、服务源语名等)，以及各个交互所附带的参数都必须在通道定义中给出。例如，ISO传输层的服务访向点（TSAP）可定义为一个通道：channel tsap type（user，provider）； by user： t一connection req（source：a

25、ddress 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/828第四章 协议形式描述语言例2：如果通道为buy,其通信角色有Customer和Vendor。Customer向通道施加的交互信息为coin，而ven

26、dor向通道施加的交互信息为trinketChannel Buy（customer，vendor）； by customer； coin； by vendor； trinket；2024/8/829第四章 协议形式描述语言在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；Chann

27、el CB（PartyB，Agent） by PartyB：answerb；available；busyb； by Agent：checkb； ringb；stopringb；2024/8/830第四章 协议形式描述语言2.交互点（interaction points） 一个通道定义二个通讯角色，这不意味着只能有两个模块使用一个通道。多个模块可扮演同一个通讯角色使用同一个通道。一个模块必须定义一个交互点之后才能将它自己与一个通道联系起来。如果一个模块要使用父模块定义的通道，它必须在模块头定义中给出交互点定义，这种交互点叫做外部交互点。如果一个模块要使用它自己定义的通道，那么它必须在模块定义中给

28、出交互点定义、这种交互点叫做内部交互点。交互点简称ip。2024/8/831第四章 协议形式描述语言3.交互点的约束（ip binding） 一个独立的交互点无通讯能力，只有当两个以上的交互点约束(bind)在一起时，一个交互点的输入事件才能作为输出事件传递到另一个交互点。connect语句和attach语句将交互点约束在一起，disconnect和detach解除ip的约束。(1)connect格式：connect ip 1 to ip一2ip 1 to ip一2必须是定义在同一个通道两端的交互点(通讯角色相反)。发出connect语句的模块可以将两个子模块的外部ip约束在一起;可以将它自己

29、的两个内部ip约束在一起;可以将它自己的一个内部ip和一个子模块的外部ip约束在一起。2024/8/832第四章 协议形式描述语言(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格式：

30、detach eip或child一eip解除eip或child一eip中任何一个交互点的约束就自动解除另一个ip的约束口。 2024/8/833第四章 协议形式描述语言4联接端点(connection endpoints) 多个ip利用多条conncet语句和attach语句串行约束在一起可形成一条联接(connection) ,联接两端的ip叫做联接端点。联接的主要特征是：进入一个联接端点的输入将自动传递到另一端的联接端点的队列中，中间ip的队列隐藏起来。 为了说明通道，交互点约束的概念，举例如下。图4.2是一个由四个模块W，X，Y，Z嵌套而成的系统（W，X，Y，Z为模块变量名),a为W的内

31、部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/834第四章 协议形式描述语言在X的模块中头中ip b：CH(provider) individual queue；在Y的模块中头中ip c：CH(provider) individual queue；在X的模块中头中ip d：CH(provider) individual queue；2024/8/835第四章 协议形

32、式描述语言在各自的模块中发出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/836第四章 协议形式描述语言5ip队列（输入队列） 定义ip时必须指明ip的队列性质：common queue或individual queue。多个模块使用同一个通道时，它们可使用自己的单独队列，也可

33、以共享队列。如果定义在通道同一端的ip队列为common queue，那么定义这些ip的模块使用共享队列。2024/8/837第四章 协议形式描述语言图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/8386. 输入和输出 when 语句从ip读一个事件，而output语句往

34、ip输入一个事件。格式为：when ip.m(arquments)output ip.m(arquments)这里m(arquments)必须是channel定义中指明交互事件.when语句从ip的队列(FIFO)读出事件,该事件是联接的另一端output语句所输入的事件.由于FIFO队列的原因,输出和输入不是同时发生的,因此模块通讯是异步的 第四章 协议形式描述语言2024/8/839第四章 协议形式描述语言4.2.3 4.2.3 状态转换的描述状态转换的描述 状态转换部分是模块中最重要的部分.模块状态转换的描述基于扩展有限状态机模型(EESM),其描述直观明了：1 1、描述语句、描述语句

35、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/840第四章 协议形式描述语言例如:trans when ip.m from A any x:13 do

36、 provided E(x) to C begin S1;S2; end;这里any语句把X=1,X=2和X=3时三个转换合成一个简练的转换.如果不用any语句,上述描述必须重复三次,每次转换中的provided语句不同,其它相同. S1,S2,.为转换所执行的事件或过程(包括output语句).2024/8/841第四章 协议形式描述语言2 2 转换的选择和执行转换的选择和执行转换可分成三种状态:(1) Enabled: 如果when,from和provided语句得到满足,该转换变成enabled状态.(2) Fireable:如果delay和priority语句得到满足,那么一个enab

37、led转换变成fireable状态.如果无delay和priority语句.那么enabled状态和fireable状态相同.(3) Offered:对于某个模块实例来说,它和它的子模块中可能存在多个fireable转换,模块将选择一个或多个转换交付执行,被交付执行的转换叫做offered转换.模块怎样选择fireable转换取决于模块本身类别和子模块的结构.选择按4.2.1所述的原则先父后子,process并行,activity串行. 被交付的转换怎样执行在协议实现中解决,ESTELLE只认为交付的转换就一定执行.2024/8/842第四章 协议形式描述语言4.2.4 AB4.2.4 AB协

38、议的协议的ESTELLEESTELLE描述描述 本节所描述的整体AB协议系统(类别为system process)如图4.4所示.系统中存在多个AB协议模块实例(类别为process),每个AB协议对应一个用户模块实例(类别为process).所有AB协议模块实例共享一个网络模块实例(类别process).用户模块实例和网络模块实例为外部模块(external),它们由其它ESTELLE文本描述.2024/8/843第四章 协议形式描述语言图4.4 AB协议系统2024/8/844第四章 协议形式描述语言 系统定义两个通道:Uaccesspoint和Naccesspoint.前者为AB协议模块

39、与用户模块的接口,后者为AB协议模块和网络模块的接口。接口(通道之间)的通讯原语示于图4.4中. AB协议模块既是sender也是receiver.为了缩小状态转换部分的篇幅,（1）AB协议模块作为sender只定义了两个状态:ESTAB(初始状态),ACKWAIT(等待认可报文),（2）作为receiver没有定义状态.（3）多个用户实例和多个AB协议模块实例用数字标识.2024/8/845第四章 协议形式描述语言 Sender用Source_id标识它自己，并由Send-request和data-request的参数destination决定。如果有n个用户，那么通道N-access-po

40、int两端各定义n个ip,并用n个connect语句约束在一起。2024/8/846第四章 协议形式描述语言示例程序：2024/8/8472024/8/8482024/8/8492024/8/8502024/8/8512024/8/852第四章 协议形式描述语言4.2.5 ESTELLE4.2.5 ESTELLE的特点与应用方法的特点与应用方法 ESTELLE的基本特点可归纳如下：(1) 基于扩充有限状态机(EFSM)的FDL，专为协议描述而设计。模块实例可通过初始化语句动态产生。如果协议实现后模块实例对应于一个进程或任务，那么网络进程或任务也是动态产生的。(2) 模块通讯为异步通讯。(3)

41、ESTELLE是pascal语言的扩充，用ESTELLE描述的协议容易转换成pascal或C代码。因此，它是一种面向协议实砚的FDL。(4) ESTELLE对并发、不确定性、超时、异步通讯状态转换有较强的表达能力，但对递归、共享通道（广播通道）、同步通讯、协议性质（如不变性等）的表示缺少有力的手段。2024/8/853第四章 协议形式描述语言用ESTELLE描述的协议易于提取FSM模型和Petri网模型，但不容易提取转变成TL和CCS模型。 用ESTELLE描述一个协议，最重要的工作(也是第一步工作)就是构造协议的模块结构和通讯机制。系统由多少层模块构成？每个模块应该是什么类别(类别决定了工作

42、方式)？定义多少通道和交互点？交互点队列属于哪种？它们约束成什么样联接？这些问题必须作出周密安排；否则将影响协议实现后执行效率，例如应该定义为system process类别的模块定义system activity之后，并行性就会失去。论文3给出了ISO传输层协议的ESTELLE描述。是一篇很好的参考资料。2024/8/854第四章 协议形式描述语言4.3 LOTOS4.3 LOTOS概述概述 LOTOS 的基本思想是： 外部可观察到的系统行为由一系列的交互作用组成， 通过对这些交互作用的时间关系进行定义， 从而描述整个系统。在定义这些交互作用的时间关系时，不是采用时序逻辑的方式，而是基于进程

43、代数的方法。 LOTOS 规 格（ specification ）主要包括数据类型的定义和进程的定义两个部分，其整体结构大致如下 ： SPECIFICATION 规格名 全局类型定义 进程定义 ENDSPEC LOTOS 具有如下基本特点。 1.LOTOS 是基于进程代数 CCS 和多类代数 (Many-Sorted Algebra) 的 FDL ，是一种为适应协议工程、分布处理和并行处理技术的要求而产生的语言。2.进程通信为同步通信。3.LOTOS 不是面向协议实现的语言。例如，它只是在抽象数据类型定义中给出协议内部操作的性质说明，而没有给出操作怎样实施的说明。从而，在将 LOTOS 描述的

44、协议转变成程序设计语言（如 C,Pascal ） 代码时需要做许多工作。4.用 LOTOS 描述的协议很容易转换成 CCS 或 CSP 模型，也比较容易转换成 TL, FSM 或 Petri 网模型。5.LOTOS 的不足之处体现在以下几个方面。无异步通信机制，无清晰的记录型数据结构的描述手段，无常量描述手段，可读性差等。 2024/8/855第四章 协议形式描述语言4.3.1 4.3.1 进程定义进程定义 LOTOS将一个系统看做多个相互作用的子进程组成的进程，每个子进程又是由多个子进程构成。进程定义为：process process-id gate-list (parameter-list

45、):noexit:=endprocess这里process和endprocess为关键词，表示进程定义的开始和结束。process-id为进程名，gate-list为门径表(参见4.3.4) ; parameter-list为参数表(类似子程序设计语言的过程定义中的哑元哑元); behaviour-expression为描述进程行为的表达式(参见4.3.2); noexit为关键词，表示该进程为非终止进程; 关键词exit说明一个终止进程。2024/8/856第四章 协议形式描述语言2024/8/857第四章 协议形式描述语言图 3-8 具有门径 ag 的进程 P 2024/8/858第四章

46、协议形式描述语言进程 Max3 的空间表示 LOTOS 进程中定义的典型结构 2024/8/859第四章 协议形式描述语言4.3.2 4.3.2 行为算子行为算子 多个协议事件和行为表达式可用行为算子组合成新的行为表达式。1.行动前辍(action-prefix) 行动前缀(用符号”;”)说明进程顺序执行事件的行为，它对应于CCS的“.”算子。例如：2.选择(choice) 选择(用符号”)说明进程从多个行为表达式中选择一个去执行的行为，它对应于CCS的“+”算子。例如：B1B2 表示选择B1或B2执行 a;B进程执行事件a之后，执行行为表达式B。g?x:t;B进程执行事件g?x:t之后，执行

47、行为表达式B。这里g?x:t为一个输入事件：从作用点g输入一个事件(数据)，将它放入类型为t的变量x中。g!E;BE为数值表达式，进程执行事件g!E之后，执行行为表达式B。g!E为输出事件：将数值表达式E之值输出到作用点g。2024/8/860第四章 协议形式描述语言3.并行(parallelism) 并行算子说明进程并行执行多个行为表达式的行为，它对应于CCS的“|”算子。LOTOS的并行算子有三种形式：4.串行( sequentiality ) 串行算子(用符号“”)说明进程执行一个行为表达式之后“使能”另一个行为表达式的行为，它是CCS顺序算子变种S1和S2(参见3.5)。例如：B1B2

48、如果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/861第四章 协议形式描述语言5.5.作废作废(disruption)(disruption) 作废算子(用符号“|”表示)说明进程在后个行为表达式的事件发生时停止并且作废前个行为表达式的行为，它类似于CCS的并行算子变种 (参见3.5)。例如：B1|B2

49、执行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/862第四章 协议形式描述语言8. 8. 终止终止(termination)(termination) 表示进程的终止有两个关键词：exi

50、t和stop exit成功结束； stop 停止进程活动9.9.内部事件内部事件 一个进程的内部事件用“I”表示，不确定性选择也用“I”表示。例如：I;a;A I;b;B 为了说明上述算子以及LOTOS语言的能力，我们举一个双缓冲通道的例子。图4.5中进程two-slot-bufferi,o为两个单缓冲进程bufferi,m和bufferm,o并行组合而成，事件m为它们协同事件，系统定义如下：2024/8/863第四章 协议形式描述语言exam1:process two-slot-bufferi,o:= hide m in bufferi,m|m|bufferm,owhere process

51、bufferinput,output:=input;output; bufferinput,output endprocendproc2024/8/864第四章 协议形式描述语言上述LOTOS的进程定义可化作CCS表达形式。将two-slot-bufferi,o记作P，bufferi,m记作A，bufferm,o记作B，那么双缓冲通道表示为：(1)式等效于hide语句(hide m等效于/m)，A和B的定义包括在process bufferinput,output定义中。利用CCS的扩展规则，(1)式变成：2024/8/865（4）式和（5）式就是外部观察者所见到的双缓冲通道的特征。（4）式和

52、（5）式反过来用LOTOS描述成互相嵌套的进程(exam2)。Exam2:Process two-slot-bufferi,o:= i;Qi,oendprocprocess Qi,o:= o;two-slot-bufferi,o i;o;Qi,oEndproc我们已用CCS的代数变换法则证明了exam1和exam2是完全观察等价的。第四章 协议形式描述语言2024/8/866第四章 协议形式描述语言4.3.3 抽象数据模型 与程序设计语言无关的数据模型叫做抽象数据模型，它描述一类具体的数据类型（由不同的程序设计语言实现的）的数学模型。例如逻辑值“真”或“假”，程序设计语言可实现为true,fa

53、lse或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为类型名。一个定义引用其他定义时用定义名，说明一个变量的类型时用类型

54、名。关键词opns的表达式说明可施加于该类型的操作，nat-number定义的是自然数类型nat，可施加于nat类型数据的操作是o和succ。o操作的含义是：0是自然数类型;succ操作的含义是：自然数类型的数的后继数（successor）也是自然数类型.上面的Opns操作只是声明了个操作，同时指明了各操作从定义域到值域的关系。2024/8/867第四章 协议形式描述语言一个定义引用另外一个定义的目的有两个：对一个已有的类型进行扩充，或将几个定义合成一个新定义。Exam4：Type enrich-nat-number is nat-number withOpns _+_:nat,nat-nat

55、Eqns 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/868第四章 协议形式描述语言为了进一步理解抽象数据类型的定义方法，举自然数队列为例。Exam5：Type nat-number-queu

56、e 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），往队列里增加一个元素

57、（add），从队列里取出第一个元素（first）。每种队列操作的输入参数类型和输出参数类型都有明确定义，操作的性质由eqns后的等式说明，等式两边的数据类型为nat（由ofsort nat说明）。变量的类型以及参数类型用“：”说明，例如x:nat, y:queue。2024/8/869第四章 协议形式描述语言4.3.4 门径（gates）LOTOS引入了门径的概念。门径就是协同事件发生点，或两个进程同步通讯点。在ISO/OSI模型中，各层协议的服务访问点（如tsap nsap）就是一个门径。门径的定义包括多个通讯变量的定义和输入、输出参数的定义，例如ISO传输层服务访问点（tsap）的门径定义

58、如下：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/870第四章 协议形式描述语言 进程从门径变量输入用“？”操作符，向门径变量发送用“！”操作符。输入输出操作必须采用g?x:t和和g!y的形式，g为门径名，x和y变量名，t为变量类型，LOTOS允许同一个门径内的多个变量的读写组合在一起，例如：tsap ?t-a

59、ddr ?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/871第四章 协议形式描述语言(2)两个进程通过同一个门径变量可进行“数值匹配（value matching）”、“数值传

60、递（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/872第四章 协议形式描述语言（3）一个进程对门径进行读时，可施行条件接收。例如，a?xa:integerxa3表示进程从门径a接收数据放入变量xa时，只有当xa3时施行读

61、操作。（4）多个进程可对同一门径进行输入、输出操作，但是，协同事件在哪一对进程之间发生是不确定的。一个进程所利用的门径必须出现在进程定义的gate-list中（参见4.3.1）。两个进程并行组合时要说明两个进程的协同事件（即门径），必要时隐藏这些门径。例如在exam1中，行为表达式Hide m in bufferi,m|m|bufferm,o说明门径m为协同事件，并加以隐藏。门径i 和o 不能隐藏。2024/8/873第四章 协议形式描述语言4.3.5 AB协议的LOTOS描述 我们仍然以图4.4所示的AB协议系统为例给出一个LOTOS的应用示范，4.2.4用ESTELLE描述了AB协议全系统

62、，这里我们只用LOTOS描述AB协议实体。一个AB协议实体（ABentity）由两个独立的进程（psender | eceiver ）并行组合（用“|”算子）而成。psender为发送进程，它调用qsender,receiver为接收进程。这三个进程是按3.5.4所给出AB协议的CCS描述定义的，S对应于psender，对应于qsender,R对应于receiver。2024/8/874第四章 协议形式描述语言数据类型seqsort包含两个操作（int和inc）,x=init(x)和init(x)是等价的表达式，x=inc(x)和inc(x)是等价表达式。数据类型Ndatasort包含八种操作

63、。AB协议实体的内部过程几乎全部包含在这两个数据类型中timesort 是一个特殊的数据类型，stop 使之停止工作，start使之启动。Tdsort的两个操作（DATA和ACK）的结果就是报文类型标识号（DATA=1，ACK=2）。Uprimsort和Nprimsort的定义类似。门径Uap为user和ABentity的接口，对应于ESTELLE描述中通道Uaccesspoint(参见4.2.4)，那里的服务原语名和参数在这里变成三个门径变量。门径Nap对应于ESTELLE描述中的Naccesspoint.2024/8/875第四章 协议形式描述语言程序示例2024/8/876第四章 协议形

64、式描述语言2024/8/877第四章 协议形式描述语言2024/8/878第四章 协议形式描述语言2024/8/879第四章 协议形式描述语言4.3.6 LOTOS 的特点与应用方法 LOTOS的基本特点可归纳如下：1. LOTOS是基于进程代数CCS和多类代数（manysorted algebra）的FDL，是一种适应协议工程，分布处理和并行处理技术的要求而产生的语言。2. 进程通讯为同步通讯3. LOTOS不是面向协议实现的语言。例如，它只是抽象数据类型定义中给出协议内部操作（报文的装配encode,顺序寄存器的操作inc等）的性质说明，而没有给出操作怎样实施的说明，这样，将LOTOS描述

65、的协议转变成程序设计语言（c.pascal）代码需要做许多工作。4.将LOTOS描述的协议很容易转换CCS或CSP模型，也比较容易转换TL，FSM或Petrinet模型。5.总言之，LOTOS是一种面向协议验证技术的抽象级别较高FDL。LOTOS以附录的形式给出比较完整的协议验证规则，这是别的FDL所不及的地方。2024/8/880第四章 协议形式描述语言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所述的规则。