Four Formal Models of IEEE 1394 Link Layer
<|reference_start|>Four Formal Models of IEEE 1394 Link Layer: 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.<|reference_end|>
@article{garavel2024four,
    title={Four Formal Models of IEEE 1394 Link Layer},
    author={Hubert Garavel (Univ. Grenoble Alpes, INRIA, CNRS, Grenoble INP, LIG,
  Grenoble, France), Bas Luttik (Eindhoven University of Technology, The
  Netherlands)},
    journal={EPTCS 399, 2024, pp. 21-100},
    year={2024},
    doi={10.4204/EPTCS.399.5},
    archivePrefix={arXiv},
    eprint={2403.18723},
    primaryClass={cs.LO cs.AR cs.PL}
}