CWI (Amsterdam) and Philips Research Laboratories
LOTOS and PROMELA
CADP (Construction and Analysis of Distributed Processes)
SPIN (Simple Promela INterpreter)
about 1500 lines of LOTOS (40% for the data part, 60% for the control part)
about 400 lines of PROMELA
The HAVi specification is the result of a joint attempt from eight consumer electronics companies (Grundig, Hitachi, Matsushita, Philips, Sharp, Sony, Thomson, and Toshiba) to solve interoperability problems for home audio/video networks.
It defines a set of APIs allowing consumer electronics manufacturers and third parties to develop applications for the home network, which is viewed as a distributed computing platform supposed to work on top of an IEEE-1394 serial bus network.
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.
This case-study is summarized in the SEN2 Scientific Report (1998,
) as follows:
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.
Grundig, Hitachi, Matsushita, Philips, Sharp, Sony, Thomson,
"The HAVi Specification. Version 1.0 beta".
November 19, 1998.
Available on-line at: http://www.havi.org
[Romijn-99] Judi Romijn. "Model Checking a HAVi Leader Election Protocol". Technical Report SEN-R9915, CWI, June 1999.
Available on-line at: http://www.win.tue.nl/~jromijn/papers/HAVi.ps.gz
or also from our FTP site in PDF or PostScript
Computing Science Institute
University of Nijmegen
Toernooiveld 1 (Room A5025)
6525 ED Nijmegen
P.O. Box 9010
6500 GL Nijmegen
Tel: +31 (0)24 36 52599
Fax: +31 (0)24 36 53137
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|