Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Four Formal Models of IEEE 1394 Link Layer

Hubert Garavel, Bas Luttik

TL;DR

The paper revisits the asynchronous link-layer of IEEE 1394 FireWire, using formal methods to uncover and address deadlocks. It presents four formal models—muCRL, mCRL2, LOTOS, and LNT—tracing their evolution from the original muCRL model to a modern LNT version and comparing their modelling styles. Through model checking and equivalence checks, it demonstrates that LOTOS and LNT yield closely related results, while the original deadlock issues are resolved in the newer models; the work also serves as a cross-language benchmark for protocol modelling. Overall, the study provides a valuable Rosetta stone for understanding how different formal languages capture complex concurrent systems and highlights the practical benefits of modern tools for validating historic protocol designs.

Abstract

We revisit the IEEE 1394 high-performance serial bus ("FireWire"), which became a success story in formal methods after three PhD students, by using process algebra and model checking, detected a deadlock error in this IEEE standard. We present four formal models for the asynchronous mode of the Link Layer of IEEE 1394: the original model in muCRL, a simplified model in mCRL2, a revised model in LOTOS, and a novel model in LNT.

Four Formal Models of IEEE 1394 Link Layer

TL;DR

The paper revisits the asynchronous link-layer of IEEE 1394 FireWire, using formal methods to uncover and address deadlocks. It presents four formal models—muCRL, mCRL2, LOTOS, and LNT—tracing their evolution from the original muCRL model to a modern LNT version and comparing their modelling styles. Through model checking and equivalence checks, it demonstrates that LOTOS and LNT yield closely related results, while the original deadlock issues are resolved in the newer models; the work also serves as a cross-language benchmark for protocol modelling. Overall, the study provides a valuable Rosetta stone for understanding how different formal languages capture complex concurrent systems and highlights the practical benefits of modern tools for validating historic protocol designs.

Abstract

We revisit the IEEE 1394 high-performance serial bus ("FireWire"), which became a success story in formal methods after three PhD students, by using process algebra and model checking, detected a deadlock error in this IEEE standard. We present four formal models for the asynchronous mode of the Link Layer of IEEE 1394: the original model in muCRL, a simplified model in mCRL2, a revised model in LOTOS, and a novel model in LNT.
Paper Structure (46 sections, 1 figure)

This paper contains 46 sections, 1 figure.

Table of Contents

  1. Introduction
  2. IEEE 1394 bus
  3. Architecture
  4. Link layer
  5. Send mode.
  6. Receive mode.
  7. Send acknowledgement mode.
  8. Physical layer
  9. Transaction and application layers
  10. TRANS process.
  11. APPLI process.
  12. NODE process.
  13. Formal models
  14. Formal model in $\mu$CRL
  15. Formal model in LOTOS
  16. ...and 31 more sections

Figures (1)

  • Figure 1: IEEE 1394 architecture