Formal Aspects of Computing
Volume 14, Number 3, 319-327, DOI: 10.1007/s001650300008

Original Paper

False Loop Detection in the IEEE 1394 Tree Identify Phase

Judi Romijn

View Related Documents

Abstract

The physical layer of the IEEE 1394 (FireWire, i-Link) architecture contains a protocol for spanning a tree in the network topology, which fails if the topology contains a loop. We show that the timing requirements for both the 1394-1995 and 1394a-2000 standards are too lenient: these allow for scenarios in which there is no loop in the topology, but the tree-spanning protocol does detect one. The scenarios are found by the model checker UPPAAL.

Keywords: Algorithm; Dynamic network; Loop detection; Protocol; Real-time; Timed automata; Spanning tree; Verification

Received August 2001/Accepted in revised form August 2001
Correspondence and offprint requests to: J. M. T. Romijn, Computing Science Department, Eindhoven University of Technology, PO Box 513, 5600 MB Eindhoven, The Netherlands. Email: J.M.T.Romijn@tue.nl

Fulltext Preview

Image of the first page of the fulltext document