|Title||Mechanical Verification of Timed Automata: A Case Study|
|Publication Type||Conference Paper|
|Year of Publication||1996|
|Authors||Archer, M., and C. L. Heitmeyer|
|Conference Name||996 Real-Time Technology and Applications Symposium|
|Other Numbers||MR 5546-98-8180|
This 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 special properties of the mathematical model. This 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.