IEEE 1394 link layer

From MCRL2

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.

Contents 1 Technical details 1.1 Type of verification 1.2 Models 2 Organizational context 2.1 Contact person 2.2 Other people involved 2.3 Institution 2.4 Time period 3 Publications

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 (TU/e)

Other people involved

Institution

Centrum voor Wiskunde en Informatica (CWI), Amsterdam

Time period

The model was written in 1997, translation to mCRL2 in 2005.

Publications

Description and formal specification of the Link Layer of P1394. In: Ignac Lovrek, editor, Proceedings of the 2nd International Workshop on Applied Formal Methods in System Design, University of Zagreb, Croatia. Also available as Report SEN-R9706, CWI, The Netherlands.