剖析3 协议模型技术.ppt

第三章 协议模型技术 3 并行算子变种 下面为进程并行组合的几种情况： P 进程通过协同事件耦合（同步并行）； P1 多个完全相同的进程组合在一起和它们的共同外部环境通讯，但是，它们彼此之间当外部环境向它们输入一个事件时，谁执行该事件是不确定的（但只是一个执行），此种情况称为独立并行； P2 一个进程执行一个事件时，该事件对另一个进程来说是中断事件（中断并行）。 在计算机系统中，这三个都是常见的情况，然而，CCS的并行算子不支持P1和P2。所有进程代数都不定义异步并行算子，这是因为进程之间的异步通讯引入队列进程之后变成同步通讯。 CSP和LOTOS定义了比CCS多的算子，它们大都是CCS基本算子的变种算子，一般地说，表达能力就越强，代数变换规则就丰富。表3.1列出CCS，CSP和LOTOS所定义的算子情况。 第三章 协议模型技术 S S1 S2 C C1 C2 P P1 P2 CCS √ √ √ CSP √ √ √ √ √ √ √ LOTOS √ √ √ √ √ √ √ 三种进程代数的算子设立情况 第三章 协议模型技术 3.5.4 AB协议的CCS描述 我们仍然以AB协议为例来显示CCS在协议模型技术中的应用能力，定义下列符号（参见图3.4） /a :发送者S从A点接受用户报文，赋予顺序号，即A?m,seq→m; b: 接受者R向B点递交报文给用户，即B！m; m,/m: S向R发送报文(m),S接收报文(/m),即a!m,b?m; k,/k: R向S发送ack报文（K），S接收ack报文（/k），即b!ack,a?ack; t: S超时重发，即timeout; d: R在接收报文m之后，如果m有错误，或顺序号不对，则丢弃报文，即drop. 第三章 协议模型技术 定义上述符号之后，AB协议的发送进程S和接收进程R可分别用CCS表达式定义为： 发送进程 （1） 重发进程 （2） 接收进程 （3） 用户所看到的整个AB协议系统，它应该是S和R的并行组合，我们记作P=S|R。利用扩展规则、限止规则和隐藏规则，我们可以推导出AB协议系统作为一个进程应具备的行为。下面推导中，我们限制事件从表达式中省去限制符号“/”。 第三章 协议模型技术 第三章 协议模型技术 第三章 协议模型技术 （4）和（5）完整地描述了外部观察者所看到的AB协议行为，当它从用户接收一个报文(事件)之后，执行进程Q。（5）式的第一项和第二项表述了报文丢失重发的递归特性：报文多次丢失重发时，外部观察者所看到的行为可能先丢失(d)后重发(t)，也可能是先重发(t)后丢失(d)。（5）的第三项表明Q进程总有一次能成功地将报文递交给收端用户(b)，然后退出Q进程。(5)的第四项表明AB协议的这祥一种并发可能性：收端正准备将报文递交给用户之前，发端先从用户那里取下个报文，这样外部观察者所看到的事件顺序就是 。 第三章 协议模型技术 如果在上述推导中，我们还限制t和d的扩展，那么我们得出的AB协议系统的行为是: （6）和（5）式比较有显著差别。（6）式的第二项所描述的行为和（5）的第（4）项所描述的行为相同。然而，AB协议的丢失重发行为在（6）式中消失了。 第三章 协议模型技术 推导讨程是检测有无死锁的过程，把过多的事件列入限制范围将减少检测协议错误的能力。为了说明这一点，我们将（3）式改为： （9）式第一项说明AB协议出现死锁，第二项显示AB协议丢掉报文无重发动作（用户报文最终丢失）。（9）式中存在的错误由（7）式中的错误引起。然而，当我们在推导中把t和d也列入限制范围，那么推导出来的结果和（6）式相同，错误不能检测出来。 第三章 协议模型技术 (1),(2)和(3)所描述的AB协议没有显示地说明报文顺序的交替出现的行为。如果将AB协议系统在传送序号为“0”的报文时所执行的事件记作， 传送序号为“1”的报文时所执行的事件记作， 那么AB协议的发送端和接收端就可以定义为： 第三章 协议模型技术 第三章 协议模型技术 3.5.5 CCS的应用要点 1.协议正确性判定 从CCS的表达式可判定协议是否有活动性、安全性、一致性和完备性。为了说明这一点，我们给出一个协议的CCS描述如下： 联立递归表达式（13）中存在死