Towards Integrated Verification of Timed Transition Models

Issue title: APPLICATION OF CONCURRENCY TO SYSTEM DESIGN (ACSD'04)

Article type: Research Article

Authors: Lawford, Mark | Pantelic, Vera | Zhang, Hong

Affiliations: Software Quality Research Lab, McMaster University, 1280 Main St W. Hamilton ON, L8S 4K1, Canada. E-mails: lawford@mcmaster.ca; pantelv@mcmaster.ca; zhangh5@cas.mcmaster.ca

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 of real-time systems, the current implementation in the general purpose SAL model-checker lags well behind state of the art real-time model-checkers.

Keywords: Real-time, equivalence verification, theorem proving, PVS, model-checking, model reduction, SAL

Journal: Fundamenta Informaticae, vol. 70, no. 1-2, pp. 75-110, 2006