Mechanical verification of the IEEE 1394a root contention protocol using

Abstract. The mechanical verification of the root contention protocol from the physical layer of the IEEE1394a standard [1] for a high performance serial bus is described. In this case study, the Uppaal2k [2, 3] model checker of real-time systems is utilized. An enhanced model of the protocol is presented, which corrects for imperfections in the communication model from [4]. Using this new model, the correctness of the root contention protocol is demonstrated. The required timing constraints are established via analysis of the protocol and via approximate parameter analysis.