Frontiers of Computer Science

, Volume 12, Issue 4, pp 763–776 | Cite as

Probabilistic verification of hierarchical leader election protocol in dynamic systems

  • Yu Zhou
  • Nvqi Zhou
  • Tingting Han
  • Jiayi Gu
  • Weigang Wu
Research Article


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.


distributed computing hierarchical leader election protocol dynamic systems probabilistic model checking 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.



This work was supported by the Fundamental Research Funds for the Central Universities (NS2016093).

Supplementary material

11704_2018_6173_MOESM1_ESM.ppt (100 kb)
Supplementary material, approximately 99.5 KB.


  1. 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–134Google Scholar
  2. 2.
    Singh G. Leader election in the presence of link failures. IEEE Transactions on Parallel & Distributed Systems, 1996, 7(3): 231–236CrossRefGoogle Scholar
  3. 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–68Google Scholar
  4. 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–409CrossRefGoogle Scholar
  5. 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–72Google Scholar
  6. 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–118Google Scholar
  7. 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–224CrossRefGoogle Scholar
  8. 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–87Google Scholar
  9. 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–351Google Scholar
  10. 10.
    Baier C, Katoen J P. Principles of Model Checking. Cambridge: MIT Press. 2008.Google Scholar
  11. 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–113Google Scholar
  12. 12.
    Kwiatkowska M, Norman G, Parker D. Prism 4. 0: verification of probabilistic real-time systems. Lecture Notes in Computer Science. 2011, 6806: 585–591Google Scholar
  13. 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–205CrossRefGoogle Scholar
  14. 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–765CrossRefGoogle Scholar
  15. 15.
    Yang Z W, Wu WG, Chen Y S, Zhang J. Efficient information dissemination in dynamic networks. In: Proceedings of the 42nd International Conference on Parallel Processing. 2013, 603–610Google Scholar
  16. 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–37Google Scholar
  17. 17.
    Kwiatkowska M, Norman G, Parker D, Qu H Y. Compositional probabilistic verification through multi-objective model checking. Information and Computation. 2013, 232: 38–65MathSciNetCrossRefMATHGoogle Scholar
  18. 18.
    Shen J, Tan HW, 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–178Google Scholar
  19. 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–246CrossRefGoogle Scholar
  20. 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–261CrossRefGoogle Scholar
  21. 21.
    Rault T, Bouabdallah A, Challal Y. Energy efficiency in wireless sensor networks: A top-down survey. Computer Networks. 2014, 67: 104–122CrossRefGoogle Scholar
  22. 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–103Google Scholar
  23. 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–3743CrossRefGoogle Scholar
  24. 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–150CrossRefGoogle Scholar
  25. 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–123CrossRefGoogle Scholar
  26. 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–40Google Scholar
  27. 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–138Google Scholar
  28. 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–277CrossRefGoogle Scholar

Copyright information

© Higher Education Press and Springer-Verlag GmbH Germany, part of Springer Nature 2018

Authors and Affiliations

  • Yu Zhou
    • 1
    • 2
  • Nvqi Zhou
    • 1
  • Tingting Han
    • 3
  • Jiayi Gu
    • 1
  • Weigang Wu
    • 4
  1. 1.College of Computer Science and TechnologyNanjing University of Aeronautics and AstronauticsNanjingChina
  2. 2.State Key Laboratory for Novel Software TechnologyNanjing UniversityNanjingChina
  3. 3.Department of Computer Science and Information Systems, BirkbeckUniversity of LondonLondonUK
  4. 4.Department of Computer ScienceSun Yat-sen UniversityGuangzhouChina

Personalised recommendations