Design and Analysis of Dynamic Leader Election Protocols in Broadcast Networks

摘要

The well-known problem of leader election in distributed systems is considered ina dynamic context where processes may participate and crash spontaneously. Processes communicate by means of buffered broadcasting as opposed to usual point-to-point communication. In this paper we design a leader election protocol in such a dynamic system. As the problem at hand is considerably complex we adopt a step-wise refinement design method starting from a simple leader election protocol. In a first refinement a symmetric solution is obtained and eventually a fault-tolerant protocol is constructed. This gives rise to three protocols. The worst case message complexity of all protocols is analyzed. A formal approach to the verification of the leader election protocols is adopted. The requirements are specified in a property-oriented way, and the protocols are denoted by means of extended finite state machines. It is proven using linear-time temporal logic that the protocols satisfy their requirements. Furthermore, the protocols are specified in more detail in the process algebra formalism Algebra of Communicating Processes (ACP).