ccs及其在ab协议中的运用

《ccs及其在ab协议中的运用》由会员上传分享，免费在线阅读，更多相关内容在工程资料-天天文库。

1、CCS及其变换规则【第二页】协议是数据通讯、计算机网络、多机系统等分布系统的灵魂。分布系统的特征是它的分布性、并发性、异步性、实时性、以及信道不可靠性，这意味着它的协议一定复杂。此外，随着分布系统的发展，它的功能越来越多，所提供的服务越来越丰富，异种系统的互通、互操作性要求越来越高，这就进一步增强了协议的复杂度。复杂的协议不但意味着协议的开发难度大，周期长，而且分布系统产品中的潜在错误多。协议开发过程中任何一点错误和缺陷都将给分布系统的稳定性、可靠性、安全性带来巨大的危害。为此，一门新的计算机学科一协议工程(protocolengineering)便产生了。协议工程

2、旨在减少协议开发中潜在错误，提高开发效率，促进标准化发展。协议工程包括形式描述、协议验证、协议综合(protocolsynthesis)＞协议实现半自动化、协议一致性测试等多方面的理论和技术，其中最关键的是形式描述技术。形式描述技术要解决的问题是，用什么样的数学模型才能严密地表述协议的逻辑结构、时序关系及各种协议特性，并且还能使得协议验证、协议综合、协议实现、协议测试变得容易。目前，人们采用的形式描述技术主要有FSM(FiniteStateMachines),Petrinet,TL(TemporalLogic),进程代数等。FSM由于简单、直观而得到广泛应用，但不利

3、于协议验证的实现。Petrinet是FSM的变种，应用不广泛。TL过于抽象，不利于描述协议的逻辑结构，难于在协议工程中使用。进程代数(theAlgebraofProcesses)不但能严密地表述协议的逻辑机构和协议的时序性，而且有利于协议验证的进行。进程代数的开拓性工作是R.Miler的通信进程演算(CCS,CalculusofCommunicationSystem).Hoare在CCS的基础上建立了通信顺序进程(CSP,CommunicatingSequentialProcesses)・除CCS和CSP夕卜，还建立了其他一些进程代数，而CCS是进程代数的基础。【第

4、三页】一、CCS算子通信进程演算(CCS)是计算机通信系统的基本理论模型，它也许是许多形式化语言的基础。CCS的基本成分是事件与进程，而进程是通过顺序、选择和并行三个基本算子来定义的。我们可以用大写字母来表示进程，用小写字母来表示事件。【第四页】顺序算子(・)顺序执行事件的行为用顺序算子描述，顺序算子用句点”表示。事件之间用”连接，得到事件序列。在事件序列中，事件是按照从左向右的顺序执行的。用顺序算子可以定义进程，例如：P=a.b.NIL(进程P顺序执行事件a和b之后终止。NIL表示“终止”进程或“空”进程，Q=NIL表示一个空进程。)A=a.c.A(递归进程，非终

5、止进程)非终止进程可写成展开形式，上式的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.NILQ=b.P+d.QX=P

6、Q

7、=a.b.NIL

8、(a.d.NIL+e.NIL)注意：并行操作不能用于事件，例如：X=a

9、b是非法表达式，而X=a.NIL

10、b.NIL是合法表达式。【第七页】二、CCS变换规则任何一个代数系统都有一套表达式的“等价”变换规则，这是代数系统的核心。“等价”的含义根据代数系统的不同而不同。在初等代数中，“等价”指数值相等，因此，结合律ac+bc=(a+b)c,分配律a(b+c)=ab+ac是成立的。在CCS中，表达式的变换规则基于"观察等价(ObservationalEquivalence)^对外部观察者来说，如果进程执行的两个表达式所表现的行为时不能区分的，那么这两个

11、表达式是等价的。基于这一原则，初等代数的分配律在CCS中不成立，例如a.(b.P+c.Q)和a.b.P+a.c.Q不等价。对于前者，进程执行事件a之后，其结果可能影响b和c的选择。对于后者，进程不确定地选择一个事件执行(因为第一个事件都是a),a的执行结果不能影响b和c的选择。(如图所示在CCS中两个表达式所表现的行为)bNILNILcNIL【第八页】(1)基本规则P+P二PP+NIL=Pa.P+(b.Q+c.R)二(a.P+b.Q)+c.Ra.P+b.Q=b.Q+a.P选择算子的交换规则P

12、Q=Q

13、P组合算子的交换规则P

14、(Q

15、R)=(P

16、Q)

17、R组合算子的分