|
|
|
On automatic verification of self-stabilizing
population protocols |
| PANG Jun1, LUO Zhengqin2, DENG Yuxin2 |
| 1.Department of Computer Science and Communications, Université du Luxembourg；State Key Laboratory of Novel Software Technology, Nanjing University; 2.Department of Computer Science and Engineering, Shanghai Jiao Tong University; 3.2008-12-11 13:56:58 |
|
|
|
|
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 constraint. One essential property of population protocols is that all nodes must eventually converge to the correct output 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.
|
|
Issue Date: 05 December 2008
|
|
| 1 |
Fuzzati R . Merro M, Nestmann U . Distributed consensus, revisited. Acta Informatica, 2007, 44(6): 377–425.
doi:10.1007/s00236-007-0052-1
|
| 2 |
Chandra T D . Toueg S . Unreliable failure detectorfor reliable distributed systems. Journalof the ACM, 1996, 43(2): 225–267.
doi:10.1145/226643.226647
|
| 3 |
Holzmann G J . The model checker Spin. IEEE Transactionson Software Engineering, 1997, 23(5): 279–295.
doi:10.1109/32.588521
|
| 4 |
Aspnes J . Ruppert E . An introduction to populationprotocols. Bulletin of the European Associationfor Theoretical Computer Science, Distributed Computing Column, 2007, 93: 98–117
|
| 5 |
Attie P C . Francez N, Grumberg O . Fairness and hyperfairness in multi-party interactions. Distributed Computing, 1993, 6: 245–254.
doi:10.1007/BF02242712
|
| 6 |
Lamport L . Fairnessand hyperfairness. Distributed Computing, 2000, 13(4): 239–245.
doi:10.1007/PL00008921
|
| 7 |
Völzer H . Varacca D, Kindler E . Defining fairness. In: Proceedingsof the 14th Conference on Concurrency Theory. Berlin: Springer, 2005, 3653: 458–472
|
| 8 |
Völzer H . Onconspiracies and hyperfairness in distributed computing. In: Proceedings of the 19th Conference on DistributedComputing. Berlin: Springer, 2005, 3724 : 33–47
|
| 9 |
Corradini F . Di Berardini M, Vogler W . Checking a mutex algorithm in a process algebra withfairness. In: Proceedings of the 15th Conferenceon Concurrency Theory. Berlin: Springer, 2006, 4137: 142–157
|
| 10 |
Fischer M J . Jiang H . Self-stabilizing leader electionin networks of finite-state anonymous agents. In: Proceedings of the 10th Conference on Principles of Distributed Systems. Berlin: Springer, 2006, 4305: 395–409
|
| 11 |
Angluin D . Aspnes J, Fischer M J, Jiang H . Selfstabilizingpopulation protocols. In: Proceedings ofthe 9th Conference on Principles of Distributed Systems. Berlin: Springer, 2005, 3974: 103–117
|
| 12 |
Holzmann G J . On-the-fly, LTL model checking with spin. http://spinroot.com
|
| 13 |
Holzmann G J . The spin model checker: Primer and reference manual. Addison-Wesley, 2003
|
| 14 |
Dijkstra E W . Self-stabilizing systems in spite of distributed control. Communications of the ACM, 1974, 17(11): 643–644.
doi:10.1145/361179.361202
|
| 15 |
Luo Z Q . Pang J, Deng Y X . Promela source codes of self-stabilizing population protocols. http://basics.sjtu.edu.cn/∼zhengqin/population
|
| 16 |
Jiang H . Distributedsystems of simple interacting agents. YaleUniversity, 2007
|
| 17 |
Hammer M . Knapp A, Merz S . Truly on-the-fly LTL model checking. In: Proceedings of the 11th Conference on Tools and Algorithms for theConstruction and Analysis of Systems. Berlin: Springer, 2005, 3440: 191–205
|
| 18 |
Fokkink W J . Hoepman J H, Pang J . A note on K-stateself-stabilization in a ring with K = N. Nordic Journal of Computing, 2005, 12(1): 18–26
|
|
Viewed |
|
|
|
Full text
|
|
|
|
|
Abstract
|
|
|
|
|
Cited |
|
|
|
|
| |
Shared |
|
|
|
|
| |
Discussed |
|
|
|
|
