Design and Analysis of Dynamic Leader Election Protocols in Broadcast Networks

The well-known problem of leader election in distributed systems is considered in a 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..