DESIGN AND ANALYSIS OF DYNAMIC LEADER ELECTION PROTOCOLS IN BROADCASTNETWORKS

The well-known problem of leader election in distributed systems is co nsidered in a dynamic context where processes may participate and cras h spontaneously. Processes communicate by means of buffered broadcasti ng as opposed to usual point-to-point communication. In this paper we design a leader election protocol in such a dynamic context. As the pr oblem at hand is considerably complex we develop the protocol in three steps. In the initial design processes are considered to be perfect a nd a leader is assumed to be present initially. In the second protocol , the assumption of an initial leader is dropped. This leads to a symm etric protocol which uses an (abstract) timeout mechanism to detect th e absence of a leader. Finally, in the last step of the design process es may crash without giving any notification of other processes. The w orst case message complexity of all protocols is addressed. A formal a pproach to the specification and verification of the leader election p rotocols is adopted. The requirements are specified in a property-orie nted way and the protocols are denoted by means of extended finite sta te machines. It is proven using linear-time temporal logic that the fa ult-tolerant protocol satisfies its requirements.