2010 10th International Conference on Application of Concurrency to System Design (2004)
Hamilton, Ontario, Canada
June 16, 2004 to June 18, 2004
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.
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