Mechanical verification of timed automata: a case study
- 23 December 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
The paper reports the results of a case study on the feasibility of developing and applying mechanical methods, based on the proof system PVS, to prove propositions about real time systems specified in the Lynch-Vaandrager timed automata model. In using automated provers to prove propositions about systems described by a specific mathematical model, both the proofs and the proof process can be simplified by exploiting the spectral properties of the mathematical model. The paper presents the PVS specification of three theories that underlie the timed automata model, a template for specifying timed automata models in PVS and an example of its instantiation, and both hand proofs and the corresponding PVS proofs of two propositions. It concludes with a discussion of our experience in applying PVS to specify and reason about real time systems modeled as timed automata.Keywords
This publication has 8 references indexed in Scilit:
- Mechanical verification of timed automata: a case studyPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Forward and Backward SimulationsInformation and Computation, 1996
- Formal verification for fault-tolerant architectures: prolegomena to the design of PVSIEEE Transactions on Software Engineering, 1995
- Simulation techniques for proving properties of real-time systemsPublished by Springer Nature ,1994
- Towards a duration calculus proof assistant in PVSPublished by Springer Nature ,1994
- The generalized railroad crossing: a case study in formal verification of real-time systemsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1994
- Symbolic Model CheckingPublished by Springer Nature ,1993
- Using mappings to prove timing propertiesDistributed Computing, 1992