Firewire

Description:IEEE 1394 Link Layer
Author(s):Hubert Garavel, Bas Luttik
Event(s): MARS'24
Paper(s): Four Formal Models of IEEE 1394 Link Layer

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.

Model(s)

    1. Download Model
    2. Browse Model
    3. tool(s): mCRL
    1. Download Model
    2. Browse Model
    3. tool(s): LOTOS (CADP)
    1. Download Model
    2. Browse Model
    3. tool(s): mCRL2
    1. Download Model
    2. Browse Model
    3. tool(s): LNT (CADP)
Creative Commons License    This work is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License.

© 2016–2024, Last Update March 27, 2024