Regular contribution Verication of the Link layer protocol of the IEEE-1394 serial bus (FireWire): an experiment with E-LOTOS
Mihaela Sighireanu, Radu Mateescu, Inria Rh · 1998
The Ieee-1394 Standard (\FireWire) de- scribes a high-speed serial bus for multimedia PCs in- tended to unify several serial buses such as Vme, Multi- bus II ,a ndFuture Bus. This 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 verication using model checking. The E-Lotos descriptions are based on both the standard and the Crl descriptions writ- ten by Luttik. The verications are performed using the Cadp (Csar/Ald ebaran) 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 proto- col, such as deadlock freedom, appropriate sequencing of messages, etc. To contain the state space explosion, the verication is carried out only for a few scenarios involv- ing a restricted number of nodes connected to the bus and a xed number of transaction requests per node. Even under these restrictions, an undesirable deadlock situ- ation 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.