Parametric verification of the IEEE 1394a Root Contention protocol using LPMC

This paper presents an application of mechanical verification using LPMC, a new version of the PMC model checker tool. The focus is on the modeling and the automatic verification of a protocol contained in the IEEE 1394a standard, the Root Contention protocol. The Root Contention protocol involves both real-time and randomization. As is shown, the study demonstrates the power of the new LPMC capability of handling linear constraints in order to exploit parametric real-time model checking. LPMC generates parameter relations and parameter timing intervals associated with fair TCTL properties