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

	This Article
	Subscribers, please Login Purchase article: $19 PDF IEEE Xplore Subscribers RSS feed
	Share
	Email this Article to a friend
	Bibliographic References
	ASCII Text BibTex RefWorks Procite/RefMan/Endnote
	Add to:
	Digg Furl Spurl Blink Simpy Google Del.icio.us Y!MyWeb
	Search
	Similar Articles Articles by H. Toetenel Articles by R.L. Spelberg Articles by G. Bandini

Seventh International Conference on Real-Time Computing Systems and Applications (RTCSA'00)

Cheju Island, South Korea

December 12-December 14

ISBN: 0-7695-0930-4

	ASCII Text	x
	H. Toetenel, R.L. Spelberg, G. Bandini, "Parametric verification of the IEEE 1394a Root Contention protocol using LPMC," Real-Time Computing Systems and Applications, International Workshop on, pp. 207, Seventh International Conference on Real-Time Computing Systems and Applications (RTCSA'00), 2000.

	BibTex	x
	@article{ 10.1109/RTCSA.2000.896393, author = {H. Toetenel and R.L. Spelberg and G. Bandini}, title = {Parametric verification of the IEEE 1394a Root Contention protocol using LPMC}, journal ={Real-Time Computing Systems and Applications, International Workshop on}, volume = {0}, year = {2000}, issn = {1533-2306}, pages = {207}, doi = {http://doi.ieeecomputersociety.org/10.1109/RTCSA.2000.896393}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }

	RefWorks Procite/RefMan/Endnote	x
	TY - CONF JO - Real-Time Computing Systems and Applications, International Workshop on TI - Parametric verification of the IEEE 1394a Root Contention protocol using LPMC SN - 1533-2306 SP EP A1 - H. Toetenel, A1 - R.L. Spelberg, A1 - G. Bandini, PY - 2000 KW - formal verification; IEEE standards; telecommunication standards; protocols; real-time systems; parametric verification; IEEE 1394a standard; Root Contention protocol; LPMC; PMC model checker; randomization; parameter relations; linear constraints; real-time model checking; parameter timing intervals VL - 0 JA - Real-Time Computing Systems and Applications, International Workshop on ER -

H. Toetenel, Fac. of Inf. Technol. & Syst., Delft Univ. of Technol., Netherlands

R.L. Spelberg, Fac. of Inf. Technol. & Syst., Delft Univ. of Technol., Netherlands

G. Bandini, Fac. of Inf. Technol. & Syst., Delft Univ. of Technol., Netherlands

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/RTCSA.2000.896393

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.

Index Terms:

formal verification; IEEE standards; telecommunication standards; protocols; real-time systems; parametric verification; IEEE 1394a standard; Root Contention protocol; LPMC; PMC model checker; randomization; parameter relations; linear constraints; real-time model checking; parameter timing intervals

Citation:

H. Toetenel, R.L. Spelberg, G. Bandini, "Parametric verification of the IEEE 1394a Root Contention protocol using LPMC," rtcsa, pp.207, Seventh International Conference on Real-Time Computing Systems and Applications (RTCSA'00), 2000

Peer Review Notice | Give Us Feedback

Usage of this product signifies your acceptance of the Terms of Use.