Publication Type

Conference Proceeding Article

Version

publishedVersion

Publication Date

7-2009

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.

Discipline

Programming Languages and Compilers | Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

Proceedings of the 2009 Third IEEE International Symposium on Theoretical Aspects of Software Engineering, Tianjin, China, July 29-31

First Page

81

Last Page

89

ISBN

9780769537573

Identifier

10.1109/TASE.2009.51

Publisher

IEEE

City or Country

Tianjin, China

Additional URL

https://doi.org/10.1109/TASE.2009.51

Download

Share

COinS