|
|
Probabilistic verification of hierarchical leader election protocol in dynamic systems |
Yu ZHOU1,2( ), Nvqi ZHOU1, Tingting HAN3, Jiayi GU1, Weigang WU4 |
1. College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing 210016, China 2. State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing 210093, China 3. Department of Computer Science and Information Systems, Birkbeck, University of London, LondonWC1E 7HX, UK 4. Department of Computer Science, Sun Yat-sen University, Guangzhou 510006, China |
|
|
Abstract Leader election protocols are fundamental for coordination problems—such as consensus—in distributed computing. Recently, hierarchical leader election protocols have been proposed for dynamic systems where processes can dynamically join and leave, and no process has global information. However, quantitative analysis of such protocols is generally lacking. In this paper, we present a probabilistic model checking based approach to verify quantitative properties of these protocols. Particularly, we employ the compositional technique in the style of assume-guarantee reasoning such that the sub-protocols for each of the two layers are verified separately and the correctness of the whole protocol is guaranteed by the assume-guarantee rules. Moreover, within this framework we also augment the proposed model with additional features such as rewards. This allows the analysis of time or energy consumption of the protocol. Experiments have been conducted to demonstrate the effectiveness of our approach.
|
Keywords
distributed computing
hierarchical leader election protocol
dynamic systems
probabilistic model checking
|
Corresponding Author(s):
Yu ZHOU
|
Just Accepted Date: 27 December 2017
Online First Date: 20 March 2018
Issue Date: 14 June 2018
|
|
1 |
Tucci-Piergiovanni S, Baldoni R. Eventual leader election in infinite arrival message-passing system model with bounded concurrency. In: Proceedings of European Dependable Computing Conference (EDCC). 2010, 127–134
https://doi.org/10.1109/EDCC.2010.24
|
2 |
Singh G. Leader election in the presence of link failures. IEEE Transactions on Parallel & Distributed Systems, 1996, 7(3): 231–236
https://doi.org/10.1109/71.491576
|
3 |
Nakano K, Olariu S. A survey on leader election protocols for radio networks. In: Proceedings of International Symposium on Parallel Architectures, Algorithms and Networks. 2002, 63–68
https://doi.org/10.1109/ISPAN.2002.1004263
|
4 |
Fischer M, Jiang H. Self-stabilizing leader election in networks of finite-state anonymous agents. In: Proceedings of the 10th International Conference on Principles of Distributed Systems. 2006, 395–409
https://doi.org/10.1007/11945529_28
|
5 |
Bakhshi R, Fokkink W, Pang J, Van De Pol J. Leader election in anonymous rings: Franklin goes probabilistic. In: Proceedings of the 5th IFIP International Conference on Theoretical Computer Science–Tcs. 2008, 57–72
https://doi.org/10.1007/978-0-387-09680-3_4
|
6 |
Mostefaoui A, Raynal M, Travers C, Patterson S, Agrawal D, Abbadi A. From static distributed systems to dynamic systems. In: Proceedings of the 24th IEEE Symposium on Reliable Distributed Systems. 2005, 109–118
https://doi.org/10.1109/RELDIS.2005.19
|
7 |
Larrea M, Raynal M, Soraluze I, Cortiñas R. Specifying and implementing an eventual leader service for dynamic systems. International Journal of Web and Grid Services. 2012, 8(3): 204–224
https://doi.org/10.1504/IJWGS.2012.049167
|
8 |
Gómez-Calzado C, Lafuente A, Larrea M, Raynal M. Fault-tolerant leader election in mobile dynamic distributed systems. In: Proceedings of the 19th Pacific Rim International Symposium on Dependable Computing. 2013, 78–87
https://doi.org/10.1109/PRDC.2013.17
|
9 |
Li H G, Wu W G, Zhou Y. Hierarchical eventual leader election for dynamic systems. In: Proceedings of International Conference on Algorithms and Architectures for Parallel Processing. 2014, 338–351
https://doi.org/10.1007/978-3-319-11197-1_26
|
10 |
Baier C, Katoen J P. Principles of Model Checking. Cambridge: MIT Press. 2008.
|
11 |
Forejt V, Kwiatkowska M, Norman G, Parker D. Automated verification techniques for probabilistic systems. In: Bernardo M, Issarny V, eds. Formal Methods for the Design of Computer, Communication and Software Systems. Springer International Publishing, 2011, 53–113
https://doi.org/10.1007/978-3-642-21455-4_3
|
12 |
Kwiatkowska M, Norman G, Parker D. Prism 4.0: verification of probabilistic real-time systems. Lecture Notes in Computer Science. 2011, 6806: 585–591
https://doi.org/10.1007/978-3-642-22110-1_47
|
13 |
Gu J Y, Zhou Y, Chen T L, Wu W G. Analyzing eventual leader election protocols for dynamic systems by probabilistic model checking. In: Proceedings of International Conference on Cloud Computing and Security. 2015, 192–205
https://doi.org/10.1007/978-3-319-27051-7_17
|
14 |
Wu W G, Cao J N, Raynal M. Eventual clusterer: a modular approach to designing hierarchical consensus protocols in manets. IEEE Transactions on Parallel and Distributed Systems. 2009, 20(6): 753–765
https://doi.org/10.1109/TPDS.2008.266
|
15 |
Yang Z W, Wu W G, Chen Y S, Zhang J. Efficient information dissemination in dynamic networks. In: Proceedings of the 42nd International Conference on Parallel Processing. 2013, 603–610
https://doi.org/10.1109/ICPP.2013.74
|
16 |
Kwiatkowska M, Norman G, Parker D, Qu H Y. Assume-guarantee verification for probabilistic systems. In: Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2010, 23–37
https://doi.org/10.1007/978-3-642-12002-2_3
|
17 |
Kwiatkowska M, Norman G, Parker D, Qu H Y. Compositional probabilistic verification through multi-objective model checking. Information and Computation. 2013, 232: 38–65
https://doi.org/10.1016/j.ic.2013.10.001
|
18 |
Shen J, Tan H W, Wang J, Wang J W, Lee S Y. A novel routing protocol providing good transmission reliability in underwater sensor networks. Journal of Internet Technology. 2015, 16(1): 171–178
|
19 |
Xie S D, Wang Y X. Construction of tree network with limited delivery latency in homogeneous wireless sensor networks. Wireless Personal Communications. 2014, 78(1): 231–246
https://doi.org/10.1007/s11277-014-1748-5
|
20 |
Yue H D, Katoen J P. Leader election in anonymous radio networks: model checking energy consumption. In: Proceedings of International Conference on Analytical and Stochastic Modeling Techniques and Applications. 2010, 247–261
https://doi.org/10.1007/978-3-642-13568-2_18
|
21 |
Rault T, Bouabdallah A, Challal Y. Energy efficiency in wireless sensor networks: A top-down survey. Computer Networks. 2014, 67: 104–122
https://doi.org/10.1016/j.comnet.2014.03.027
|
22 |
Gupta I, Van Renesse R, Birman K P. A probabilistically correct leader election protocol for large groups. In: Proceedings of International Symposium on Distributed Computing. 2000, 89–103
https://doi.org/10.1007/3-540-40026-5_6
|
23 |
Jiménez E, Arévalo V E, Herrera C, Tang J. Eventual election of multiple leaders for solving consensus in anonymous systems. The Journal of Supercomputing. 2015, 71(10): 3726–3743
https://doi.org/10.1007/s11227-015-1460-6
|
24 |
Duflot M, Kwiatkowska M, Norman G, Parker D, Peyronnet D, Picaronny C, Sproston J. Practical applications of probabilistic model checking to communication protocols. In: Gnesi S, Margaria T, eds. Formal Methods for Industrial Critical Systems: A Survey of Applications. Wiley, 2012, 133–150
https://doi.org/10.1002/9781118459898.ch7
|
25 |
Baier C, Dubslaff C, Klein J, Klüppelholz S, Wunderlich S. Probabilistic model checking for energy-utility analysis. In: van Breugel F, Kashefi E, Palamidessi C, et al, eds. Horizons of the Mind. A Tribute to Prakash Panangaden. Springer International Publishing, 2014, 96–123
https://doi.org/10.1007/978-3-319-06880-0_5
|
26 |
Naskos A, Stachtiari E, Gounaris A, Katsaros P, Tsoumakos D, Konstantinou I, Sioutas S. Dependable horizontal scaling based on probabilistic model checking. In: Proceedings of the 15th IEEE/ACM International Symposium on Cluster, Cloud and Grid Computing. 2015, 31–40
https://doi.org/10.1109/CCGrid.2015.91
|
27 |
He K L, Zhang M, He J, Chen Y X. Probabilistic model checking of pipe protocol. In: Proceedings of International Symposium on Theoretical Aspects of Software Engineering. 2015, 135–138
https://doi.org/10.1109/TASE.2015.15
|
28 |
Zhang F L, Bu L, Wang L Z, Zhao J H, Chen X, Zhang T, Li X D. Modeling and evaluation of wireless sensor network protocols by stochastic timed automata. Electronic Notes in Theoretical Computer Science. 2013, 296: 261–277
https://doi.org/10.1016/j.entcs.2013.09.001
|
|
Viewed |
|
|
|
Full text
|
|
|
|
|
Abstract
|
|
|
|
|
Cited |
|
|
|
|
|
Shared |
|
|
|
|
|
Discussed |
|
|
|
|