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

fYear

2001

fDate

6-6 Jan. 2001

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;

fLanguage

English

Publisher

ieee

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

Type

conf

DOI

10.1109/HICSS.2001.927265

Filename

927265