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 theorie s. 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 of real-time systems, the curr ent implementation in the general purpose SAL model-checker lags well behind st ate of the art real-time model-checkers.
lawford_FI06.pdf (174k, PDF)
@Article{Lawford06, author = {M. Lawford and V. Pantelic and H. Zhang}, title = {Towards Integrated Verification of Timed Transition Models}, journal = {Fundamenta Informaticae}, year = {2006}, OPTkey = {}, volume = {70}, number = {1-2}, pages = {75 - 110}, month = jan, OPTnote = {}, OPTannote = {} }