《[互联网]第3章 协议模型技术.ppt》由会员分享，可在线阅读，更多相关《[互联网]第3章 协议模型技术.ppt（89页珍藏版）》请在三一办公上搜索。
1、网络协议工程,南京邮电大学计算机学院,2/89,第3章 协议模型技术,3.1 引言3.2 有限状态机(FSM)3.3 Petri网3.4 时序逻辑(TL)3.5 通信进程演算(CCS),3/89,3.1 引言,协议模型技术是协议工程的核心技术之一，是协议工程的基础。形式描述语言、协议正确性验证、协议自动化实现以及协议测试都基于某种模型技术。协议模型技术旨在精确地表述(n-1)层通道，n层局部系统和全局系统的行为和性质。n层局部系统由各种协议元素组成，因此，模型技术必须精确地表述各种协议元素的性质和行为，以及它们之间作用关系(即协议机制)。全局系统性质即协议性质。,4/89,3.1.1 协议性质
2、,3.1.1 协议性质3.1.2 协议元素性质3.1.3 通道类别3.1.4 协议模型的选取,5/89,3.1.1 协议性质,一个好协议应该具有的协议性质，主要包括：1 活动性(liveness)2 安全性(Safety)3 一致性(consistency)4 完备性(completeness),6/89,3.1.1 协议性质,1 活动性协议活动性指协议运行时发生所期望的事情，包括：预定的事件会产生、指定的协议状态会达到、应该进行的协议行动会进行等等。活动性体现在终止性和进展性两个方面，如果协议有终止性和进展性也就具有活动性。终止性协议从任何一个状态开始运行，总能正确地达到终止状态。进展性协议
3、从初始状态运行，总能正确地达到指定状态。某些情况下，终止状态和初始状态是同一的，协议从初始状态开始运行总能正确地回到初始状态，并可反复运行，即具有回归性。回归性终止性进展性活动性,7/89,3.1.1 协议性质,活动性可以从事件状态表观察和分析协议活动性。一个简单系统示例：,(a)事件状态表,(b)FSM图,8/89,3.1.1 协议性质,2 安全性(Safety)协议安全性指协议运行时没有坏事情出现。这些坏事情包括不可接收的事件、不可进一步向前的状态、错误的行动、错误的条件、变量值越界等等。坏事情一般导致两种现象：死锁(deadlock)协议堵塞在某一个状态而无法向前活锁(livelock)
4、协议作无意义的循环示例：从事件状态表和FSM观察死锁和活锁现象。假定O1-I2不能保证，即不能产生I2(坏事情产生)，则系统在S0时收到I1之后就永远停止在S1上，除非再次输入I3，否则无法回到S0，即死锁。假定S3收到I3后，输出O2,转到S0，则导致S0、S1和S3无止境循环，即活锁。,9/89,3.1.1 协议性质,3 一致性一致性是指协议服务行为(性质)和协议行为(性质)一致。一致性包括两个方面：协议应该提供用户要求的服务；协议无需提供用户没有要求的服务。,10/89,3.1.1 协议性质,4 完备性完备性是指协议性质完全符合协议环境的各种要求，即协议的构造考虑了用户要求、用户特点、通
5、道性质、工作模式等各种潜在因素的影响，考虑了各种错误事件、异常情况的处理。,11/89,3.1.1 协议性质,注1：协议性质的分类一般性质：与协议具体内容无关的性质，如：安全性和活动性。协议验证技术所侧重的。特殊性质：与协议具体内容相关的性质，如：一致性和完备性协议测试技术所侧重的。注2：一致性部分正确性等价性完备性完全正确性有界性：协议元素性质和通道性质,12/89,3.1.2 协议元素性质,协议元素性质对协议模型有重要影响协议元素性质如下：1 事件成对性2 事件原子性3 事件时序性4 状态时序性5 变量有界性6 过程的原子性,13/89,3.1.2 协议元素性质,事件成对性事件分通信事件和
6、内部事件两类，通信事件是成对出现的，而内部事件不是成对出现的。例如，n层用户发出服务原语(输出事件)和n层协议接收到服务原语(输入事件)成对地出现在(n)SAP的两侧，(n)SAP为事件发生点。n层协议实体A发出一个PDU和B收到一个PDU是一对通信事件，出现在两个(n-1)SAP上，出现在两个不同的事件发生点。,14/89,3.1.2 协议元素性质,事件成对性通信事件分两类：同步事件(也叫协同事件)：输入事件和输出事件发生在同一个事件点上，同时出现。异步事件：输入事件和输出事件发生在两个事件点上，不同时出现，输出事件滞后于输入事件,15/89,3.1.2 协议元素性质,事件原子性不论通信事件
7、还是内部事件要么不发生，一旦发生就一定完成，这种性质称为事件的原子性。有原子性的事件称为原子事件(atomic events)。例如，当n层协议实体向(n-1)层通道输出一个报文时，输出一旦启动，即使是输出失败(通道丢失报文)，事件“输出报文”也认为已发生。假定所有事件都有原子性。,16/89,3.1.2 协议元素性质,事件时序性服务原语状态图表述了服务原语的时序关系PDU交换规则表述了PDU的时序关系通信事件由服务原语和PDU的交换引起，因此，服务原语状态图和PDU交换规则决定了通信事件时序性。状态时序性事件时序性决定了状态时序性变量有界性协议变量的取值范围有明确定义,17/89,3.1.2
8、 协议元素性质,过程的原子性一个协议过程可能包括多个协议行动，过程一旦启动之后，所有包括的行动一次性完成，不经历中间协议状态，不被其它过程打断，这种性质就是过程的原子性，具有原子性的过程为原子过程。协议运行时，从一个状态到另一个状态的转换可处理成原子过程。,18/89,3.1.3 通道类别,通道分成三类：空通道报文的传送时间和延时时间为0的通道。非缓冲通道任何时刻，最多只有一个正在传送中报文的通道缓冲通道允许有多个报文停留的通道,19/89,3.1.3 通道类别,事件点、事件通道的两端为两个通信事件发生点，一个报文从通道一端传送到另一端的过程中，两个事件点产生四个事件。两个端点分别标记为a和b
9、，假定报文从a端传送到b端，经历：a端用户通道a端通道b端b端用户四个事件的含义：a!m a端用户向通道a端发送报文ma?m 通道从a端接收报文m，并启动传送b!m 通道完成报文传送，将报文发送给b端用户b?m b端用户从通道b端接收报文,20/89,3.1.3 通道类别,四个事件的含义：a!m a端用户向通道a端发送报文ma?m 通道从a端接收报文m，并启动传送b!m 通道完成报文传送，将报文发送给b端用户b?m b端用户从通道b端接收报文a!m与a?m、b!m与b?m是协同事件(同步事件)a!m与b?m、a?m与b!m是异步事件假设报文传送延时T秒，异步事件延迟为T秒对于空通道，T0，a!
10、m与b?m、a?m与b!m可处理为同步事件。通道工作方式可以是单工、半双工、全双工。全双工可视为两个独立的单工通道。,21/89,3.1.4 协议模型的选取,来自数学模型(或方法)、自动机模型(或程序模型)理想的协议模型能方便地充分地表示协议元素和通道的各种性质，有强的表达能力和实用性；容易观察协议性质，容易进行协议验证和测试。模型FSM、Petri网等,22/89,3.2 有限状态机(FSM),FSM定义通道FSM协议实体FSMFSM简化FSM合成FSM扩充,23/89,3.2.1 FSM定义,有限状态机FSM定义为四元系统，其中，S是系统状态集，状态数有限，(无限状态机为图灵机)i为系统初
11、始状态，iSE为原子事件集T为状态转换函数集,24/89,3.2.1 FSM定义,有限状态机FSM转换函数定义为当系统处于状态Si时，如果发生事件e，那么系统状态变成Sj。FSM可以用于协议模型技术能表示协议元素的时序性以及状态随事件变化的关系具有直观易懂的优点。,25/89,3.2.1 FSM定义,有限状态机FSM图形表示法圆圈 表示状态，圆圈内的符号表示状态含义弧 带箭头的弧表示状态转换，弧的标识表示事件黑点圆 中心为黑点的圆表示初始状态方框 表示系统边界，边框上的小圆表示事件发生点(或系统和外界的耦合点)。,26/89,3.2.2 通道FSM,空通道状态数为1，即只有一个初始状态。真正的
12、空通道不存在，但是我们有时可将非缓冲通道简化成空通道。非缓冲通道假设一个方向上传送的报文相同，则单工非缓冲通道状态数为2，半双工的状态数为3，全双工的状态数为4。,27/89,3.2.2 通道FSM,非缓冲通道FSM示例：,28/89,3.2.2 通道FSM,图(a)表示单工FSM，初始状态表示通道中无报文，状态1表示报文在传送中，ma表示a端用户报文。图(c)表示半双工FSM,状态1表示a端用户报文ma在传送中，状态2表示b端用户报文mb在传送中。,29/89,3.2.2 通道FSM,缓冲通道其状态数随通道中允许停留的报文数目和报文种类数而急剧增加。如果所有报文相同，则队列边界为n的单工缓冲
13、通道的状态数为(n+1)，队列边界表示通道中缓冲队列的最大允许长度；对于全双工通道，状态数为(n+1)2很多情况下，通道中的报文是不同的，如，顺序号不同。如果通道中有多个不同的报文(每种报文最多一个，并且报文有序)，那么边界为n的单工缓冲通道的状态数为2n个。,30/89,3.2.2 通道FSM,缓冲通道,31/89,3.2.3 协议实体FSM,以AB协议系统为实例，说明怎样用FSM表示协议实体,32/89,3.2.3 协议实体FSM,图(a)为AB协议系统，S和R为协议实体，S表示发送端，R表示接收端。A、B分别为AB协议系统和其用户的耦合点。通道CH为非缓冲通道，端点分别为a和b。,33/
14、89,3.2.3 协议实体FSM,S有四个状态1 S已从A接收报文，顺序号置成0，报文命名为m02 S已向a发出m0，等待R的ack03 S已从A接收报文，顺序号置成1，报文命名为m14 S已向a发出m1，等待R的ack1R有四个状态1 R已从b接收报文m02 R已向b发ack03 R已从b接收报文m14 R已向b发ack1,34/89,3.2.3 协议实体FSM,图(b)为S的FSM图(c)为R的FSM,35/89,3.2.4 FSM简化,FSM的缺点是会产生状态爆炸。队列边界为n的系统的FSM的状态数可大于2n，两个状态数为x和y的FSM合并后的状态数可为xy。FSM简化旨在减少状态数。,
15、36/89,3.2.4 FSM简化,FSM简化方法方法1 状态层次化方法2 使用原子过程方法3 使用协议变量方法4 隐藏内部协同事件方法5 通道FSM的简化,37/89,3.2.4 FSM简化,方法1 状态层次化将若干协议功能按阶段组织起来设置状态，然后分阶段设立子状态，可大大减少每一级的状态数。如：ISO T层协议设立22个总状态，数据传输阶段为状态OPEN，在此阶段还包括若干子状态。在只考虑连接建立和撤销等协议功能时，定义22个总状态就可以了。如：TCP协议设立了12个总状态。数据传输阶段为状态ESTAB。,38/89,3.2.4 FSM简化,方法2 使用原子过程在FSM的四元系统中，如果
16、转换函数SiSjT和SjSkT能够合并成SiSkT，那么状态Sj就可以消去。两个转换函数对应于两个协议过程，它们能够合并的准则是：合并后的过程为原子过程。如：单工非缓冲通道的a?ma和b!ma,a?ma和drop可合并成两个原子过程。,39/89,3.2.4 FSM简化,方法3 使用协议变量FSM扩充中使用该方法,40/89,3.2.4 FSM简化,方法4 隐藏内部协同事件两个系统的FSM合成时，合成之前两个系统的耦合点变成合成系统的内部事件点，合成之前分别出现在两个系统中的协同事件变成合成系统的内部事件。内部协同事件根据需要可以隐藏，相关联的状态可以合并。隐藏内部协同事件的方法：,41/89
17、,3.2.4 FSM简化,方法4 隐藏内部协同事件隐藏内部协同事件的方法：第一步：用I表示内部协同事件。如果，并且e1和e2为协同事件，那么，I=。第二步：合并关联的两个状态。SiSk合并成一个状态，或重新定义成一个新状态。Sj是否消去，根据其它方法进行。,42/89,3.2.4 FSM简化,方法5 通道FSM的简化简化原则原则1：如果n层协议实体采用同步通信方式(一问一答)，那么不管(n-1)层通道是否缓冲通道，都可以处理成非缓冲通道。原则2：如果报文传送时间和延时时间对协议机制无影响，或者只影响协议变量的值，那么非缓冲通道可处理成空通道。,43/89,3.2.4 FSM简化,44/89,3
18、.2.5 FSM的合成,全局系统的FSM是由各个局部系统和通道系统的FSM合成的。合成过程1 简化各个FSM2 两个单工通道合成一个全双工通道3 对任意两个彼此耦合的系统合成中间合成系统，简化中间合成系统，然后将中间合成系统再合成，直到获得全局FSM为止。任意两个耦合系统的FSM的合成步骤和规则：P42,45/89,3.2.5 FSM的合成,假定两个FSM系统分别为F1=和F2=，合成后系统为F=。任意两个耦合系统的FSM的合成步骤和规则：i=(i1,i2),其中，iS，i1S1，i2S2。即，合成系统的初始状态为两个系统初始状态的组合。S=S1*S2，如果sS1，rS2，那么(s,r)S，S
19、的状态数为S1和S2状态数的乘积。E=E1E2，如果e1E1，e2E2，那么e1E，e2E。E的事件数为E1和E2事件数之和。T=T1T2，如果，那么；如果，那么，T的转换函数的数目为T1和T2数目之和。合成后，消去无用的状态，必要时隐藏内部协同事件。,46/89,3.2.5 FSM的合成,47/89,3.2.5 FSM的扩充,纯粹FSM只反映了协议事件和协议状态之间的关系，不能表述最重要的协议元素：协议变量、协议行动、谓词。扩充的FSM引入协议变量、谓词和行动(对变量进行操作)使得FSM的转换函数变得丰富而复杂。弥补了纯粹FSM的不足。,48/89,3.2.5 FSM的扩充,扩充方法引入谓词
20、、行动用转换函数 替代，t=e/p:a。e表示输入事件，eE；p表示谓词；a表示行动(包括输出事件，对变量进行的操作等)。如果系统从一个状态到另一个状态的转换不包含输入事件，t=p:a。引入协议变量引入协议变量可以减少状态数。协议行动对协议变量执行操作。如seq=(seq+1)mod 2。,49/89,3.2.5 FSM的扩充,示例：引入协议变量seq，减少了状态数。S状态数53，R状态数52。,50/89,3.3 Petri网,Petri网概念Petri网特性Petri网扩充协议实体Petri网通道Petri网Petri网的替换与合成协议并发性表示,51/89,3.3.1 Petri网的概念
21、,Petri网的提出1962年，波恩大学的C.A.Petri提出一种可表示系统部件异步并发操作的网络模型，后来取名为Petri网。该模型已广泛应用于计算机科学、电子学、机械学、化学、物理学等许多领域。也非常适合于协议模型技术。,52/89,3.3.1 Petri网的概念,1 Petri网定义Petri网定义为一个五元系统，其中，P：位置(places)集，P=p1,p2,pi,T：转换(transitions)集，T=t1,t2,ti,I：输入函数集，I=I(t1),I(t2),I(tj),，转换tj的输入函数I(tj)=pk,.,.plO：输出函数集，O=O(t1),O(t2),O(tj),
22、，转换tj的输出函数O(tj)=pm,.,.pnM：标记(marking)集，M=m1,m2,mk,，m0为初始标记，mk为第k次标记。标记mk为一个向量，mk=p1(n),p2(n),pi(n),，pi(n)为一个正整数，表示位置pi中的旗标数(tokens)。Petri网的标记也叫Petri网的状态，m0为初始状态，mk为状态k，M为Petri网的状态集合。,53/89,3.3.1 Petri网的概念,1 Petri网定义Petri网的表示用图形表示圆为位置，短线为转换，连接圆和短线的有向弧为输入函数或输出函数，圆中的黑点为旗标。,54/89,3.3.1 Petri网的概念,1 Petri
23、网定义Petri网的示例,55/89,3.3.1 Petri网的概念,1 Petri网定义无界网及其状态空间,56/89,3.3.1 Petri网的概念,2 Petri网的触发规则Petri网的特点之一是可运行性。Petri网的运行由连续的触发(firing)来进行。触发规则当转换tj的输入函数I(tj)=pk,pl的所有位置都至少有一个旗标存在时，tj被触发。tj触发后，输入函数的所有位置分别减少一个旗标，而输出函数O(tj)=pm,pn中的所有位置增加一个旗标。示例：3 Petri网的状态空间每触发一次，状态就变化一次，构成状态序列，可用树表示。,57/89,3.3.2 Petri网特性,
24、1 保守网2 有界网3 活动性4 并发与冲突,58/89,3.3.2 Petri网特性,1 保守网如果一个Petri网的每次触发之后，输出函数所增加的旗标数总是等于输入函数所减少的旗标数，这种Petri网叫保守网，反之叫非保守网。保守网的一个中重要含义是：如果旗标代表 一个系统的资源，那么该系统运行中不能自动生产这种资源，也不会丢失或消耗掉这种资源。2 有界网如果一个Petri网运行中任何一个位置中的旗标数总是不超过K个，这种Petri网就叫K阶有界网，若某个位置的旗标数无限变大，就叫无界网。有界网的一个重要含义是：如果一个Petri网的某个位置代表系统中的一个队列，那么该队列的最大允许长度为
25、K。等等。,59/89,3.3.2 Petri网特性,1阶有界网K阶有界网,60/89,3.3.2 Petri网特性,3 活动性如果一个Petri网在运行中，它的所有转换都是潜在可触发的，那么这个网有活动性。即，从初始标记m0开始，它的任何一个标记都有可能达到，或者从任何一个标记开始运行，它总能返回到初始标记。Petri网的活动性的一个重要含义是：如果用它来表示一个协议，则它的活动性代表着协议活动性。,61/89,3.3.2 Petri网特性,4 并发与冲突多个转换可并发(并行)触发。协议并发所带来的碰撞现象可通过Petri网表达出来一个协议用Petri网表示后，可通过研究Petri网，设法提
26、高协议功能的并发度，检查并解决潜在的碰撞现象。,62/89,3.3.3 Petri网扩充,前面所介绍的标准Petri网难以表示协议性质、协议元素性质和通道性质。需要对其扩充，提高标准Petri网的表达能力。扩充方面1 旗标和位置的扩充2 输入函数和输出函数的扩充3 转换的扩充,63/89,3.3.3 Petri网扩充,扩充方面1 旗标和位置的扩充标准Petri网中，旗标没有名字，没有标识号。着色Petri网(colored Petrinet)允许一个位置中的多个旗标有自己的名字或标识号，这样可扩充旗标的表达能力。例如，当旗标表示系统资源时，着色旗标可表示不同的资源；当旗标表示报文时，着色旗标可
27、代表内容不同的报文或顺序号不同的报文。,64/89,3.3.3 Petri网扩充,65/89,3.3.3 Petri网扩充,2 输入函数和输出函数的扩充打破标准Petri网中输入输出函数在每个位置只减少或增加一个旗标的限制。在标准Petri网中可引入逻辑“或”、“非”和“异或”关系，丰富转换的触发条件。着色Petri网中，还可说明输入函数中不同旗标之间的关系。如，图(c)中转换t的触发条件,66/89,3.3.3 Petri网扩充,3 转换的扩充在转换上标明谓词和行动，这种Petri网叫谓词行动Petri网。,67/89,3.3.4 协议实体Petri网,扩充的Petri网有很强的灵活的表达能
28、力，对于同一个协议实体，不同的人可以构造出不同的Petri网。使Petri网变得简洁、形象直观、含义准确的规则：用转换表示协同事件，如A!m,A?m。外部输入函数和输出函数可用虚线表示。用转换表示内部事件，如超时T和报文丢失drop等。转换上扩充谓词和协议行动用位置表示协议变量(窗口、序号、队列等)和系统资源(缓冲区、连接数等)用位置中的旗标表示资源边界(变量的取值范围，缓冲区的缓冲器数等)尽量不用着色旗标表示资源的名字和标识号，因为着色旗标使Petri网变得复杂。简单的方法是采用谓词行动Petri网。,68/89,3.3.4 协议实体Petri网,对于AB协议，发端S只要设立一个Send-b
29、uffer和ack-buffer，以及变量seq就可以运行。而收端R只要设立一个Receive-buffer和变量seq就可以运行。下图Petri网分别表示S和R。位置和转换的含义说明：S的位置：S1 Send-buffer空 S2 Send-buffer已接收一个报文 S3 Send-buffer中报文已发送，等待认可 S4 ack-buffer中收到ack报文S的转换：t1 A?m,seqm(m为数据报文)t2 a!m t3 a?ack t4 if ack=seq,seq=(seq+1)(mod 2)S初始标记:S1中旗标表示：Send-buffer空，S可以从A接收一个报文。,69/89
30、,3.3.4 协议实体Petri网,R的位置：R1 Receive-buffer空 R2 Receive-buffer中收到一个数据报文 R3 Receive-buffer中组装了一个ack报文R的转换：t7 b?m(m为数据报文)t8 if m has error,drop m t9 b!ack t10 B!m,seq=(seq+1)(mod 2)R初始标记:R1中的旗标表示：Receive-buffer空，R准备接收S发来的数据报文。,70/89,3.3.4 协议实体Petri网,71/89,3.3.5 通道Petri网,单工空通道等效于协同事件点，可表示为一个转换。非缓冲通道单工非缓冲通
31、道：全双工非缓冲通道：用两个单工Petri网表示半双工非缓冲通道：有发信权控制，比较复杂。缓冲通道：单工缓冲通道：全双工缓冲通道：用两个单工Petri网表示,72/89,3.3.5 通道Petri网,73/89,3.3.6 Petri网的替换与合成,用一个低层子系统的Petri网替换高层系统Petri网的一个位置或转换的过程(或反过程)即Petri网的替换。Petri网的替换在协议模型技术中有两种用法。一个协议实体的一个协议功能或模块用一个位置或转换表示，需要时用一个较细的Petri网去替换它。通道只用一个位置或转换表示，需要时再细化。将多个Petri网合成一个大的Petri网的过程即Petr
32、i网的合成,74/89,3.3.6 Petri网的替换与合成,Petri网的替换,75/89,3.3.6 Petri网的替换与合成,Petri网的合成,76/89,3.3.7 协议并发性表示,实际的协议有强的并发性(并行性)。Petri网很适合表示协议的并发性。ISO T层协议(TP4)的数据发送过程为使T层数据发送过程能并发允许，设立变量和系统资源ISO TP4数据发送Petri网,77/89,3.3.7 协议并发性表示,78/89,Ch3 End！,79/89,3.4 时序逻辑TL,名词术语时序逻辑系统AB协议的TL描述协议的TL描述方法,80/89,3.4.1名词术语,命题：非真即假的陈
33、述句个体常量、个体变量、量词：谓词：表示个体变量性质或属性的词函数：多个变量之间的映象项：由数学运算符和关系符联系起来的常量公式：符合形成规则的符合序列公理：作为推理出发的公式定理：根据推理规则由公理推导的公式永真式：其值永远为真的公式原子命题(谓词)：不含任何逻辑操作符的命题(谓词)；逻辑操作符合法公式：按一定的形成规则构成的逻辑符号一阶谓词逻辑：量词只施加于个体变量的逻辑,81/89,3.4.2时序逻辑系统,时序逻辑公式由命题、谓词、函数、常量、变量、量词、和逻辑操作符组成。时序操作符：今后、总是、最终、某时、下次、直到时序逻辑公理：线性TL和分叉TL线性TL将系统的状态序列处理为线性结构
34、分叉TL处理成树形结构,82/89,3.4.3AB协议和TL描述,命题和谓词的表达通道性质的描述协议实体性质 的描述协议性质的描述,83/89,3.4.4协议的TL描述方法,描述原则：用一组公理表述协议的行为和性质协议的TL描述是抽象描述，协议机制被隐含在描述中，协议行动、协议事件被隐含在描述中，协议的状态被隐含在描述中,84/89,描述方法的步骤标识变量、命题和谓词，和协议元素有一定对应关系。描述通道性质描述各个协议实体的行动和性质对已形成的TL描述优化，判定其完整性严密性和正确性对协议进行验证。,85/89,3.5通讯进度演算(CCS),CCS算子变换规则CCS的发展AB协议的CCS描述C
35、CS应用的要点,86/89,3.5.1CCS算子,用三个基本算子定义一个进程：顺序、选择、并行顺序算子：描述进程顺序执行事件的行为，用句点“.”表示选择算子：描述进程从多个事件中选择执行一个的行为并行算子：用”|”符号将多个进程组合成一个进程,87/89,3.5.2 变换规则,表达式的变换规则基于观察等价基本规则扩展规则限制规则内部事件隐藏规则,88/89,3.5.3CCS的发展,基本算子过于简练，不能表达复杂行为，引入附加算子或变种算子顺序算子变种选择算子变种并行算子变种,89/89,3.5.4 AB协议的CCS描述(举例)3.5.5 CCS的应用要点,协议正确性判定协议证明方法观察等价问题CCS的迹通道的CCS描述,
