loading...
Equivalence Verification of Timed Transition Models
Hamilton, Ontario, Canada June 16-June 18
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/CSD.2004.1309128Fourth International Conference on Ap ...
 This Article 
 
Buy PURCHASE ARTICLE: $19
PDF
HTML
Buy IEEE Xplore Subscribers
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
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
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
Usage of this product signifies your acceptance of the Terms of Use.