Model checking the HAVi leader election protocol
The HAVi specification proposes an architecture for audio/video interoperability in home networks. Part of the HAVi specification is a distributed leader election protocol. We have modelled this leader election protocol in Promela and Lotos and have checked several properties with the tools Spin and Xtl (from the Caesar/Aldebaran package). It turns out that the protocol does not meet some safety properties and that there are situations in which the protocol may never converge to designate a leader. Our conclusion is that realistic timing requirements on sending and processing of messages should be added to the HAVi specification. Then a (timed) formal verification could give a definite answer with respect to correctness of the leader election protocol.
|, , , , ,|
|Software Engineering [SEN]|
Romijn, J.M.T. (1999). Model checking the HAVi leader election protocol. Software Engineering [SEN]. CWI.