Fun with FireWire: A Comparative Study of Formal Verification Methods Applied to the IEEE 1394 Root Contention Protocol

摘要

The IEEE 1394 Root Contention Protocol is an industrial leader election algorithm for two processes in which probability, real time and parameters play an important role. This protocol has been analysed in various case studies, using a variety of verification and analysis methods. In this paper, we survey and compare several of these case studies.