E-LOTOS and LOTOS
CADP (Construction and Analysis of Distributed Processes)
March 1997 (approximately one man month)
750 lines of source E-LOTOS code
1150 lines of source LOTOS code
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.
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 technical information about this case-study can be found at the
following Web page:
The LOTOS sources as well as explanations on the verification with CADP are available on line at: http://cadp.inria.fr/ftp/demos/demo_23
This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies