基于PVS的自稳定算法形式化分析

发布时间：2020-10-16 17:18

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

任务能够由一个进程或者一个线程实现。图中的分布式应用程序有三分组成，尽管程序 3 的任务 A 和任务 D 在相同的计算机上，但是它们；因为它们由两个分离的处理器执行。并行程序中的任务比分布式程序合得更紧密，通常与分布式程序关联的处理器在不同的计算机上，但是关联的处理器在相同的计算机上。

学位论文 第三章 自稳定算法的，我们将给出具体的证明。同时我们可以证明，整个算法需定状态，具体的证明可以参考[9]。ijkstra在 1974年的同一篇文章中提出了另外两个自稳定算法，算法和三状态自稳定算法，具体在这里就不介绍了，可以参 提出的这三个自稳定算法虽然比较简单，但是作为自稳定性这些算法得到广大学者的一致性认同，并被后来的很多学者。

SPIN模拟和检验的基本过程
【参考文献】

相关期刊论文 前2条

1 郑红军;张乃孝;;软件开发中的形式化方法[J];计算机科学;1997年06期

2 廖宇,杨大军;定理证明辅助工具PVS剖析[J];计算机工程;2000年09期

本文编号：2843544