随着计算机和网络的发展,分布式系统的应用也越来越广泛,同时对系统容错性和健壮性的要求也越来越高。分布式系统的容错性和健壮性也称为自稳定性。1974年Dijkstra首次把自稳定性的概念引入了计算机科学中[1],即系统从任何初始状态出发,总能在有限步内到达一个合法状态。自稳定系统是能够保证自稳定性的分布式系统,它的研究是计算机科学与理论中比较前沿的领域之一。自稳定算法是作用在分布式系统上的算法,它能够保证系统的容错性和健壮性。对于不同拓扑结构的分布式系统,要设计不同的自稳定算法来保证系统的自稳定性。性能好的自稳定算法需要经过复杂的正确性验证才能应用到实际中。自稳定算法的验证有多种方法,包括数学分析、定理证明、形式化分析等。形式化方法是基于数学的方法来描述目标软件系统属性的一种技术,它可以用来检测软件的可靠性和正确性。许多计算机科学家都认为,采用形式化方法对系统进行形式化验证和分析是构造可靠安全软件的一个重要途径,而原型验证系统PVS就是著名的模型检测和自动化验证工具之一。PVS为开发形式化规范和分析验证提供了一个集成化环境,它既有强有力的机器推理支持,规约语言,又有足够丰富的表达手段,为算法的形式化验证提供了很好的验证工具和证明系统。本文主要使用PVS自动验证工具对自稳定算法进行形式化分析和验证,主要的研究成果和创新如下:1.在形式化分析和验证方面,本文使用PVS自动化验证工具对自稳定算法进行形式化建模和分析验证,完善地证明了自稳定系统的基本性质并提出了一个比较系统的形式化验证方法。2.在算法的设计方面,本文的主要工作是在研究和总结前人工作的基础上,提出了自稳定算法设计的基本方法和原则。3.本文从实践的角度出发,在试验的基础上对原型验证系统PVS做了非常全面的说明和分析,并指明了PVS存在的缺陷以及需要的改进的地方。4.深入剖析和比较了形式化分析领域中各种自动化验证工具的优缺点,并提出了比较理想的自动化验证工具的设计思想和实现。5.在研究了自稳定算法在分布式系统以及通信协议中的应用的基础上,指明了今后可能的研究方向和研究课题。