Title :
Equivalence verification of timed transition models
Author :
Lawford, Mark ; Zhang, Hong
Author_Institution :
Software Quality Res. Lab., McMaster Univ., Hamilton, Ont., 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.
Keywords :
automata theory; bisimulation equivalence; control engineering computing; formal specification; formal verification; industrial control; real-time systems; theorem proving; PVS proof checker; equivalence verification; formal model; observation equivalences; real-time control system; semantic model; state-event equivalences; state-event labeled transition systems; timed automata modeling environment; timed transition models; Automata; Automatic control; Control system synthesis; Control systems; Electrical equipment industry; Industrial control; Real time systems; Software quality; Software systems; Time to market;
Conference_Titel :
Application of Concurrency to System Design, 2004. ACSD 2004. Proceedings. Fourth International Conference on
Print_ISBN :
0-7695-2077-4
DOI :
10.1109/CSD.2004.1309128
