Verification of the link layer protocol of the IEEE-1394 serial bus (FireWire): An experiment with E-LOTOS (Q1856183)

The IEEE-1394 Standard (``FireWire'') describes a high-speed serial bus for multimedia PCs intended to unify several serial buses such as VME, MULTI-BUS II, and FUTURE BUS. The paper deals with the formal description of the LINK layer protocol of the IEEE-1394 Standard in the formal description techniques E-LOTOS and LOTOS, and its subsequent verification using model checking. The E-LOTOS descriptions are based on both the standard and the \(\mu\)CRL descriptions written by Luttik. The verifications are performed using the CADP (CÆSAR/ALDÉBARAN) toolbox. As a preliminary step, the E-LOTOS descriptions are translated, using the TRAIAN compiler, in LOTOS, which is the input language for the CADP toolbox. Five correctness criteria stated in natural language by Luttik are formalized in the action-based temporal logic ACTL. These logic formulas assess safety and liveness properties of the LINK layer protocol, such as deadlock freedom, appropriate sequencing of messages, etc. To contain the state space explosion, the verification is carried out only for a few scenarios involving a restricted number of nodes connected to the bus and a fixed number of transaction requests per node. Even under these restrictions, an undesirable deadlock situation in the protocol is detected. The error is caused by the ambiguous semantics of the state machines given in the standard, and it can be misleading for implementors of the IEEE-1394 protocol. A correction of this deadlock is proposed and validated.