用NuSMV验证单向异步环中的Peterson前导选举算法
Verification of Peterson's Algorithm for Leader Election in a Unidirectional Asynchronous Ring Using NuSMV
摘要：
大多数分布式算法的有限内在本质使我们能够使用模型检验工具来验证这类算法。在本文中，我试图使用NuSMV作为一个模型检验工具，验证必要的性质彼得森的领导选举问题的单向异步环形拓扑结构的算法。Peterson的异步环算法假设环中的每个节点都有一个唯一的ID和一个用于处理存储问题的队列。考虑到队列可以有任何值的组合，一个只有四个节点的环的构造模型将有超过十亿个状态。虽然似乎模型检验是不是一个可行的方法，这个问题，我试图使用几个有效的限制性假设雇用正式的模型检验的方法，而不会失去正确的功能的彼得森算法。这些强制限制假设的目标是模型检验过程中的自由度，并显着减少CPU时间，内存使用和页面错误的总数。通过部署这些限制，在NuSMV的模型检验过程中，节点数量可以从4个增加到8个。
英文摘要：
The finite intrinsic nature of the most distributed algorithms gives us this ability to use model checking tools for verification of this type of algorithms. In this paper, I attempt to use NuSMV as a model checking tool for verifying necessary properties of Peterson's algorithm for leader election problem in a unidirectional asynchronous ring topology. Peterson's algorithm for an asynchronous ring supposes that each node in the ring has a unique ID and also a queue for dealing with storage problem. By considering that the queue can have any combination of values, a constructed model for a ring with only four nodes will have more than a billion states. Although it seems that model checking is not a feasible approach for this problem, I attempt to use several effective limiting assumptions for hiring formal model checking approach without losing the correct functionality of the Peterson's algorithm. These enforced limiting assumptions target the degree of freedom in the model checking process and significantly decrease the CPU time, memory usage and the total number of page faults. By deploying these limitations, the number of nodes can be increased from four to eight in the model checking process with NuSMV.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
