Probabilistic verification of hierarchical leader election protocol in dynamic systems

doi:10.1007/s11704-018-6173-6

Front. Comput. Sci.

2018, Vol. 12

Issue (4) : 763-776 https://doi.org/10.1007/s11704-018-6173-6

RESEARCH ARTICLE

Probabilistic verification of hierarchical leader election protocol in dynamic systems

Yu ZHOU^1,²(

), Nvqi ZHOU¹, Tingting HAN³, Jiayi GU¹, Weigang WU⁴

¹. College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing 210016, China
². State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing 210093, China
³. Department of Computer Science and Information Systems, Birkbeck, University of London, LondonWC1E 7HX, UK
⁴. Department of Computer Science, Sun Yat-sen University, Guangzhou 510006, China

Download: PDF(693 KB)
Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks

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

Cite this article:

Yu ZHOU,Nvqi ZHOU,Tingting HAN, et al. Probabilistic verification of hierarchical leader election protocol in dynamic systems[J]. Front. Comput. Sci., 2018, 12(4): 763-776.

URL:

https://academic.hep.com.cn/fcs/EN/10.1007/s11704-018-6173-6
https://academic.hep.com.cn/fcs/EN/Y2018/V12/I4/763

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

[1]	Wenjie LIU, Zhanhuai LI. An efficient parallel algorithm of N-hop neighborhoods on graphs in distributed environment[J]. Front. Comput. Sci., 2019, 13(6): 1309-1325.
[2]	Shuai MA,Jia LI,Chunming HU,Xuelian LIN,Jinpeng HUAI. Big graph search: challenges and techniques[J]. Front. Comput. Sci., 2016, 10(3): 387-398.
[3]	Qinma KANG, Hong HE. Task assignment for minimizing application completion time using honeybee mating optimization[J]. Front Comput Sci, 2013, 7(3): 404-415.
[4]	Ying ZHANG, Gang HUANG, Wei ZHANG, Xuanzhe LIU, Hong MEI. Towards module-based automatic partitioning of Java applications[J]. Front Comput Sci, 2012, 6(6): 725-740.

Viewed

Full text

Abstract

Cited

Shared

Discussed