Mechanical Verification of Timed Automata: A Case Study
Abstract
This report describes 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. Because both specifications and methods of reasoning about them tend to be repetitive, the use of a standard template for specifications, accompanied by repetitive, the use of a standard template for specifications, accompanied by standard shared theories and standard proof strategies or tactics, if often feasible. Presented are 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. Both hand proofs and the corresponding PVS proofs of two propositions are provided to illustrate how these can be made parallel at different degrees of granularity. Our experience in applying PVS to specify and reason about real-time systems modeled as timed automata is also discussed. The methods for reasoning about timed automata in PVS developed in the study have evolved into a system called TAME (Timed Automata Modeling Environment). A summary of recent developments regarding TAME is provided. A shorter version of the report was presented at the 1997 Real-Time Applications Symposium.
Document Details
- Document Type
- Technical Report
- Publication Date
- Dec 31, 1998
- Accession Number
- ADA359891
Entities
People
- Constance Heitmeyer
- Myla M. Archer
Organizations
- United States Naval Research Laboratory