论文部分内容阅读
作为计算机科学理论的一个重要分支,进程演算(也称为进程代数)在并发和交互式系统的建模和验证方面有广泛的应用。与此同时,新的应用场景(比如,多核处理器和无线网络等等)带来的挑战又促进了进程演算的发展。本文在该背景下提出并研究了两种基于图的进程演算:传值树进程演算及其应用和基于图的面向无线网络的进程演算及其应用。 首先,本文研究了传值树进程演算。它使用图来定义多个进程的并发组合,这些进程位于图的不同顶点上,只有被图的边连接的那些进程才能够进行通信。为传值树进程定义了归约语义和标号迁移语义。为了研究传值树进程的行为等价关系,定义了弱barbed同余关系和弱互模拟关系,并且证明了如果两个进程是弱互模拟的那么它们是弱barbed同余的。作为传值树进程演算的应用,本文定义了一个简单的多线程程序,该程序具有原子变量操作和线程创建指令。通过将多线程程序翻译到传值树进程,为该程序语言定义了一种非线性的操作语义,并且证明了该翻译过程的正确性。本文在传值树进程演算的框架中研究了弱内存模型(weak memory models),形式化了两个弱内存模型的实例,并且证明了该形式化过程的正确性。 其次,本文重点研究了传值树进程演算的语义和行为等价关系。行为等价关系是进程演算的核心问题,弱barbed同余关系和弱互模拟关系的等价性是CCS和π-演算的重要结论。为传值树进程演算定义了一种完全抽象的(fully abstract)语义,即在满足image-finite条件的迁移系统中,弱barbed同余关系和弱互模拟关系是等价的。 最后,本文提出了一种基于图的进程演算对具有局部广播能力的无线网络进行建模和分析。在语法层面,该进程演算使用图来刻画无线网络的拓扑结构。在语义层面,为该进程演算定义了归约语义和标号迁移语义。基于前一种语义,定义了弱barbed同余关系;基于后一种语义,定义了弱互模拟关系并且突出考虑了网络中节点的位置信息和连接信息。证明了这两种语义是一致的,并且证明了如果两个网络是弱互模拟的那么它们是弱barbed同余的。不同于其他广播进程演算的行为等价关系,这里的弱互模拟关系可以详细地刻画和分析无线网络中节点的分布和连接信息。为了说明该进程演算的潜在应用,本文列举了一些例子并且对ARAN协议和Alternating Bit Protocol中的一些场景进行了建模和分析。