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.
|Network design and communication (msc 68M10), Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (msc 68Q10), Theory of computing (msc 68Qxx), Formal languages and automata (msc 68Q45), Specification and verification (program logics, model checking, etc.) (msc 68Q60), Abstract data types; algebraic specification (msc 68Q65)|
|Software Engineering [SEN]|
Romijn, J.M.T. (1999). Model checking the HAVi leader election protocol. Software Engineering [SEN]. CWI.