The system as a whole is complex, comprising a number of distributed communicating components and using a number of different protocols for different tasks (e.g. data transfer between nodes in the network, bus arbitration, leader election). The IEEE standard IEEE 1394-1995 provides a layered description in the style of OSI, with physical, link, and transaction layers. Each layer is in turn split into different phases.
In essence, the tree identify process of IEEE 1394 is a leader election protocol which takes place after a bus reset in the network (i.e. when a node is added to, or removed from, the network). Immediately after a bus reset all nodes in the network have equal status, and know only to which nodes they are directly connected. A leader (root) needs to be chosen to act as the manager of the bus for subsequent phases of the 1394. The protocol is designed for use on connected networks, will correctly elect a leader if the network is acyclic, and will report an error if a cycle is detected.
Essentially, each node has two phases based on the number of children, c, and the number of neighbours, n. If n - c > 1 the node waits for ``be my parent'' requests from its neighbours. If n - c = 1 then the node sends a ``be my parent'' request to the neighbour which isn't a child if it hasn't already received a ``be my parent'' request from that neighbour. This implies that leaf nodes are the first to communicate with their neighbours, and that the spanning tree is built from the leaves.
The protocol may not proceed this straightforwardly because ``be my parent'' requests are not atomic and may not be sucessful. Actually, a request must be followed by an acknowledgement, and an acknowledgement of the acknowledgement!
Since requests are not atomic contention may arise (two nodes simultaneously send ``be my parent'' requests to each other). Since only one node can be the leader contention must be resolved; this is done by timing. The standard specifies that each node chooses nondeterministically whether to wait for a long or short time. If, after the wait period is over, there is a message from the other node saying ``be my parent'' then the node becomes the root. If there is no such message then the node resends its own ``be my parent'' message (and contention may result again).
This protocol is similar to one presented in Distributed Algorithms, page 501, where a different method of contention resolution is used (the node with the highest identifier becomes the root). This approach will not work for IEEE 1394 because the nodes do not have identifiers during the Tree Identification Phase. The protocols were developed independently.
We have a special arrangement with IEEE for bulk ordering the standard and the supplement documents at substantially reduced cost (half normal non IEEE member price). Contact us to find out more.
You may also wish to visit the IEEE standards site.
Specifically, for the Tree Identify Protocol the safety and liveness requirements to be proved are:
For after the workshop:
J.M.T. Romijn. A Timed Verification of the IEEE 1394 Leader Election Protocol. In Fourth International Workshop on Formal Methods for Industrial Critical Systems , 1999. To appear as a special issue of Formal Methods in System Design.
D.P.L. Simons and M.I.A. Stoelinga. Mechanical Verification of the IEEE 1394a Root Contention Protocol using Uppaal2k. Report CSI-R009, Computing Science Institute, University of Nijmegen, Nijmegen, 2000.
M.I.A. Stoelinga and F.W. Vaandrager. Root Contention in IEEE 1394. In 5th AMAST Workshop on Real-Time and Probabilistic Systems, LNCS 1601. Springer-Verlag, 1999.
G. Bandini, R.L. Spelberg, R.C.H. de Rooij, and W.J. Toetenel. Application of Parametric Model Checking - The Root Contention Protocol. In proceedings of the Hawaii International Conference on Systems Sciences (HICSS-34 2001), IEEE Computer Society Press, 2001.
Have we missed out your formal specification/analysis of the Tree Identify Protocol of IEEE 1394? Contact us and we'll update the page.
IEEE 1394a-2000. Institute of Electrical and Electronics Engineers. IEEE Standard for a High Performance Serial Bus (Supplement). Std 1394a-2000, 2000.
N. Lynch. Distributed Algorithms. Morgan Kaufmann Publishers, Inc, 1996.