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 asynchronously.
Technical details¶
Asynchronous mode of the Link Layer of IEEE 1394 was modeled in µCRL based on the documentation.
- Type of verification
- Deadlock, safety and liveness properties checking.
- Models
- 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. Institution: Centrum voor Wiskunde en Informatica (CWI), Amsterdam Time period: The model was written in 1997, translation to mCRL2 in 2005.
