Analyzing Eventual Leader Election Protocols for Dynamic Systems by Probabilistic Model Checking
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.
KeywordsDynamic systems Verification Leader election Probabilistic model checking
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.
- 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.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.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
- 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
- 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
- 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.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