Equivalence Verification of Timed Transition Models

	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 Mark Lawford Articles by Hong Zhang

Fourth International Conference on Application of Concurrency to System Design (ACSD'04)

Hamilton, Ontario, Canada

June 16-June 18

ISBN: 0-7695-2077-4

	ASCII Text	x
	Mark Lawford, Hong Zhang, "Equivalence Verification of Timed Transition Models," Application of Concurrency to System Design, International Conference on, pp. 155, Fourth International Conference on Application of Concurrency to System Design (ACSD'04), 2004.

	BibTex	x
	@article{ 10.1109/CSD.2004.1309128, author = {Mark Lawford and Hong Zhang}, title = {Equivalence Verification of Timed Transition Models}, journal ={Application of Concurrency to System Design, International Conference on}, volume = {0}, year = {2004}, isbn = {0-7695-2077-4}, pages = {155}, doi = {http://doi.ieeecomputersociety.org/10.1109/CSD.2004.1309128}, 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 - Equivalence Verification of Timed Transition Models SN - 0-7695-2077-4 SP EP A1 - Mark Lawford, A1 - Hong Zhang, PY - 2004 KW - null VL - 0 JA - Application of Concurrency to System Design, International Conference on ER -

Mark Lawford, McMaster University, Hamilton, ON, Canada

Hong Zhang, McMaster University, Hamilton, ON, Canada

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

This paper describes how the Timed Automata Modeling Environment (TAME) has been modified to provide a formal model for Time Transition Models (TTMs) in the PVS proof checker. State-event equivalences (extensions of Milner's observation equivalences) are also formalized in PVS for state-event labeled transition systems (SELTS), the underlying semantic model of TTMs. These theories are used to verify a real-time control system.

Citation:

Mark Lawford, Hong Zhang, "Equivalence Verification of Timed Transition Models," acsd, pp.155, Fourth International Conference on Application of Concurrency to System Design (ACSD'04), 2004

Peer Review Notice | Give Us Feedback

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