Probabilistic verification of hierarchical leader election protocol in dynamic systems

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

References

[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

[2] Singh G. Leader election in the presence of link failures. IEEE Transactions on Parallel & Distributed Systems, 1996, 7(3): 231–236

[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

[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

[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

[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

[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

[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

[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

[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

[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

[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

[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

[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

[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

[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

[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

[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

[21] Rault T, Bouabdallah A, Challal Y. Energy efficiency in wireless sensor networks: A top-down survey. Computer Networks. 2014, 67: 104–122

[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

[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

[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

[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

[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

[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

[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

RIGHTS & PERMISSIONS

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