Database of Case Studies Achieved Using CADP

The Link Layer Protocol of the IEEE-1394 Serial Bus (``FireWire'')

Organisation: INRIA Rhone-Alpes

Method: E-LOTOS and LOTOS

Tools used: CADP (Construction and Analysis of Distributed Processes)

Domain: Hardware Design.

Period: March 1997 (approximately one man month)

Size: 750 lines of source E-LOTOS code
1150 lines of source LOTOS code

Description:

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.

Conclusions:

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.

Publications:
  • [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 our FTP site in PDF or PostScript

Contact:
Mihaela SIGHIREANU and Radu MATEESCU
INRIA Rhone-Alpes / Dyade
655, Avenue de l'Europe
38330 Montbonnot Saint Martin, FRANCE
Tel: +(33) 04 76 61 52 83
Fax: +(33) 04 76 61 52 52
e-mail: Mihaela.Sighireanu@inria.fr, Radu.Mateescu@inria.fr



Further remarks: Further technical information about this case-study can be found at the following Web page: http://vasy.inria.fr/press/firewire.html

The LOTOS sources as well as explanations on the verification with CADP are available on line at: ftp://ftp.inrialpes.fr/pub/vasy/demos/demo_23

This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies


Last modified: Sun Jun 18 22:38:23 2017.


Back to the CADP case studies page