Verifying the IEEE 1394 FireWire Tree Identify Protocol with SMV

This case study contains a formal verification of the IEEE 1394 FireWire tree identify protocol. Crucial properties of finite models of the protocol have been validated with state-of-the-art symbolic model checkers. Various optimisation techniques were applied to verify concrete and generic configurations. Received September 2001/Accepted in revised form September 2001 Correspondence and offprint requests to: Viktor Schuppan, Computer Systems Institute, ETH Zurich, 8092 Zurich, Switzerland. Email: Viktor.Schuppan@inf.ethz.ch