A timed verification of the IEEE 1394 leader election protocol
The IEEE 1394 architecture standard defines a high performance serial multimedia bus that allows several components in a network to communicate with each other at high speed. In the physical layer of the architecture, a leader election protocol is used to find a spanning tree with a unique root in the network topology. If there is a cycle in the network, the protocol treats this as an error situation. This paper presents a formal model of the leader election protocol in the language IOA as well as a correctness proof. The verification shows that under certain timing restrictions the protocol behaves correct. The timing constants proposed in the IEEE 1394 standard documentation obey the requirements found in this proof.
|Network design and communication (msc 68M10), Models of computation (Turing machines, etc.) (msc 68Q05), Formal languages and automata (msc 68Q45), Specification and verification (program logics, model checking, etc.) (msc 68Q60), Applications of graph theory (msc 94C15)|
|Software Engineering [SEN]|
Romijn, J.M.T. (1999). A timed verification of the IEEE 1394 leader election protocol. Software Engineering [SEN]. CWI.