Application of Parametric Model Checking – The Root Contention Protokol

Introduction and overview

The IEEE 1394 high performance serial bus was first developed – under the name FireWire- by Apple Computer, Inc. and later formally approved and accepted as a standard by IEEE in 1996.

Various parts of IEEE 1394 have been specified and/or formally verified. Among these are the link layer core , the leader election protocol and other communication mechanisms . In this paper we focus in the verification of the root Contention protocol. A verification for this protocol has been al-ready conducted using a formal verification technique based on theorem proving but, as far as we know, it has never been automatically verified using a model checking technique.

Read More...