Model Checking the HAVi Leader Election Protocol. Software Engineering

摘要

The HAVi specification (9) proposes an architecture for audio/video211u001einteroperability in home networks. Part of the HAVi specification is a 211u001edistributed leader election protocol. The authors have modelled this leader 211u001eelection protocol in Promela and Lotos and have checked several properties with 211u001ethe tools Spin and Xtl (from the Ceasar/Aldebaran package). It turns out that the 211u001eprotocol does not meet some safety properties and that there are situations in 211u001ewhich the protocol may never converge to designate a leader. The authors' 211u001econclusion is that realistic timing requirements on sending and processing of 211u001emessages should be added to the HAVi specification. Then a (timed) formal 211u001everification could give a definite answer with respect to correctness of the 211u001eleader election protocol.