使用NuSMV验证单向异步环中领导者选举的Peterson算法

大多数分布式算法的有限内在特性使我们能够使用模型检验工具来验证这类算法。在本文中，我尝试使用NuSMV作为模型检验工具，来验证单向异步环拓扑中领导者选举问题的Peterson算法的必要性质。用于异步环的Peterson算法假设环中每个节点都有一个唯一的ID，以及一个用于处理存储问题的队列。考虑到队列可以有任何值的组合，一个仅包含四个节点的环的构建模型将拥有超过十亿个状态。尽管模型检验似乎不是解决此问题的可行方法，但我尝试使用几个有效的限制性假设来采用形式化模型检验方法，同时不损失Peterson算法的正确功能。这些强加的限制性假设针对模型检验过程中的自由度，并显著减少了CPU时间、内存使用和总缺页次数。通过部署这些限制，在NuSMV的模型检验过程中，节点数可以从四个增加到八个。