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.

Requirements/Specifications (acm D.2.1), Software/Program Verification (acm D.2.4), Language Constructs and Features (acm D.3.3), Specifying and Verifying and Reasoning about Programs (acm F.3.1)
Theory of computing (msc 68Qxx), Formal languages and automata (msc 68Q45), Specification and verification (program logics, model checking, etc.) (msc 68Q60)
Software Engineering [SEN]

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