π-演算交互式验证工具的研究与实现

作     者：杜旭涛 

作者单位：国防科学技术大学 

学位级别：硕士

导师姓名：李舟军

授予年度：2002年

学科分类：08[工学] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

主      题：π-演算 验证工具 唯一不动点归纳法 证明系统 AB协议 

摘      要：随着计算机技术的发展，并发系统的重要性越来越显著。如何保证并发系统的正确性成为一个重要的课题。 进程代数在对并发系统的分析和验证等方面获得了广泛应用。π-演算是进程代数的典型代表，它可以描述那些通信拓扑结构会动态变化的系统。 作为一种形式化方法，使用π-演算对大型系统的证明过程往往很长并且容易出现错误，所以，机器的支持与协助就相当必要。我们的工作就是为π-演算设计并实现第一个交互式的验证工具PiM(the Pi-calculus Manipulator)。主要工作和成果包括如下三个方面： 首先，为了处理递归，我们对Lin给出的适合于理论研究的唯一不动点归纳法进行了扩展，得到了所需要的适合于应用的一般化的版本。我们证明了原有的关于强互模拟的公理系统加上我们这个版本的唯一不动点归纳法后的可靠性和完备性。 然后，以Lin的关于迟／早互模拟的证明系统和Li的关于开互模拟的证明系统为理论基础，我们实现了π-演算的第一个交互式验证工具-PiM。我们还实现了自己版本的唯一不动点归纳法。 最后，我们使用PiM验证了网络AB协议。在这项工作过程中，我们发现了***的著作“Communication and Concurrency中的一个有关AB协议的错误。 上述结果中的有关唯一不动点归纳法的研究具有重要的理论意义，验证工具PiM具有明确的应用价值，而对AB协议的验证及***的著作中一个错误的发现更是我们工作的价值的体现。