================================================================================
P9324   J.J. Brunekreef, J.P. Katoen, R.L.C. Koymans & S. Mauw
        "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. Furthermore, the protocols are specified in more detail in
the process algebra formalism ACP.