Timed Verification of the IEEE 1394 Leader Election Protocol

摘要

The IEEE 1394 architecture standard defines a high performance serial multimedia211u001ebus that allows several components in a network to communicate with each other at 211u001ehigh speed. In the physical layer of the architecture, a leader election protocol 211u001eis used to find a spanning tree with a unique root in the network topology. If 211u001ethere is a cycle in the network, the protocol treat this as an error situation. 211u001eThis paper presents a formal model of the leader electron protocol in the 211u001elanguage IOA as well as a correctness proof. The verification shows that under 211u001ecertain timing restrictions the protocol behaves correct. The timing constants 211u001eproposed in the IEEE 1394 standard documentation obey the requirements found in 211u001ethis proof.