Please use this identifier to cite or link to this item:
Title: Verification of population ring protocols in PAT
Authors: Liu, Y. 
Pang, J.
Sun, J. 
Zhao, J.
Issue Date: 2009
Citation: Liu, Y., Pang, J., Sun, J., Zhao, J. (2009). Verification of population ring protocols in PAT. Proceedings - 2009 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2009 : 81-89. ScholarBank@NUS Repository.
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. © 2009 IEEE.
Source Title: Proceedings - 2009 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2009
ISBN: 9780769537573
DOI: 10.1109/TASE.2009.51
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.


checked on Feb 13, 2019


checked on Feb 13, 2019

Page view(s)

checked on Feb 2, 2019

Google ScholarTM



Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.