随着信息技术的高速发展,计算机系统已经被广泛的应用于日常生活中的各个方面,比如电话通讯系统、银行系统等。这些系统大部分都需要后台运行的分布式算法来完成一些基本目标,比如分布式一致性和错误避免。这些算法的正确性和有效性对系统而言是至关重要的。然而,由于分布式算法所运行的环境复杂,算法的设计很容易出错。应用恰当的数学理论和分析方法可以增强系统的正确性和可靠性。基于模型检测的形式化方法就是这样一种技术,并已成功地在实践中应用于对复杂的时序线路设计和通信协议的正确性验证。模型检测通过遍历系统所有可达的状态空间来验证系统是否满足特定的安全属性。当被验证的系统的状态空间非常大,甚至是无限的时候,就会导致模型检测中的状态空间爆炸问题：即在有限的时间和存储空间条件下,无法遍历系统的整个状态空间,进而无法对系统的正确性进行验证。在分布式计算领域中,存在着许多分布式算法用来解决分布式计算中的基本问题,比如领袖选举问题和一致性问题。由于这些问题没有确定性的解决方案,这些算法往往通过引入轮数来确保其能够以一定的概率完成目标,但这却导致了轮数的无界性,从而导致在应用模型检测对算法进行形式化验证时的空间爆炸问题。本文的目标就是针对这一类基于轮数的分布式算法,通过处理这类算法的状态空间爆炸问题来使用模型检测来对这类算法进行形式化验证。本文通过分析轮数之间的相互关系,发现虽然算法的轮数可以无限增加,然而轮数之间的距离却是有界的。基于这一发现本文提出了一种对这类算法进行模型检测的方法,通过维护轮数之间的相对关系来对轮数进行表示,从而采用一种有限的表示方法来等价的对无界轮数进行表示,而不是对算法中的轮数直接进行表示。这样就可以把算法的状态空间表示为有限的,从而使这类算法的自动化验证成为可能。同时文中也对这一方法的可行性进行了形式化的证明。本文将这一方法应用到了两个领袖选举算法(包括文中新提出的一个领袖选举算法)和两个分布式一致性算法中。以下是本文所专注的四个算法以及主要的理论结果：1) Itai-Rodeh领袖选举算法：在该算法的运行过程中,活动进程的轮数之间的距离最多为1；2)一个本文新提出的领袖选举算法：在该算法中,活动进程之间的轮数之间的距离最多为n-1；3)由Bracha和Toueg提出的一个概率一致性算法：当只有一个进程可以崩溃时,在某个进程决定之前,所有正确进程的轮数之间的距离最多为3；4)一个包含故障检测器的轮转协调者算法：当只有一个进程可以崩溃时,在某个进程决定之前,所有正确进程的轮数之间的距离最多为2n。对于上述算法,本文首先对算法中轮数之间的相互关系进行分析,从而找出算法中轮数之间的距离范围,并给出所得到结果的理论分析和数学证明；然后,据此对算法进行转化,从而将算法的状态空间转换为有限；最后,使用模型检测器Spin来对它们进行验证。