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. (1999). Model checking the HAVi leader election protocol. Software Engineering [SEN]. CWI.