We specify the tree identify protocol of the IEEE 1394 high performance serial multimedia bus at three different levels of detail using $mu$CRL. We use the cones and foci verification technique of Groote and Springintveld to show that the descriptions are equivalent under branching bisimulation, thereby demonstrating that the protocol behaves as expected.

, , ,
, ,
Software Engineering [SEN]

Shankland, C, & van der Zwaag, M.B. (1998). The tree identify protocol of IEEE 1394 in uCRL. Software Engineering [SEN]. CWI.