Application of parametric model checking - the Root Contention protocol
Gianfranco Bandini, Ronald Lutje Spelberg, R.C.M. de Rooij, W.J. Toetenel · 2005
Presents an application of formal verification which was carried out using a new implemented version of the LPMC model checker tool. The focus is on the modeling and the automatic verification of a protocol contained in the IEEE 1394 standard, the Root Contention protocol. This protocol involves both real time and randomization. This is an illustrative case study which fully demonstrates the use of the new LPMC tool's capability of handling linear constraints in order to exploit parametric real-time model checking.