We performed the formal specification and verification of the asynchronous mode of the Link Layer protocol of the IEEE-1394 Serial Bus (``FireWire''). This protocol will be used in multimedia PCs, to connect high data transfer rate peripherials (such as Video cameras). Many constructors already use this protocol: Apple, AT&T, Canon, Compaq, Hewlett Packard ...

We started off from the description of the link protocol written in the muCRL language by Luttik. After translating it into E-LOTOS, we added the specification of the transaction layer protocol. These descriptions were then translated into the LOTOS language, and we performed verifications by model-checking using the CADP toolbox.

The models of the LOTOS descriptions were generated using the CAESAR compiler (by putting bounds on the data domains and choosing specific scenarios). We formally expressed in ACTL temporal logic five correctness properties of the LINK layer protocol stated in natural language by Luttik and we verified them on the models using the XTL model-checker.

We detected and corrected a potential deadlock caused by the ambiguous semantics of the state machines given in the standard, which can be misleading for implementors of the IEEE-1394 protocol.

We successfully applied the model-checking approach to this case-study. Thus, we were able to verify the correctness properties of the LINK layer protocol for a number of nodes less than 4, and for specific scenarios covering all the cases of the protocol. Of course, the approach cannot "prove" the correctness of the protocol for an arbitrary number of nodes and arbitrary scenarios, but it provides a better understanding of the protocol's behaviour and a certain degree of confidence in its correctness. Moreover, model-checking has the advantage of being completely automated and efficient (we performed the above-mentionned verifications in a few minutes). The whole case-study took approximately one month.

This protocol has also been studied in the framework of theorem-proving [Kuhne-Hooman-Roever-97] and [Luttik-97]. It is worth noticing that neither of these approaches prove (at this moment) the complete correctness of the protocol.

As regards the specification's formalism, we found E-LOTOS very adequate for this kind of application. E-LOTOS eliminates some deficiencies of LOTOS. The E-LOTOS descriptions we obtained are quite compact (7 pages of source code) compared to 13 pages of muCRL description language in [Luttik-97]. Especially for the data types, the gain in conciseness is significant: 4 pages of E-LOTOS instead of 8 pages of muCRL. Also, it is worth noticing that E-LOTOS allows a clearer and more readable description of the behaviour expressions than LOTOS and muCRL.

• [Kuhne-Hooman-Roever-97]
  Lars Kuhne and Josef Hooman and Willem-Paul de Roever. Towards Mechanical Verification of Parts of the IEEE P1394 Serial Bus. In Proceedings of the 2nd COST 247 International Workshop on Applied Formal Methods in System Design (Zagreb, Croatia), June 1997.

• [Luttik-97]
  Bas Luttik. Description and Formal Specification of the Link Layer of P1394. In Proceedings of the 2nd COST 247 International Workshop on Applied Formal Methods in System Design (Zagreb, Croatia), June 1997.

• [Sighireanu-Mateescu-97]
  Mihaela Sighireanu and Radu Mateescu. Validation of the Link Layer Protocol of the IEEE-1394 Serial Bus (``FireWire''): an Experiment with E-LOTOS. In Proceedings of the 2nd COST 247 International Workshop on Applied Formal Methods in System Design (Zagreb, Croatia), June 1997. Full version of this paper is available as INRIA Research Report RR-3172.
  Available on-line from http://cadp.inria.fr/publications/Sighireanu-Mateescu-97.html
  and from the CADP Web site in PDF or PostScript

• [Garavel-Luttik-24]
  Hubert Garavel and Bas Luttik. Four Formal Models of IEEE 1394 Link Layer. In Proceedings of the 6th Workshop on Models for Formal Analysis of Real Systems (MARS 2024), Luxembourg, April 2024.
  Available on-line from http://cadp.inria.fr/publications/Garavel-Luttik-24.html
  and from the CADP Web site in PDF or PostScript