Modeling and Verification of Biphase Mark Protocolsin Duration Calculus Using PVS

	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
	Add to:
	Digg Furl Spurl Blink Simpy Google Del.icio.us Y!MyWeb
	Search
	Similar Articles Articles by Dang Van Hung

First International Conference on Application of Concurrency to System Design (ACSD'98)

Fukushima, Japan

March 23-March 26

ISBN: 0-8186-8350-3

	ASCII Text	x
	Dang Van Hung, "Modeling and Verification of Biphase Mark Protocolsin Duration Calculus Using PVS," Application of Concurrency to System Design, International Conference on, pp. 88, First International Conference on Application of Concurrency to System Design (ACSD'98), 1998.

	BibTex	x
	@article{ 10.1109/CSD.1998.657542, author = {Dang Van Hung}, title = {Modeling and Verification of Biphase Mark Protocolsin Duration Calculus Using PVS}, journal ={Application of Concurrency to System Design, International Conference on}, volume = {0}, year = {1998}, isbn = {0-8186-8350-3}, pages = {88}, doi = {http://doi.ieeecomputersociety.org/10.1109/CSD.1998.657542}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }

	RefWorks Procite/RefMan/Endnote	x
	TY - CONF JO - Application of Concurrency to System Design, International Conference on TI - Modeling and Verification of Biphase Mark Protocolsin Duration Calculus Using PVS SN - 0-8186-8350-3 SP EP A1 - Dang Van Hung, PY - 1998 KW - Biphase Mark Protocol KW - Duration Calculus KW - Theorem Prover VL - 0 JA - Application of Concurrency to System Design, International Conference on ER -

Dang Van Hung, The United Nations University

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/CSD.1998.657542

The paper presents a model of Biphase Mark Protocols (BMP) using Duration Calculus, which seems to be more general and more intuitive than the others in the literature. With Duration Calculus we can model the behaviour of the bus in a natural way and in more detail. The model makes it possible to specify and verify BMP using PVS/DC tool. The mechanical verification not only ensures the correctness of the protocol, but also helps engineers to choose the optimal values for the parameters given the ratio between the clock rates of the sender and the receiver and the time for changing the signal from high to low and low to high.

Index Terms:

Biphase Mark Protocol, Duration Calculus, Theorem Prover

Citation:

Dang Van Hung, "Modeling and Verification of Biphase Mark Protocolsin Duration Calculus Using PVS," acsd, pp.88, First International Conference on Application of Concurrency to System Design (ACSD'98), 1998

Peer Review Notice | Give Us Feedback

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