Four Formal Models of IEEE 1394 Link Layer

Hubert Garavel and Bas Luttik

Proceedings of the 6th Workshop on Models for Formal Analysis of Real Systems (MARS 2024), Luxembourg, April 2024


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.

80 pages

Slides of H. Garavel's lecture at the MARS'24 workshop