Sciweavers

FUIN
2006

Towards Integrated Verification of Timed Transition Models

13 years 3 months ago
Towards Integrated Verification of Timed Transition Models
Abstract. This paper describes an attempt to combine theorem proving and model-checking to formally verify real-time systems in a discrete time setting. The Timed Automata Modeling Environment (TAME) has been modified to provide a formal model for Time Transition Models (TTMs) in the PVS proof checker. Strong and weak state-event observation equivalences are formalized in PVS for state-event labeled transition systems (SELTS), the underlying semantic model of TTMs. The state-event equivalences form the basis of truth value preserving abstractions for a real-time temporal logic. When appropriate restrictions are placed upon the TTMs, their PVS models can be easily translated into input for the SAL model-checker. A simple real-time control system is specified and verified using these theories. While these preliminary results indicate that the combination of PVS and SAL could provide a useful environment to perform equivalence verification, model-checking and compositional model reduction...
Mark Lawford, Vera Pantelic, Hong Zhang
Added 12 Dec 2010
Updated 12 Dec 2010
Type Journal
Year 2006
Where FUIN
Authors Mark Lawford, Vera Pantelic, Hong Zhang
Comments (0)