Advertisement

Analyzing Eventual Leader Election Protocols for Dynamic Systems by Probabilistic Model Checking

  • Jiayi Gu
  • Yu Zhou
  • Weigang Wu
  • Taolue Chen
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9483)

Abstract

Leader election protocols have been intensively studied in distributed computing, mostly in the static setting. However, it remains a challenge to design and analyze these protocols in the dynamic setting, due to its high uncertainty, where typical properties include the average steps of electing a leader eventually, the scalability etc. In this paper, we propose a novel model-based approach for analyzing leader election protocols of dynamic systems based on probabilistic model checking. In particular, we employ a leading probabilistic model checker, PRISM, to simulate representative protocol executions. We also relax the assumptions of the original model to cover unreliable channels which requires the introduction of probability to our model. The experiments confirm the feasibility of our approach.

Keywords

Dynamic systems Verification Leader election Probabilistic model checking 

Notes

Acknowledgements

The work was partially funded by the NSF of China under grant No.61202002, No.61379157 and the Collaborative Innovation Center of Novel Software Technology and Industrialization.

References

  1. 1.
    Yang, Z.W., Wu, W.G., Chen, Y.S., Zhang, J.: Efficient information dissemination in dynamic networks. In: 2013 42nd International Conference on Parallel Processing, pp. 603–610 (2013)Google Scholar
  2. 2.
    Mostefaoui, A., Raynal, M., Travers, C., Patterson, S., Agrawal, D., Abbadi, A.E.: From static distributed systems to dynamic systems. In: Proceedings of the 24th Symposium on Reliable Distributed Systems (SRDS05), IEEE Computer, pp. 109–118 (2005)Google Scholar
  3. 3.
    Li, H., Wu, W., Zhou, Yu.: Hierarchical eventual leader election for dynamic systems. In: Sun, X.-h., Qu, W., et al. (eds.) ICA3PP 2014, Part I. LNCS, vol. 8630, pp. 338–351. Springer, Heidelberg (2014)Google Scholar
  4. 4.
    Chen, S., Billings, S.A.: Neural networks for nonlinear dynamic system modelling and identification. Int. J. Control 56(2), 319–346 (1992)zbMATHMathSciNetCrossRefGoogle Scholar
  5. 5.
    Merritt, M., Taubenfeld, G.: Computing with infinitely many processes. In: Herlihy, M.P. (ed.) DISC 2000. LNCS, vol. 1914, pp. 164–178. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  6. 6.
    Guerraoui, R., Hurfin, M., Mostéfaoui, A., Oliveira, R., Raynal, M., Schiper, A.: Consensus in asynchronous distributed systems: a concise guided tour. In: Krakowiak, S., Shrivastava, S.K. (eds.) BROADCAST 1999. LNCS, vol. 1752, pp. 33–47. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  7. 7.
    Jha, S.K., Clarke, E.M., Langmead, C.J., Legay, A., Platzer, A., Zuliani, P.: A bayesian approach to model checking biological systems. In: Degano, P., Gorrieri, R. (eds.) CMSB 2009. LNCS, vol. 5688, pp. 218–234. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  8. 8.
    Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70–87. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  9. 9.
    Kwiatkowska, M., Norman, G., Parker, D.: PRISM: probabilistic symbolic model checker. In: Field, T., Harrison, P.G., Bradley, J., Harder, U. (eds.) TOOLS 2002. LNCS, vol. 2324, pp. 200–204. Springer, Heidelberg (2002)Google Scholar
  10. 10.
    Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  11. 11.
    Zhou, R.F., Hwang, K.: Powertrust: A robust and scalable reputation system for trusted peer-to-peer computing. IEEE Trans. Parallel Distrib. Syst. 18(4), 460–473 (2007)CrossRefGoogle Scholar
  12. 12.
    Vaze, R., Heath, R.W.: Transmission capacity of ad-hoc networks with multiple antennas using transmit stream adaptation and interference cancellation. IEEE Trans. Inf. Theory 58(2), 780–792 (2012)MathSciNetCrossRefGoogle Scholar
  13. 13.
    Aguilera, M.K.: A pleasant stroll through the land of infinitely many creatures. ACM Sigact News 2, 36–59 (2004)CrossRefGoogle Scholar
  14. 14.
    Gupta, I., van Renesse, R., Birman, K.P.: A probabilistically correct leader election protocol for large groups. In: Herlihy, M.P. (ed.) DISC 2000. LNCS, vol. 1914, pp. 89–103. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  15. 15.
    Mostefaoui, A., Raynal, M., Travers, C.: Crash-resilient time-free eventual leadership. In: Proceedings of the 23rd IEEE International Symposium on Reliable Distributed Systems, 2004, pp.208–217. IEEE (2004)Google Scholar
  16. 16.
    Bordim, J.L., Ito, Y., Nakano, K.: Randomized leader election protocols in noisy radio networks with a single transceiver. In: Guo, M., Yang, L.T., Di Martino, B., Zima, H.P., Dongarra, J., Tang, F. (eds.) ISPA 2006. LNCS, vol. 4330, pp. 246–256. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  17. 17.
    Larrea, M., Raynal, M.: Specifying and implementing an eventual leader service for dynamic systems. In: 2011 14th International Conference on Network-Based Information Systems (NBiS), pp. 243–249 (2011)Google Scholar
  18. 18.
    Havelund, K., Skou, A., Larsen, K.G., Lund, K.: Formal modeling and analysis of an audio/video protocol: an industrial case study using uppaal. In: IEEE 18th Real-Time Systems Symposium, 2p (1997)Google Scholar
  19. 19.
    Yue, H., Katoen, J.-P.: Leader election in anonymous radio networks: model checking energy consumption. In: Al-Begain, K., Fiems, D., Knottenbelt, W.J. (eds.) ASMTA 2010. LNCS, vol. 6148, pp. 247–261. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  20. 20.
    Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  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 ScienceSun Yat-sen UniversityGuangzhouChina
  4. 4.Department of Computer ScienceMiddlesex UniversityLondonUK

Personalised recommendations