UNIVERSITY of GLASGOW

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
Abstract:

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