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

CCS及其变换规则 【第二页】 协议是数据通讯、计算机网络 、多机系统等分布系统的灵魂 。分布系统的特征是它的分布性 、并发性 、异步性 、实时性 、以及信道不可靠性 ，这意味着它的协议一定复杂。此外 ，随着分布系统的发展 ，它的功能越来越多，所提供的服务越来越丰富 ，异种系统的互通 、互操作性要求越来越高 ，这就进一步增强了协议的复杂度 。复杂的协议不但意味着协议的开发难度大 ，周期长 ，而且分布系统产品中的潜在错误多 。协议开发过程中任何一点错误和缺陷都将给分布系统的稳定性 、可靠性 、安全性带来巨大的危害。为此 ，　一门新的计算机学科——一协议工程 (protocol　engineering)便产生了。 协议工程旨在减少协议开发中潜在错误 ，提高开发效率 ，促进标准化发展 。协议工程包括形式描述 、协议验证 、协议综合 (protocol　synthesis)、协议实现半自动化 、协议一致性测试等多方面的理论和技术 ，其中最关键的是形式描述技术 。形式描述技术要解决的问题是 ，用什么样的数学模型才能严密地表述协议的逻辑结构 、时序关系及各种协议特性 ，并且还能使得协议验证 、协议综合 、协议实现、协议测试变得容易 。目前 ，人们采用的形式描述技术主要有 FSM (Finite　State　Machines)，Petrinet，TL　(Temporal　Logic)，进程代数等。FSM 由于简单、直观而得到广泛应用 ，但不利于协议验证的实现。Petrinet是 FSM 的变种 ，应用不广泛 。TL过于抽象 ，不利于描述协议的逻辑结构，难于在协议工程中使用 。 进程代数 (the　Algebra　of　Processes)不但能严密地表述协议的逻辑机构和协议的时序性，而且有利于协议验证的进行。进程代数的开拓性工作是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.Q Q=b.P+d.Q 联立表达式描述进程P和Q的迭代关系，进程Q从事件b和d中选择一个执行（可选择受事件a的执行结果的制约） 【第六页】 并行操作（|） 并行算子将多个进程组合成一个进程，并行算子用符号“|”表示。例如 P=a.b.NIL Q=b.P+d.Q X=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中两个表达式所表现的行为）