How can I be sure that my DVD player understands my TV?

by Wan Fokkink, Izak van Langevelde, Bas Luttik and Yaroslav Usenko

In the context of the ERCIM Working Group on Formal Methods for Industrial Critical Systems, protocols within HAVi (Home Audio Video Interoperability) and FireWire were analysed using a combination of state-of-the-art methods and tools for verification and testing.

A young trend in consumer electronics is the ubiquitous, transparent and intelligent integration of audio, video, communication and information services that have become so widely used in the 20th century. One of the key features of this integration is the ability of digital equipment to communicate reliably in a flexible fashion, which typically includes the plug-and-play ease of use. The look and feel of ambient intelligence, however, can be instantly destroyed by a single crude error message.

HAVi and the IEEE 1394 high-speed serial bus, better known as FireWire, target a dynamic interconnection of different pieces of equipment in the home environment. HAVi is a common, openly-licensable specification for networking digital home entertainment products that has been developed by eight multinationals. Devices connected in a HAVi network can inter-operate, using each other’s resources and functionality. HAVi is built on FireWire, which is designed to carry all forms of multiple digital audio and video streams quickly, reliably and inexpensively. Its architecture is scalable and a user can add or remove systems and peripherals easily at any time. FireWire has rapidly become the de-facto standard in the interconnection of digital devices.

Although intelligent household goods are mostly not safety-critical, validation of their correctness is an important issue. The financial implications of errors or bad performance can be enormous, because of their mass replication and damage to consumer interests. The high complexity of the protocols underlying such products (specifications typically require several hundreds of pages) turn their verification into a major challenge. A number of protocols within HAVi and FireWire have been analysed successfully using formal methods.

One notable study involved the analysis of the so-called HAVi leader election protocol, which was carried out at CWI. In HAVi, controllers, acting as hosts for digital devices, elect among themselves a leader with the best capabilities to supervise their controlling tasks. Each time when a change in the network of the underlying FireWire interface occurs, the controllers need to re-elect a leader. The HAVi leader election protocol was specified in the specification languages LOTOS, Promela and µCRL. The resulting models were analysed using model checking techniques, which facilitate the automated verification of behavioural properties. This analysis revealed that the leader election protocol does not meet some critical safety properties and that there are situations in which the protocol does not converge to the election of a leader. These errors were due to a lack of detail in the HAVi specification. They occur when communication between devices is faster than communication between components within one device. These aspects were taken into account in a subsequent specification of the HAVi leader election protocol.

A second study targeted the Link layer of FireWire using the language µCRL and the associated tool set, both developed at CWI. FireWire describes the serial bus in three layers: the Transaction layer offers an interface of high-level instructions, such as reading and writing of data, the Link layer transforms these instructions into packets of bits, and the Physical layer is concerned with the actual sending and receiving of the bits. The analysis brought to light a serious case of underspecification: when the Link layer receives a packet from the Physical layer, the handling of a request from the Transaction layer is left unspecified. Different solutions were proposed independently at CWI and at the University of Kiel. At INRIA Rhône-Alpes a model checking analysis revealed a deadlock, due to a flaw in the communication scheme between Link and Transaction layer. The shortest execution trace leading to this deadlock consists of fifty consecutive transitions, which indicates that it would be very difficult to discover this deadlock by means of testing.

Third, the FireWire tree identify protocol for spanning a tree in the network topology was tackled at the University of Nijmegen. This tree identification fails if the network topology contains a loop, which is signalled using a time-out mechanism. With the timed model checker UPPAAL it was detected that the timing constraints of FireWire are too lenient: they allow for scenarios in which there is a time-out but no loop in the topology. Furthermore, the FireWire root contention protocol was studied, which comes into play in the finale of the tree identify protocol where two nodes compete to become the root of the tree.

Correctness of this root contention protocol was established by a number of case studies using a combination of UPPAAL and probabilistic I/O automata. In collaboration with the University of Aalborg, precise timing constraints were derived. A young initiative is the analysis of the IEEE 1394.1 standard for Bus Bridges, being developed to connect FireWire networks through so-called `bridges’. The initial modelling of the standard in Promela at CWI and the University of Nijmegen has already revealed a number of bugs in the draft specification, in the algorithm that updates routing tables. Some of these discoveries have been taken into account in the latest draft of the standard. The aim is to conclude this verification before the standard is finalised, thus contributing further to the standardisation process. Envisioned extensions of this project include the analysis of stochastic aspects at the University of Twente.

Concluding, these case studies bring home the point that communication between for example a DVD player and a TV can benefit from the analysis of the underlying protocols by means of formal methods.

Links:
http://www.cwi.nl/sen2/
http://www.inrialpes.fr/vasy/fmics/
http://www.cs.stir.ac.uk/firewire-workshop/ 

Please contact:
Wan Fokkink - CWI
Tel: +31 20 592 4104
E-mail: wancwi.nl