The Community for Technology Leaders
2010 10th International Conference on Application of Concurrency to System Design (2004)
Hamilton, Ontario, Canada
June 16, 2004 to June 18, 2004
ISBN: 0-7695-2077-4
pp: 155
Mark Lawford , McMaster University, Hamilton, ON, Canada
Hong Zhang , McMaster University, Hamilton, ON, Canada
ABSTRACT
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.
INDEX TERMS
null
CITATION
Mark Lawford, Hong Zhang, "Equivalence Verification of Timed Transition Models", 2010 10th International Conference on Application of Concurrency to System Design, vol. 00, no. , pp. 155, 2004, doi:10.1109/CSD.2004.1309128
96 ms
(Ver 3.3 (11022016))