Verification of Population Ring Protocols in PAT
The population protocol model has emerged as an ele gant paradigm for describing mobile ad hoc networks, con sisting of a number of nodes that interact with each other to carry out a computation. One essential property of self stabilizing population protocols is that all nodes must even tually converge to the correct output value, with respect to all possible initial configurations. It has been shown that fairness constraints play a crucial role in designing popula tion protocols. The Process Analysis Toolkit (PAT) has been developed to perform verifications under different fairness constraints efficiently. In particular, it can handle global fairness, which is required for the correctness of most of population protocols. It is an ideal candidate for automati cally verifying population protocols. In this paper, we sum marize our latest empirical evaluation of PAT on a set of self-stabilizing population protocols for ring networks. We report one previously unknown bug in a protocol for leader election identified using PAT.
Yang Liu Jun Pang Jun Sun Jianhua Zhao
National University of Singapore School of Computing Université du Luxembourg Faculté des Sciences de la Technologie et de la Communication Nanjing University State Key Laboratory of Novel Software Technology
国际会议
天津
英文
81-89
2009-07-29（万方平台首次上网日期，不代表论文的发表时间）