Fourth International Conference on Application of Concurrency to System Design (ACSD'04) Equivalence Verification of Timed Transition Models Hamilton, Ontario, Canada June 16-June 18 ISBN: 0-7695-2077-4
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. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||