There are two kinds of devices in the HAVi architecture: controllers and controlled devices. The controller acts as a host for controlled devices via a Device Control Module (DCM). Installation and allocation of DCMs is handled by a HAVi software component called Device Control Module Manager (DCM Manager). Each controller is supposed to have a DCM Manager. All DCM Managers cooperate with each other in order to perform the correct installation and allocation of DCMs in the presence of dynamic plug-and-play changes of the IEEE-1394 network. Whenever a change in the network occurs, the DCM Managers restart their activities by first choosing a leader among them, and then under the control of this leader, complete their DCM controlling tasks.

This case-study concerns the verification of the HAVi leader election protocol between DCM Managers. Several specifications of the protocol have been developed using the description languages LOTOS and PROMELA, and four safety and liveness properties of the protocol have been formulated and verified on these specifications using the verification toolsets CADP and SPIN, respectively. Several HAVi configurations have been considered, by varying the number of DCM managers (two or three) and the communication mode (synchronous or asynchronous).

The XTL tool of CADP allowed to find some errors in the HAVi leader election protocol: although the safety properties are more or less met by the protocol, there are situations in which the protocol may never converge to designate a leader. The liveness property that is violated was expressed in ACTL and checked using XTL on the models generated from the LOTOS specifications. Since it is a "pure" branching-time property, it cannot be expressed in LTL to be checked by SPIN; however, the error trace produced by XTL has been replayed by interactive simulation with SPIN and allowed to reproduce the error on the PROMELA specification.

In cooperation with Philips Natlab, a leader election protocol from the draft HAVi standard was selected for validation with the use of model checking tools. This protocol has been specified in the formal languages LOTOS and Promela, and has been model checked with the tools CADP and SPIN. With CADP a bug in the protocol could be detected, with SPIN no errors were found, due to lack of expressiveness of the model checking logic.

The cause of the errors found in the HAVi leader election protocol is that the HAVi specification is not detailed enough to ensure that HAVi compliant implementations are faultless. It seems that realistic timing requirements on sending and processing of messages should be added to the HAVi specification in order to ensure the correctness of the leader election protocol.

The combined approach of having different models of the same protocol and different verification techniques seems to give better results: it forces the user to think carefully about the modelling of all the aspects of the protocol; it allows to establish different kinds of properties of the protocol; and it enables the user to cross-check with one tool the verification results obtained with the other.