Equivalence verification of timed transition models

Author

Lawford, Mark ; Zhang, Hong

Author_Institution

Software Quality Res. Lab., McMaster Univ., Hamilton, Ont., Canada

fYear

2004

fDate

16-18 June 2004

Firstpage

155

Lastpage

164

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Application of Concurrency to System Design, 2004. ACSD 2004. Proceedings. Fourth International Conference on

Print_ISBN

0-7695-2077-4

Type

conf

DOI

10.1109/CSD.2004.1309128

Filename

1309128