CCS及其在AB协议中的运用.doc

CCS及其变换规则【第二页】协议是数据通讯、计算机网络 、多机系统等分布系统的灵魂 。分布系统的特征是它的分布性 、并发性 、异步性 、实时性 、以及信道不可靠性 ，这意味着它的协议一定复杂。此外 ，随着分布系统的发展 ，它的功能越来越多，所提供的服务越来越丰富 ，异种系统的互通 、互操作性要求越来越高 ，这就进一步增强了协议的复杂度 。复杂的协议不但意味着协议的开发难度大 ，周期长 ，而且分布系统产品中的潜在错误多 。协议开发过程中任何一点错误和缺陷都将给分布系统的稳定性 、可靠性 、安全性带来巨大的危害。为此 ，一门新的计算机学科一协议工程 (protocolengineering)便产生了。协议工程旨在减少协议开发中潜在错误 ，提高开发效率 ，促进标准化发展 。协议工程包括形式描述 、协议验证 、协议综合 (protocolsynthesis)、协议实现半自动化 、协议一致性测试等多方面的理论和技术 ，其中最关键的是形式描述技术 。形式描述技术要解决的问题是 ，用什么样的数学模型才能严密地表述协议的逻辑结构 、时序关系及各种协议特性 ，并且还能使得协议验证 、协议综合 、协议实现、协议测试变得容易 。目前 ，人们采用的形式描述技术主要有 FSM (FiniteStateMachines)，Petrinet，TL(TemporalLogic)，进程代数等。FSM 由于简单、直观而得到广泛应用 ，但不利于协议验证的实现。Petrinet是 FSM 的变种 ，应用不广泛 。TL过于抽象 ，不利于描述协议的逻辑结构，难于在协议工程中使用 。进程代数 (theAlgebraofProcesses)不但能严密地表述协议的逻辑机构和协议的时序性，而且有利于协议验证的进行。进程代数的开拓性工作是R.Miler的通信进程演算（CCS,Calculus of Communication System）.Hoare 在CCS的基础上建立了通信顺序进程（CSP，Communicating Sequential Processes）.除CCS和CSP外，还建立了其他一些进程代数，而CCS是进程代数的基础。【第三页】一、CCS算子通信进程演算（CCS）是计算机通信系统的基本理论模型，它也许是许多形式化语言的基础。CCS的基本成分是事件与进程，而进程是通过顺序、选择和并行三个基本算子来定义的。我们可以用大写字母来表示进程，用小写字母来表示事件。【第四页】顺序算子（.） 顺序执行事件的行为用顺序算子描述，顺序算子用句点“.”表示。事件之间用“.”连接，得到事件序列。在事件序列中，事件是按照从左向右的顺序执行的。用顺序算子可以定义进程，例如：P=a.b.NIL （进程P顺序执行事件a和b之后终止。NIL表示“终止”进程或“空”进程，Q=NIL表示一个空进程。 ）A=a.c.A (递归进程，非终止进程)非终止进程可写成展开形式，上式的P2展开后为A=a.c.(a.c.(.(a.c.A).)=a.c.a.c.a.c.A对于顺序算子，括号是多余的，因为进程总是按照从左向右的顺序执行事件。【第五页】选择算子（+） 选择算子描述进程从多个事件中选择执行一个行为，选择算子用符号“+”表示。例如：P=a.QQ=b.P+d.Q联立表达式描述进程P和Q的迭代关系，进程Q从事件b和d中选择一个执行（可选择受事件a的执行结果的制约）【第六页】并行操作（|） 并行算子将多个进程组合成一个进程，并行算子用符号“|”表示。例如P=a.b.NIL Q=b.P+d.QX=P|Q=a.b.NIL|(a.d.NIL+e.NIL)注意：并行操作不能用于事件，例如：X=a|b是非法表达式，而X=a.NIL|b.NIL 是合法表达式。【第七页】二、CCS变换规则任何一个代数系统都有一套表达式的“等价”变换规则，这是代数系统的核心。“等价”的含义根据代数系统的不同而不同。在初等代数中，“等价”指数值相等，因此，结合律ac+bc=(a+b)c，分配律a(b+c)=ab+ac是成立的。在CCS中，表达式的变换规则基于“观察等价（Observational Equivalence）”。对外部观察者来说，如果进程执行的两个表达式所表现的行为时不能区分的，那么这两个表达式是等价的。基于这一原则，初等代数的分配律在CCS中不成立，例如a.(b.P+c.Q)和a.b.P+a.c.Q不等价。对于前者，进程执行事件a之后，其结果可能影响b和c的选择。对于后者，进程不确定地选择一个事件执行（因为第一个事件都是a），a的执行结果不能影响b和c的选择。（如图所示在CCS中两个表达式所表现的行为） a a a c b c b NIL NIL NIL NIL【第八页】（1） 基本规则P+P=PP+NIL=Pa.P+(b.Q+c.R)=(a.P+b.Q)+c.R a.P+b.Q=b.Q+a.P 选择算子的交换规则P|Q=Q|P 组合算子的交换规则P|(Q|R)=(P|Q)|R 组合算子的分配规则【第九页】（2） 扩展规则。CCS最重要的理论是基于协同事件的扩展规则，它将包含并行操作的表达式变换成不含并行操作的表达式，下面我们用a（输出）和(输入)的形式表示一对协同事件，忽略它们的发生点和传递的数值。两个进程用并行操作组合在一起时，它们通过协同事件进行同步，并交错执行各自的独立事件。设ai为进程A的事件，bj为进程B的事件，A和B分别定义为: A=a1.A1+a2.A2+ +ai.Ai+ =ai.Ai B=b1.B1+b2.B2+ +bj.Bj+ =bj.Bj A和B并行组合后扩展为：A|B=ai.(Ai|B)+bj.(A|Bj)+I.(Ai|Bj) 其中，aj和bj为协同事件，I表示一对协同事件。【第十页】为了理解扩展规则，举例如下：a.P|b.Q=a.(P|b.Q)+b.(a.P|Q)a.P|.Q=a.(P|.Q)+.(a.P|Q)+I.(P|Q)(a.P+b.Q)|.R=a.(P|.R)+b.(Q|.R)+(a.P+b.Q)|R)+I.(P|Q)在第一个例子中，a.P和b.Q分别为两个进程的行为。当我们把这两个进程组合成一个进程时，观察者所看到的组合行为有两种可能：先执行事件a，然后P和b.Q并行，或者先执行是事件b，然后a.P和Q并行。用“观察等价”去看扩展规则，它的含义是很好理解的。【第十一页】（3）限制规则扩展规则使表达式变得非常冗长复杂。如果在使用限制规则限制某些事件的执行时，那么表达式就会变得简单。哪些事件应该列入限制范围需要根据进程的具体内容、表达式变换的目的和要求而定。有时可将一些内部事件列入限制范围。然而，更常用的做法是将单个协同事件列入限制范围，例如，a和应该列入限制范围，但是由它们形成的I事件不列入限制范围，实际上a和是不能单独出现的。限制操作符号用“/”表示，“/”之后的字符表示列入限制范围的事件。设a和，e和为两对协同事件，下面的例子表示出限制操作符的作用。注意，限制a也将限制。(a.P|.Q）/a=I.(P/Q)/a (a.P|.Q)/a,e=NIL 【第十二页】（4）隐藏内部协同事件扩充规则产生的协同事件对组合后的进程来说是内部事件。在某些情况下，这些事件可以隐藏，并从表达式中消去。内部事件的隐藏基本规则是I.P=P a.I.P=a.P 值得注意的是，（I.P+I.Q）不能化简为 (P+Q)。这是因为，前者为不确定选择（第一个事件相同）。CCS基于协同事件 (co-events)概念。两个并行组合的进程进行会合(rendezvous)通讯时，发生在会合点的“收”和“发”事件 ，或者“读”和“写”事件就是一对协同事件。我们用a(发，写 )和 (收 ，读 )的形式表示协同事件对。一个进程执行的事件分两大类：通讯事件和非通讯事件。非通讯事件包括超时、报文丢弃等。对于CCS来说 ，所有通讯事件都是协同事件。当进程 A 和 B并行组合 (A|B)时