False Loop Detection in the IEEE 1394 Tree Identify Phase

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. 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