Title :
Application of parametric model checking - the Root Contention protocol
Author :
Bandini, G. ; Spelberg, R.L. ; de Rooij, R.C.H. ; Toetenel, W.J.
Author_Institution :
Dept. of Comput. Sci., Florence Univ., Italy
Abstract :
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.
Keywords :
IEEE standards; formal verification; network interfaces; protocols; real-time systems; telecommunication computing; telecommunication standards; FireWire; IEEE 1394 standard; LPMC model checker; Root Contention protocol; automatic verification; formal verification; linear constraints; parametric model checking; randomization; real-time protocol specification; serial bus; Application software; Computer science; Firewire; Formal verification; High performance computing; Information technology; Network topology; Parametric statistics; Protocols; Real time systems;
Conference_Titel :
System Sciences, 2001. Proceedings of the 34th Annual Hawaii International Conference on
Conference_Location :
Maui, HI, USA
Print_ISBN :
0-7695-0981-9
DOI :
10.1109/HICSS.2001.927265
