Abstract:

In formal methods we are always searching for new and interesting examples to which we can apply our techniques. In this talk I will introduce a case study based on the Philips "firewire". (More specifically, the tree identify protocol of a high performance serial multimedia bus (IEEE standard 1394)). The description, given using muCRL, is made in varying levels of detail and I show, using the cones and foci technique of Groote and Springintveldt that these different descriptions are all equivalent under branching bisimulation. I'll also talk about the techniques used, and make some observations about properties of the protocol.