Computing at Glasgow University
Paper ID: 7126
DCS Tech Report Number: TR-2003-155

Two approaches to verifying the Tree identify phase of the IEEE 1394 (FireWire) protocol for any size of network
Miller,A. Calder,M.

Publication Type: Tech Report (internal)
Appeared in: DCS Tech Report
Page Numbers :
Publisher: Dept of Computing Science, University of Glasgow
Year: 2003

We describe two techniques for proving properties of the tree identify phase of the IEEE 1394 Tree identify protocol for any size of network. The first approach involves the construction of a network invariant together with data abstraction to prove safety properties for systems with a star configuration and an extension to systems with a configuration belonging to one of a given set of families. The second approach applies to all acyclic configurations and exploits the degenerative nature of the protocol.

Keywords: IEEE 1394, Firewire

PDF Bibtex entry Endnote XML