协议形式描述语言.ppt

2019/5/31,1,第四章 协议形式描述语言,4.1引言 协议可以用自然语言，程序设计语言，形式描述语言或专用语言描述。 1、用自然语言描述协议特点： 用自然语言描述的协议可读性好（正因为如此，ISO仍然用自然语言描述并颁布协议标准），但描述不准确，有二义性。 更重要的问题是，从自然语言描述的协议到协议的实现是一个复杂的、效率低的、一致性很差的，必须手工完成的过程。所谓一致性差是指：对同一个协议，不同的人得出不同的实现版本。对自然语言描述的协议进行正确性验证，以及从中导出测试序列的工作，存在同样的问题。,2019/5/31,2,第四章 协议形式描述语言,2、程序设计语言描述协议特点 （1） 用经典的程序设计语言（例如Fortran，C，Pascal）描述协议便于协议的实现。 （2）可读性差。 （3）程序设计语言表述协议并发性、不确定性，以及其他协议性质和协议元素性质的能力较差。 （4）由于程序设计语言描述的协议过多的描述了协议实现细节（有些和实现环境相关），因此它只能作为协议实现规范在小范围内使用，而不能作为协议标准在世界上颁布。 （5）用程序设计语言描述的协议对协议验证和测试来说，协议的处理仍然是不方便的。,2019/5/31,3,第四章 协议形式描述语言,为了克服自然语言和程序设计语言的缺点，一些大计算机公司使用了专用协议描述语言。例如IBM公司的FAPL（Form and Protocol Language）就是一种专为提高IBM公司网络软件（SNA，system Network Architecture）的开发效率而设置的专用语言,2019/5/31,4,第四章 协议形式描述语言,3、协议描述语言特点 使用形式化协议描述语言有许多优点。所谓“形式化”即“模型化”和“抽象化”。一种形式描述语言必然基于一种或几种数学模型（如第三章介绍的FSM，Petri网 ，TL和CCS），这就为充分地表述协议的各种特性（并发性，不确定性，时序性，递归性等）为协议验证、协议实现、协议测试和协议转换过程的系统化和自动化提供了良好的基础。 由于形式描述语言有很好的数学基础，用它描述的协议在语义上无二义性，同时由于它抽象于具体的协议实现环境，因此它可作为协议标准的描述语言。形式描述语言简称FDL（Formal Description Languages）,2019/5/31,5,第四章 协议形式描述语言,FDL的基础是协议模型技术，从这个意义上说，本章是第三章的继续。然而，从协议模型技术到FDL还有许多工作要做。首先，作为一种语言，一种FDL在语法上和语义上必须是一个完整的体系。另外，一种FDL往往要对一种模型技术进行扩充，或将几种模型技术拟合在一起，取长补短，使之具有很强的表达能力和应用能力。 八十年代以来，计算机科学家已提出许多种FDL，有些是专为协议工程而研制的，有的是为分布（并行）计算以及软件工程而提出的。对协议工程来说，由国际标准化组织（ISO）颁布的ESTELLE和LOTOS，以及国际电报电话咨询委员会（CCITT）颁布的SDL是应用最广的FDL。本章重点介绍ESTELLE和LOTOS。,2019/5/31,6,第四章 协议形式描述语言,4.2 ESTELLE概述 ESTELLE是1989年ISO公布的基于扩展的有限状态机（EFSM)，是一种形式化、数学化、并且与具体实现相独立的协议形式化描述语言。 ESTELLE是PASCAL语言的扩充,2019/5/31,7,第四章 协议形式描述语言,在ESTELLE中， （1）一个系统被理解成是由许多相互通信的模块分层嵌套而构成的 （2）模块之间通过通道进行通信，即通道将一个模块的输出与另一个模块的输入队列连接起来。 （3）通道和模块之间的连接点称为交互点。 （4）模块间的信息传递称为交互。每个模块相当于一个有限状态自动机，有限状态集的每个状态迁移或转换都是由于某些输入所触发，状态迁移过程中可能会产生输出。这里的输入对应于模块所收到的消息，而输出则对应与模块向其他模块所发送的消息。,2019/5/31,8,第四章 协议形式描述语言,用ESTELLE来描述协议规格时，其整体结构大致如下： Specification 规格名 全局参数（Global parameter） 通道（channels） 模块头（Module headers） 模块体（module bodies） 规格主体（Main bodies） End 其中，模块体中最重要的是状态转换（迁移）,2019/5/31,9,第四章 协议形式描述语言,形式描述语言ESTELLE有以下基本特点： 基于扩展的有限状态机（EFSM),专为描述协议而设计。 ESTELLE是Pascal语言的扩充。用他描述的协议很容易转换成Pascal或C代码，因此它是一种面向协议实现的形式描述语言。 模块实例可通过初始化语句动态产生。如果协议实现后模块实例对应一个进程或任务，那么网络进程或任务也是动态产生的。 模块之间的通信方式为异步方式。 ESTEILE对并发、不确定性、超时、异步通信状态有较强的表到能力，但对递归、共享通道、同步通信、协议性质的表现尚缺乏有力的手段。 从ESTEILE描述中易于提取协议的FSM模型或Petri网模型，但是不容易提取TL和CCS模型。,2019/5/31,10,第四章 协议形式描述语言,用ESTEILE来描述一个协议，最重要的工作就是构造协议的模块结构和通信机制，主要包括：系统中模块的层次构成，模块的类别、通道和交互点的定义、交互点队列的属性，以及模块和通道的连接问题。,2019/5/31,11,第四章 协议形式描述语言,4.2.1模块概念 1.模块（modules） ESTELLE将一个系统看作是由许多相互通讯的模块分层嵌套而构成的系统。每个父模块控制对其子模块的创建和销毁，系统的每一级可有许多个模块，每个模块可通过通道以异步方式和其他的模块通讯。,2019/5/31,12,第四章 协议形式描述语言,模块的定义由两部分组成：模块头和模块体组成。 （1）模块头定义（module-head-definition） 每个模块头可对应一个或多个模块体。 模块头定义包括两个重要部分： 外部交互点（external interaction points） 输出变量（exported variables）。,2019/5/31,13,第四章 协议形式描述语言,（2）模块体定义（module-body-definition）。 模块体定义包括三个主要部分： 说明部分（declaration -part） 初始化部分（initialization-part） 转换部分（transition-part）。 说明部分对模块所使用的通道（channels）、内部交互点（internal interaction points）、数据类型和变量、模块状态、调用的过程和函数进行说明。 初始化部分说明模块初起时各变量和模块状态的初始值。 转换部分是模块的关键部分，它按照EFSM定义模块状态转换过程。模块描述的非形式结构示意如下：,2019/5/31,14,第四章 协议形式描述语言,Module 模块头A 模块类别 外部交互点说明 输出变量说明 End; Body 模块体-1 for 模块头-A 通道说明； 内部交互点说明； 数据类型和变量说明； 模块状态定义； 过程和函数定义； 模块初始化部分； 状态转换部分； End；,Body 模块体-2 for 模块头-A . . . End；,2019/5/31,15,第四章 协议形式描述语言,2模块实例（module instances） 协议运行时，用ESTELLE定义的一个模块体可同时生成一个或多个模块实例，模块实体并可动态产生和消失。同一个模块体的不同模块实例用模块变量（module variables）来标识。父模块实例初始化时负责子模块实例的生成。例如， Mod var Mv-1： 模块头-A； Mv-2： 模块头-A； Initialize Begin Init mv-1 with 模块体-1； Init mv-2 with 模块体-2； End； 这里用变量mv-1表示模块体-1的实例，mv-2标识模块体-2的实例。,2019/5/31,16,第四章 协议形式描述语言,在一个自动回叫系统例子中，共定义三个模块头，每个模块头对应一个模块体，其中模块MA的描述如下： Module MA systemprocess ip P:CA(PartyA) End Body BA for MA . . . END,2019/5/31,17,第四章 协议形式描述语言,ESTEILE所定义的一个模块体，在协议运行过程中可同时生成一个或多个实例，模块实例可动态产生和撤销。不同模块实例用模块变量来标识（module variables）,在ESTEILE中模块实例的生成部分包括在规格主体部分（main bodyes）中。例如在自动回叫系统的例子最后。 Modvar partyA:MA partyB:MB Agent:MG Initilize begin init partyA with MA; init partyB with MB; init Agent with MG; end,这里，首先说明了三个模块变量partyA, partyB, Agent,它们分别对应模块MA, MB, MG,然后初始化部分生成实例。,2019/5/31,18,第四章 协议形式描述语言,3.模块类别（module classes） 按模块内容是否包含状态转换部分来说，模块分为： (1) 非活跃模块（inactive modules） 模块体内无状态转换的部分的模块叫做非活跃模块，初始化非活跃模块所产生的模块实例也是非活跃的。 (2) 活跃模块（active modules） 模块体包括状态转换部分的模块叫做活跃模块。 (3) 特征模块（attributed modules） 当一个模块头定义有多个模块体定义与之关联时，如果至少有一个模块体内包含状态转换部分，此种模块叫做特征模块。,2019/5/31,19,第四章 协议形式描述语言,按照模块工作方式进行分类，模块定义时，模块类别指明模块的工作方式。模块类别指明所定义的模块是 系统进程模块（system process） 系统活动模块（system activity） 进程模块（process） 活动模块（activity）。,2019/5/31,20,第四章 协议形式描述语言,(1) 系统进程模块（System process） System process本身可以是特征模块，但它的父模块必须为非特征模块。它的子模块可是任何类别的模块，父进程必须是system process。它的工作方式：父模块优先于子模块，兄弟模块并行（并发）。假定一个system process有三个子模块。当system process有转换需要执行时，不管子模块是否有转换要执行，system process的转换优先执行。当system process无转换要执行时，如果三个子模块都有转换要执行，三个转换并行执行。,2019/5/31,21,第四章 协议形式描述语言,(2) 系统活动模块（System activity） System activity本身可以是特征模块，它的父模块必须为非特征模块，并且必须是system process或system activity 。它的子模块必须是活动模块（activity）。系统活动模块的工作方式是：父模块优先于子模块，兄弟模块串行执行（选择是随意得）。假定一个系统活动模块有三个子模块，当系统活动模块本身有转换要执行时，不管子模块是否有转换，它先执行自己的转换。当它自己无转换要执行时，如果三个子模块都有转换要执行，则它从三个activity中任选一个转换执行，并且这种选择是不确定的(nondeterminic )。,2019/5/31,22,第四章 协议形式描述语言,（3）进程模块（process） 它必须为特征模块，它的子模块不能为systemprocess和systemactivity，只能为 process。它的工作方式和systemprocess相同。 （4） 活动模块（activity） 活动模块必须为特征模块，它的子模块只能为activity。它的工作方式和systemactivity相同。,2019/5/31,23,第四章 协议形式描述语言,图4.1为一个协议运行时各模块实例的嵌套情况。虚线边框为非活跃模块。最高层模块为整个协议规范模块（SP）。,2019/5/31,24,第四章 协议形式描述语言,(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.,2019/5/31,25,第四章 协议形式描述语言,4.模块嵌套规则(module nesting rules) system process和system activity统称之为系统模块。模块嵌套的规则为: (1）系统模块的父模块必须为非特征模块 (2)系统模块的子模块必须为特征模块。 (3)同一级可有多个系统模块。 (4)非系统模块的子模块不能为系统模块 (5)system process的子模块可以是process或activity；system activity的子模块必须为activity。 (6)process的子模块必须为process，activity的子模块必须为activity。 (7)非活跃模块头定义可以不指明“模块类别”。,2019/5/31,26,第四章 协议形式描述语言,5 specification模块 用ESTELIE描述一个协议时，描述规格总是从关键词specification开始。由specification开始的整个协议描述也是一个模块，它是最高层的模块。 Specification模块可以是非活跃模块，也可以是系统模块（systemprocess或systemactivity）.例如：Specification AC; 说明了整个规格名称为AC，同时AC也是本规格中的最高层模块。,2019/5/31,27,第四章 协议形式描述语言,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即为传渝层协议实体，它们向通道施加的交互信息都是传输层协议的服务源语。,2019/5/31,28,第四章 协议形式描述语言,例2：如果通道为buy,其通信角色有Customer和Vendor。Customer向通道施加的交互信息为coin，而vendor向通道施加的交互信息为trinket Channel Buy（customer，vendor）； by customer； coin； by vendor； trinket；,2019/5/31,29,第四章 协议形式描述语言,在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；,2019/5/31,30,第四章 协议形式描述语言,2.交互点（interaction points） 一个通道定义二个通讯角色，这不意味着只能有两个模块使用一个通道。多个模块可扮演同一个通讯角色使用同一个通道。一个模块必须定义一个交互点之后才能将它自己与一个通道联系起来。如果一个模块要使用父模块定义的通道，它必须在模块头定义中给出交互点定义，这种交互点叫做外部交互点。如果一个模块要使用它自己定义的通道，那么它必须在模块定义中给出交互点定义、这种交互点叫做内部交互点。交互点简称ip。,2019/5/31,31,第四章 协议形式描述语言,3.交互点的约束（ip binding） 一个独立的交互点无通讯能力，只有当两个以上的交互点约束(bind)在一起时，一个交互点的输入事件才能作为输出事件传递到另一个交互点。connect语句和attach语句将交互点约束在一起，disconnect和detach解除ip的约束。 (1)connect 格式：connect ip 1 to ip一2 ip 1 to ip一2必须是定义在同一个通道两端的交互点(通讯角色相反)。发出connect语句的模块可以将两个子模块的外部ip约束在一起;可以将它自己的两个内部ip约束在一起;可以将它自己的一个内部ip和一个子模块的外部ip约束在一起。,2019/5/31,32,第四章 协议形式描述语言,(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的约束口。,2019/5/31,33,第四章 协议形式描述语言,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；,2019/5/31,34,第四章 协议形式描述语言,在X的模块中头中 ip b：CH(provider) individual queue； 在Y的模块中头中 ip c：CH(provider) individual queue； 在X的模块中头中 ip d：CH(provider) individual queue；,2019/5/31,35,第四章 协议形式描述语言,在各自的模块中发出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形成的联接无通讯能力。,2019/5/31,36,第四章 协议形式描述语言,5ip队列（输入队列） 定义ip时必须指明ip的队列性质：common queue或individual queue。多个模块使用同一个通道时，它们可使用自己的单独队列，也可以共享队列。如果定义在通道同一端的ip队列为common queue，那么定义这些ip的模块使用共享队列。,2019/5/31,37,第四章 协议形式描述语言,图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的共享队列。,2019/5/31,38,6. 输入和输出 when 语句从ip读一个事件，而output语句往ip输入一个事件。格式为： when ip.m(arquments) output ip.m(arquments) 这里m(arquments)必须是channel定义中指明交互事件.when语句从ip的队列(FIFO)读出事件,该事件是联接的另一端output语句所输入的事件.由于FIFO队列的原因,输出和输入不是同时发生的,因此模块通讯是异步的,第四章 协议形式描述语言,2019/5/31,39,第四章 协议形式描述语言,4.2.3 状态转换的描述 状态转换部分是模块中最重要的部分.模块状态转换的描述基于扩展有限状态机模型(EESM),其描述直观明了： 1、描述语句 trans 表示状态转换群开始,一个模块体可有多个状态转换群. when ip.m 从ip读一个事件 from A 转换发生前的状态为A to B 转换发生后的状态B provided E 转换的条件,E为布尔表达式 delay(E1,E2) 转换至少延迟单位时间,最多单位时间.单位时间的大小 在全局specification语句中说明 priority E 转换的优先级为E,E为布尔表达式. any var do 当内容相同的一组转换存在,而变量var值不同时,可用 此语句缩短转换的描述.,2019/5/31,40,第四章 协议形式描述语言,例如: trans when ip.m from A any x:13 do provided E(x) to C begin S1;S2; end; 这里any语句把X=1,X=2和X=3时三个转换合成一个简练的转换.如果不用any语句,上述描述必须重复三次,每次转换中的provided语句不同,其它相同. S1,S2,.为转换所执行的事件或过程(包括output语句).,2019/5/31,41,第四章 协议形式描述语言,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只认为交付的转换就一定执行.,2019/5/31,42,第四章 协议形式描述语言,4.2.4 AB协议的ESTELLE描述 本节所描述的整体AB协议系统(类别为system process)如图4.4所示.系统中存在多个AB协议模块实例(类别为process),每个AB协议对应一个用户模块实例(类别为process).所有AB协议模块实例共享一个网络模块实例(类别process).用户模块实例和网络模块实例为外部模块(external),它们由其它ESTELLE文本描述.,2019/5/31,43,第四章 协议形式描述语言,图4.4 AB协议系统,2019/5/31,44,第四章 协议形式描述语言,系统定义两个通道:Uaccesspoint和Naccesspoint.前者为AB协议模块与用户模块的接口,后者为AB协议模块和网络模块的接口。接口(通道之间)的通讯原语示于图4.4中. AB协议模块既是sender也是receiver.为了缩小状态转换部分的篇幅, （1）AB协议模块作为sender只定义了两个状态:ESTAB(初始状态),ACKWAIT(等待认可报文), （2）作为receiver没有定义状态. （3）多个用户实例和多个AB协议模块实例用数字标识.,2019/5/31,45,第四章 协议形式描述语言,Sender用Source_id标识它自己，并由Send-request和data-request的参数destination决定。如果有n个用户，那么通道N-access-point两端各定义n个ip,并用n个connect语句约束在一起。,2019/5/31,46,第四章 协议形式描述语言,示例程序：,2019/5/31,47,2019/5/31,48,2019/5/31,49,2019/5/31,50,2019/5/31,51,2019/5/31,52,第四章 协议形式描述语言,4.2.5 ESTELLE的特点与应用方法 ESTELLE的基本特点可归纳如下： (1) 基于扩充有限状态机(EFSM)的FDL，专为协议描述而设计。 模块实例可通过初始化语句动态产生。如果协议实现后模块实例对应于一个进程或任务，那么网络进程或任务也是动态产生的。 (2) 模块通讯为异步通讯。 (3) ESTELLE是pascal语言的扩充，用ESTELLE描述的协议容易转换成pascal或C代码。因此，它是一种面向协议实砚的FDL。 (4) ESTELLE对并发、不确定性、超时、异步通讯状态转换有较强的表达能力，但对递归、共享通道（广播通道）、同步通讯、协议性质（如不变性等）的表示缺少有力的手段。,2019/5/31,53,第四章 协议形式描述语言,用ESTELLE描述的协议易于提取FSM模型和Petri网模型，但不容易提取转变成TL和CCS模型。 用ESTELLE描述一个协议，最重要的工作(也是第一步工作)就是构造协议的模块结构和通讯机制。系统由多少层模块构成？每个模块应该是什么类别(类别决定了工作方式)？定义多少通道和交互点？交互点队列属于哪种？它们约束成什么样联接？这些问题必须作出周密安排；否则将影响协议实现后执行效率，例如应该定义为system process类别的模块定义system activity之后，并行性就会失去。论文3给出了ISO传输层协议的ESTELLE描述。是一篇很好的参考资料。,2019/5/31,54,第四章 协议形式描述语言,4.3 LOTOS概述 LOTOS 的基本思想是： 外部可观察到的系统行为由一系列的交互作用组成， 通过对这些交互作用的时间关系进行定义， 从而描述整个系统。在定义这些交互作用的时间关系时，不是采用时序逻辑的方式，而是基于进程代数的方法。 LOTOS 规 格（ specification ）主要包括数据类型的定义和进程的定义两个部分，其整体结构大致如下 ： SPECIFICATION 规格名 全局类型定义 进程定义 ENDSPEC,LOTOS 具有如下基本特点。 LOTOS 是基于进程代数 CCS 和多类代数 (Many-Sorted Algebra) 的 FDL ，是一种为适应协议工程、分布处理和并行处理技术 的要求而产生的语言。 进程通信为同步通信。 LOTOS 不是面向协议实现的语言。例如，它只是在抽象数据类型定义中给出协议内部操作的性质说明，而没有给出操作怎样实施的说明。从而，在将 LOTOS 描述的协议转变成程序设计语言（如 C,Pascal ） 代码时需要做许多工作。 用 LOTOS 描述的协议很容易转换成 CCS 或 CSP 模型，也比较容易转换成 TL, FSM 或 Petri 网模型。 LOTOS 的不足之处体现在以下几个方面。无异步通信机制，无清晰的记录型数据结构的描述手段，无常量描述手段，可读性差等。,2019/5/31,55,第四章 协议形式描述语言,4.3.1 进程定义 LOTOS将一个系统看做多个相互作用的子进程组成的进程，每个子进程又是由多个子进程构成。进程定义为： process process-id gate-list (parameter-list):noexit:= endprocess 这里process和endprocess为关键词，表示进程定义的开始和结束。process-id为进程名，gate-list为门径表(参见4.3.4) ; parameter-list为参数表(类似子程序设计语言的过程定义中的哑元); behaviour-expression为描述进程行为的表达式(参见4.3.2); noexit为关键词，表示该进程为非终止进程; 关键词exit说明一个终止进程。,2019/5/31,56,第四章 协议形式描述语言,2019/5/31,57,第四章 协议形式描述语言,图 3-8 具有门径 ag 的进程 P,2019/5/31,58,第四章 协议形式描述语言,进程 Max3 的空间表示,LOTOS 进程中定义的典型结构,2019/5/31,59,第四章 协议形式描述语言,4.3.2 行为算子 多个协议事件和行为表达式可用行为算子组合成新的行为表达式。 1.行动前辍(action-prefix) 行动前缀(用符号”;”)说明进程顺序执行事件的行为，它对应于CCS的“.”算子。例如： 2.选择(choice) 选择(用符号”)说明进程从多个行为表达式中选择一个去执行的行为，它对应于CCS的“+”算子。例如：B1B2 表示选择B1或B2执行,2019/5/31,60,第四章 协议形式描述语言,3.并行(parallelism) 并行算子说明进程并行执行多个行为表达式的行为，它对应于CCS的“|”算子。LOTOS的并行算子有三种形式： 4.串行( sequentiality ) 串行算子(用符号“”)说明进程执行一个行为表达式之后“使能”另一个行为表达式的行为，它是CCS顺序算子变种S1和S2(参见3.5)。 例如：B1B2 如果B1成功结束使能B2。,2019/5/31,61,第四章 协议形式描述语言,5.作废(disruption) 作废算子(用符号“|”表示)说明进程在后个行为表达式的事件发生时停止并且作废前个行为表达式的行为，它类似于CCS的并行算子变种 (参见3.5)。 例如：B1|B2 执行B1时如果B2有事件发生，作废B1，执行B2。 6.隐藏(hide) 隐藏算子说明进程执行并行算子时隐藏内部协同事件的行为，它和CCS在利用扩展规则时限止协同事件的效果相同。隐藏算子的形式为： Hide a in B a为内部事件，B行为表达式。 7. 看守(guard) 看守表达式说明一个行为表达式是否执行的条件，其形式为： cond-B cond为条件表达式或谓词，B为行为表达式。cond为真，执行B。,2019/5/31,62,第四章 协议形式描述语言,8. 终止(termination) 表示进程的终止有两个关键词：exit和stop exit 成功结束； stop 停止进程活动 9.内部事件 一个进程的内部事件用“I”表示，不确定性选择也用“I”表示。 例如：I;a;A I;b;B 为了说明上述算子以及LOTOS语言的能力，我们举一个双缓冲通道的例子。图4.5中进程two-slot-bufferi,o为两个单缓冲进程bufferi,m和bufferm,o并行组合而成，事件m为它们协同事件，系统定义如下：,2019/5/31,63,第四章 协议形式描述语言,exam1: process two-slot-bufferi,o:= hide m in bufferi,m|m|bufferm,o where process bufferinput,output:= input;output; bufferinput,output endproc endproc,2019/5/31,64,第四章 协议形式描述语言,上述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)式变成：,2019/5/31,65,（4）式和（5）式就是外部观察者所见到的双缓冲通道的特征。（4）式和（5）式反过来用LOTOS描述成互相嵌套的进程(exam2)。 Exam2: Process two-slot-bufferi,o:= i;Qi,o endproc process Qi,o:= o;two-slot-bufferi,o i;o;Qi,o Endproc 我们已用CCS的代数变换法则证明了exam1和exam2是完全观察等价的。,第四章 协议形式描述语言,2019/5/31,66,第四章 协议形式描述语言,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和succ。o操作的含义是：0是自然数类型;succ操作的含义是：自然数类型的数的后继数（successor）也是自然数类型. 上面的Opns操作只是声明了个操作，同时指明了各操作从定义域到值域的关系。,2019/5/31,67,第四章 协议形式描述语言,一个定义引用另外一个定义的目的有两个：对一个已有的类型进行扩充，或将几个定义合成一个新定义。 Exam4： Type enrich-nat-number is nat-number with Opns _+_:nat,nat-nat Eqns forall x,y:nat Ofsort nat x+0=x; x+succ(y)=succ(x+y); endtype 这里，enrich-nat-number是nat-number的扩充，类型名仍然是nat，opns之后_+_定义了一个扩充的操作“+”，它是二元操作；自然数+自然数仍然是自然数。关键词eqns说明自然数三个操作（0，succ,+）的性质。关键词forall说明对于所有自然数x和y,关键词ofsort说明等式两边的数据类型。,2019/5/31,68,第四章 协议形式描述语言,为了进一步理解抽象数据类型的定义方法，举自然数队列为例。 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。,2019/5/31,69,第四章 协议形式描述语言,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等是输入输出参数,2019/5/31,70,第四章 协议形式描述语言,进程从门径变量输入用“？”操作符，向门径变量发送用“！”操作符。输入输出操作必须采用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;,2019/5/31,71,第四章 协议形式描述语言,(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=,2019/5/31,72,第四章 协议形式描述