Four Formal Models of IEEE 1394 Link Layer
Hubert Garavel, Bas Luttik · Electronic Proceedings in Theoretical Computer Science · 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 µCRL, a simplified model in mCRL2, a revised model in LOTOS, and a novel model in LNT.