Equivalence Verification of Timed Transition Models

by M. Lawford and H. Zhang

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.

Download

lawfordm_equivalence.pdf (174k, PDF)

PVS Dump files for examples in paper.

BibTeX Entry

@InProceedings{LawfordZhang:2004,
  author =       {Mark Lawford and Hong Zhang},
  title =        {Equivalence Verification of Timed Transition Models},
  booktitle =    {4th International Conference on Application of Concurrency to System Design
(ACSD 2004)},
  year =         {2004},
  month =        jun,
  publisher =    {IEEE Computer Society},
  pages =        {155-164},
}