Verification of population ring protocols in PAT
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...
Saved in:
Main Authors: | , , , |
---|---|
Format: | text |
Language: | English |
Published: |
Institutional Knowledge at Singapore Management University
2009
|
Subjects: | |
Online Access: | https://ink.library.smu.edu.sg/sis_research/5044 https://ink.library.smu.edu.sg/context/sis_research/article/6047/viewcontent/veri_of_popu.pdf |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
Institution: | Singapore Management University |
Language: | English |
id |
sg-smu-ink.sis_research-6047 |
---|---|
record_format |
dspace |
spelling |
sg-smu-ink.sis_research-60472020-03-12T08:13:13Z Verification of population ring protocols in PAT LIU, Yang PANG, Jun SUN, Jun ZHAO, Jianhua 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-07-01T07:00:00Z text application/pdf https://ink.library.smu.edu.sg/sis_research/5044 info:doi/10.1109/TASE.2009.51 https://ink.library.smu.edu.sg/context/sis_research/article/6047/viewcontent/veri_of_popu.pdf http://creativecommons.org/licenses/by-nc-nd/4.0/ Research Collection School Of Computing and Information Systems eng Institutional Knowledge at Singapore Management University Programming Languages and Compilers Software Engineering |
institution |
Singapore Management University |
building |
SMU Libraries |
continent |
Asia |
country |
Singapore Singapore |
content_provider |
SMU Libraries |
collection |
InK@SMU |
language |
English |
topic |
Programming Languages and Compilers Software Engineering |
spellingShingle |
Programming Languages and Compilers Software Engineering LIU, Yang PANG, Jun SUN, Jun ZHAO, Jianhua Verification of population ring protocols in PAT |
description |
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. |
format |
text |
author |
LIU, Yang PANG, Jun SUN, Jun ZHAO, Jianhua |
author_facet |
LIU, Yang PANG, Jun SUN, Jun ZHAO, Jianhua |
author_sort |
LIU, Yang |
title |
Verification of population ring protocols in PAT |
title_short |
Verification of population ring protocols in PAT |
title_full |
Verification of population ring protocols in PAT |
title_fullStr |
Verification of population ring protocols in PAT |
title_full_unstemmed |
Verification of population ring protocols in PAT |
title_sort |
verification of population ring protocols in pat |
publisher |
Institutional Knowledge at Singapore Management University |
publishDate |
2009 |
url |
https://ink.library.smu.edu.sg/sis_research/5044 https://ink.library.smu.edu.sg/context/sis_research/article/6047/viewcontent/veri_of_popu.pdf |
_version_ |
1770575198212325376 |