RESEARCH ARTICLE
On automatic verification of self-stabilizing population
protocols
Jun PANG
1,2
, Zhengqin LUO
3
, Yuxin DENG (*)
3
1 Department of Computer Science and Communications, Universite´ du Luxembourg, Luxembourg 1359, Luxembourg
2 State Key Laboratory of Novel Software Technology, Nanjing University, Nanjing 210093, China
3 Department of Computer Science and Engineering, Shanghai Jiao Tong University, Shanghai 200240, China
E
Higher Education Press and Springer-Verlag 2008
Abstract The population protocol model has emerged as
an elegant computation paradigm for describing mobile
ad hoc networks, consisting of a number of mobile nodes
that interact with each other to carry out a computation.
The interactions of nodes are subject to a fairness con-
straint. One essential property of population protocols is
that all nodes must eventually converge to the correct out-
put value (or configuration). In this paper, we aim to
automatically verify self-stabilizing population protocols
for leader election and token circulation in the Spin model
checker. We report our verification results and discuss the
issue of modeling strong fairness constraints in Spin.
Keywords distributed algorithms, model checking,
population protocols, verification
1 Introduction
The field of distributed algorithms has enjoyed a rapid
growth in the last two decades, due to the world-wide
development and usage of mobile ad hoc networks. A
great number of algorithms have been invented to solve
hard problems in mobile ad hoc networks. However, these
algorithms are only accessible to the distributed algo-
rithms community, since their specifications and correct-
ness arguments are often given at an informal level. This is
insufficient to convince researchers outside the field of the
validity of the arguments. If one wants to verify the cor-
rectness of some proofs, he has to prove substantial parts
or entire sub-results, for whi ch only informal arguments
were given. This has been observed and illustrated in a
recent paper [1] on formal reasoning about the correctness
of a distributed consensus algorithm [2].
The last two decades have also seen an impressive
amount of new techniques developed in the area of formal
verification or model checking in particular. Model check-
ing first builds a finite state space of a formal model of a
system, and then verifies if a property, written in some
temporal logic, about the system holds or not through
an explicit state space search. Due to the finiteness of
the state space, the search always terminates. Hence,
model checking is largely automatic. It can produce an
answer in a few minutes or even seconds for many models.
A counterexample can be generated when the checked
property fails to hold, which details why the formal model
doesn’t satisfy the property. Model checkers usually face a
combinatorial blow up of the state-space, known as the
state explosion problem. Techniques such as symbolic
representation, symmetry reduction, and predicate
abstraction, have been developed to deal with the state
explosion problem and enhance the scalability of model
checking. However, these techniques have not yet made
impact on distributed algorithms, mainly because there
have not yet been enough examples of non-trivial practical
applications.
Clearly, both two fields, distributed algorithms vs. for-
mal verification, can benefit from each other. On the one
hand, formal verification can offer techniques to well-
understand distributed algorithms. On the other hand,
distributed algorithms can offer challenging examples to
formal verification.
In this pap er, we aim to automatically verify self-
stabilizing population protocols for leader election and
token circulation in the Spin model checker [3]. The popu-
lation protocol model [4] has emerged as a new elegant
computation paradigm for describing mobile ad hoc net-
works, consisting of a number of mobile nodes that inter-
act with each other to carry out a computation. Each node
has only a few stat es. One essential property of suc h pro-
tocols is that all nodes must eventually converge to the
correct output value (or configuration), which is a typical
Received July 19, 2008; accepted October 8, 2008
E-mail: jun.pang@uni.lu, {martyluo, yuxindeng}@sjtu.edu.cn
Front. Comput. Sci. China 2008, 2(4): 357–367
DOI 10.1007/s11704-008-0040-9
剩余10页未读，继续阅读
资源评论
weixin_38694800
- 粉丝: 4
- 资源: 1021
