标题：Model Checking Round-Based Distributed Algorithms
作者：An, Xin; Pang, Jun
作者机构：[An, Xin] Shandong Univ, Sch Comp Sci & Technol, Jinan 250101, Shandong, Peoples R China.; [Pang, Jun] Univ Luxembourg, Comp Sci & Commun, 6 Rue Ric 更多
会议名称：15th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS)
会议日期：MAR 22-26, 2010
来源：2010 15TH IEEE INTERNATIONAL CONFERENCE ON ENGINEERING OF COMPLEX COMPUTER SYSTEMS (ICECCS 2010)
摘要：In the field of distributed computing, there are many round-based algorithms to solve fundamental problems, such as leader election and distributed consensus. Due to the nature of these algorithms, round numbers are unbounded and can increase infinitely during executions of the algorithms. This can lead to the state space explosion problem when verifying correctness of these algorithms using model checking.; In this paper, we present a general idea of investigating the bounded distance of round numbers in round-based algorithms. We can manage to transform their state spaces into finite by maintaining such relations in a proper way, and thus make automatic verification of these algorithms possible. We apply this idea to several algorithms and present their verification results in the model checker Spin.