A Simple Verification of the Tree Identify Protocol with SMV
Viktor Schuppan, Armin Biere · 2001
The Tree Identify Protocol of the IEEE 1394 (FireWire) standard [5], [6], proposed as a case study for the application of formal methods [7], is given as a state machine. It can be translated easily into a corresponding model for a model checker. SMV [8], which we used in our evaluation, is probably one of the most widely used model checkers. This contribution describes on-going research on modeling and verifying the IEEE 1394 Tree Identify Protocol with SMV.