面向一类基于轮数的分布式算法的状态空间分析与模型检测

发布时间：2024-07-09 03:08

　　随着信息技术的高速发展,计算机系统已经被广泛的应用于日常生活中的各个方面,比如电话通讯系统、银行系统等。这些系统大部分都需要后台运行的分布式算法来完成一些基本目标,比如分布式一致性和错误避免。这些算法的正确性和有效性对系统而言是至关重要的。然而,由于分布式算法所运行的环境复杂,算法的设计很容易出错。应用恰当的数学理论和分析方法可以增强系统的正确性和可靠性。基于模型检测的形式化方法就是这样一种技术,并已成功地在实践中应用于对复杂的时序线路设计和通信协议的正确性验证。 模型检测通过遍历系统所有可达的状态空间来验证系统是否满足特定的安全属性。当被验证的系统的状态空间非常大,甚至是无限的时候,就会导致模型检测中的状态空间爆炸问题：即在有限的时间和存储空间条件下,无法遍历系统的整个状态空间,进而无法对系统的正确性进行验证。在分布式计算领域中,存在着许多分布式算法用来解决分布式计算中的基本问题,比如领袖选举问题和一致性问题。由于这些问题没有确定性的解决方案,这些算法往往通过引入轮数来确保其能够以一定的概率完成目标,但这却导致了轮数的无界性,从而导致在应用模型检测对算法进行形式化验证时的空间爆炸问题...

【文章页数】：73 页

【学位级别】：硕士

【部分图文】：

图5.1轮数之间的距离可能会无限增加

以无限增加，从而使得算法的状态空间是无限的。为了模型检测该算法，就需要有一个对轮数的有限表示。然而，不同于Itai一Rodeh领袖选举算法，本文没有发现该算法中正确进程的轮数之间的存在一个距离的上界。下图5.1给出了该算法中轮数之间的距离无限增加的一个可能的执行。r二2…V=1-....

图5.2轮数之间的距离可能会无限增加

就需要有对轮数进行有限表示。类似于第5，1节中的BT一致性算法，本文同样没有找到该算法轮数之间的有界距离，正确进程的轮数之间的距离可以无限增加(见图5.2)。在图5.2中，进程p，停留在轮数r一1中，而其它所有进程则无限的增加轮数:在第r=1轮中，协调者pZ根据收到的消息得到这一....

本文编号：4004296