A Three-Level Verification of a Tree Identify Protocol Analysing a fragment of the IEEE 1394 Serial Bus

Judi Romijn

(CWI, Amsterdam)

The IEEE 1394 Serial Bus Protocol has been developed for interconnecting computer and consumer end-equipment, providing quick, reliable and inexpensive high-bandwidth transfer of digitized video and audio.

The 1394 protocol is divided over several layers. In the physical layer, the initialization work is partly done by the tree identify phase, which has to span a tree in the bus topology in order to elect a leader among the components connected to the bus.

We have been working at the verification of the tree identify protocol at three levels of abstraction. The idea behind our approach is that some properties of this protocol involve much more detail than others. Our aim is to verify each desired property at the appropriate level of abstraction, and reuse the results of more abstract levels by means of refinement proofs.

Joint work with: Marco Devillers, David Griffioen, and Frits Vaandrager (University of Nijmegen)
Tuesday 14th October 1997, 14:30
Seminar Room 322
Department of Computer Science