Please use this identifier to cite or link to this item:
|Title:||Verification of population ring protocols in PAT|
|Authors:||Liu, Y. |
|Source:||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. https://doi.org/10.1109/TASE.2009.51|
|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|
|Appears in Collections:||Staff Publications|
Show full item record
Files in This Item:
There are no files associated with this item.
checked on Dec 14, 2017
WEB OF SCIENCETM
checked on Nov 19, 2017
checked on Dec 17, 2017
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.