HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

Validation of the Link Layer Protocol of the IEEE-1394 Serial Bus («FireWire»): an Experiment with E-LOTOS

Mihaela Sighireanu 1 Radu Mateescu 1
1 VASY - System validation - Research and applications
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : This paper deals with the description in E-LOTOS of the asynchronous LINK layer protocol of the IEEE-1394 Standard and its verification using model-checking. The E-LOTOS descriptions are based on both the standard and the mu-CRL description written by Luttik. The verifications are performed using the CADP (CÆSAR/ALDEBARAN) toolbox. We translate the E-LOTOS descriptions in LOTOS using the TRAIAN tool, and then we generate the underlying LTS models corresponding to various scenarios using the CAESAR compiler. We formally express in the ACTL temporal logic the five correctness properties of the LINK layer protocol stated in natural language by Luttik and we verify them on the LTS models using the XTL model-checker. We detect and correct 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.
Document type :
Complete list of metadata

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 1:06:27 PM
Last modification on : Friday, February 4, 2022 - 3:24:28 AM
Long-term archiving on: : Sunday, April 4, 2010 - 10:00:10 PM


  • HAL Id : inria-00073516, version 1



Mihaela Sighireanu, Radu Mateescu. Validation of the Link Layer Protocol of the IEEE-1394 Serial Bus («FireWire»): an Experiment with E-LOTOS. [Research Report] RR-3172, INRIA. 1997. ⟨inria-00073516⟩



Record views


Files downloads