Paper Info
Title
Verification of Population Ring Protocols in PAT
Abstract
The population protocol model has emerged as an elegant paradigm for describing mobile ad hoc networks, consisting 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 eventually 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 population 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 automatically verifying population protocols. In this paper, we summarize 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.
Year
DOI
Venue
2009
10.1109/TASE.2009.51
TASE
Keywords
Field
DocType
crucial role,correct output value,global fairness,population ring protocols,process analysis toolkit,fairness constraint,different fairness constraint,self-stabilizing population protocol,population protocol model,verifying population protocol,population protocol,model checking,formal verification,leader election,mobile ad hoc networks,ad hoc networks,logic,automata,mobile ad hoc network,lead,verification,protocols,color,ring network,computer networks
Mobile ad hoc network,Leader election,Population,Model checking,Computer science,Correctness,Computer network,Population protocol,Theoretical computer science,Wireless ad hoc network,Distributed computing,Formal verification
Conference
Citations 
PageRank 
References 
8
0.53
15
Authors
4
Name
Order
Citations
PageRank
Yang Liu12194188.81
Jun Pang252130.59
Jun Sun31407120.35
Zhao Jianhua432744.13