IEEE 1394 link layer
The behavior of the Link Layer in asynchronous mode is specified in µCRL.
This layer is the middle layer of the three-layered Firewire protocol,
responsible for construction of packets, the transmission of these over a serial
(one-bit) line to other parties, and the computation and verification of
checksums. Moreover, a Bus-process is specified, describing the external
behavior of the underlying physical components according to IEEE 1394, in order
to be able to simulate the situation where a number of Link Layers communicate
Asynchronous mode of the Link Layer of IEEE 1394 was modeled in µCRL based on
- Type of verification
Deadlock, safety and liveness properties checking.
The µCRL model is available as a part of the µCRL toolset distribution.
A translation to mCRL2, performed by Jan Friso Groote, is available as a part
of the mCRL2 distribution.
- Organizational context
- Contact person:
Bas Luttik, Technische Universiteit Eindhoven, The Netherlands.
Centrum voor Wiskunde en Informatica (CWI), Amsterdam
- Time period:
The model was written in 1997, translation to mCRL2 in 2005.