Abstract
A major barrier to more common use of mechanical theorem provers in verifying software designs is the significant distance between proof styles natural to humans and proof styles supported by mechanical provers. To make mechanical provers useful to software designers with some mathematical sophistication but without expertise in mechanical provers, the distance between hand proofs and their mechanized versions must be reduced. To achieve this, we are developing a mechanical prover called TAME on top of PVS. TAME is designed to process proof steps that resemble in style and size the typical steps in hand proofs. TAME's support of more natural proof steps should not only facilitate mechanized checking of hand proofs, but in addition should provide assurance that theorems proved mechanically are true for the reasons expected and also provide a basis for conceptual level feedback when a mechanized proof fails. While infeasible for all applications, designing a prover that can process a set of high-level, natural proof steps for restricted domains should be achievable. In developing TAME, we have had moderate success in defining specialized proof strategies to validate hand proofs of properties of Lynch-Vaandrager timed automata. This paper reports on our successes, the services provided by PVS that support these successes, and some desired enhancements to PVS that would permit us to improve and extend TAME.
This work is funded by the Office of Naval Research. URLs for the authors are http://www.itd.nrl.navy.mil/ITD/5540/personnel/{archer, heitmeyer}. html
Preview
Unable to display preview. Download preview PDF.
References
M. Archer and C. Heitmeyer. Mechanical verification of timed automata: A case study. In Work-In-Progress Proc. 1996 IEEE Read-Time Systems Symp. (RTSS'96), pages 3–6, 1996.
M. Archer and C. Heitmeyer. Mechanical verification of timed automata: A case study. In Proc. 1996 IEEE Real-Time Technology and Applications Symp. (RTAS'96). IEEE Computer Society Press, 1996.
M. Archer and C. Heitmeyer. Verifying hybrid systems modeled as timed automata: A case study. In Hybrid and Real-Time Systems (HART'97), volume 1201 of Lecture Notes in Computer Science, pages 171–185. Springer-Verlag, 1997.
P. Black and P. Windley. Automatically synthesized term denotation predicates: A proof aid. In Higher Order Logic Theorem Proving and Its Applications (HOL'95), volume 971 of Lect. Notes in Comp. Sci., pages 46–57. Springer-Verlag, 1995.
R. Boyer and J. Moore. A Computational Logic. Academic Press, 1979.
S. Brackin. Deciding cryptographic protocol adequacy with HOL. In Higher Order Logic Theorem Proving and Its Applications (HOL'95), volume 971 of Lecture Notes in Computer Science, pages 90–105. Springer-Verlag, 1995.
A. Fekete, N. Lynch, and A. Shvartsman. Specifying and using a partitionable group communication service. in preparation.
M. J. C. Gordon and T. Melham, editors. Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic. Cambridge University Press, 1993.
J. Harrison. A Mizar mode for HOL. In Proc. 9th Intl. Conf. on Theorem Proving in Higher Order Logics (TPHOLs'96), volume 1125 of Lecture Notes in Computer Science, pages 203–220. Springer-Verlag, 1996.
C. Heitmeyer and N. Lynch. The Generalized Railroad Crossing: A case study in formal verification of real-time systems. In Proc., Real-Time Systems Symp., San Juan, Puerto Rico, Dec. 1994.
C. Heitmeyer and N. Lynch. The Generalized Railroad Crossing: A case study in formal verification of real-time systems. Technical Report MIT/LCS/TM-51, Lab. for Comp. Sci., MIT, Cambridge, MA, 1994. Also Technical Report 7619, NRL, Wash., DC 1994.
T. Henzinger and P. Ho. Hytech: The Cornell Hybrid Technology Tool. Technical report, Cornell University, 1995.
R. P. Kurshan. Computer-Aided Verification of Coordinating Processes: the Automata-Theoretic Approach. Princeton University Press, 1994.
G. Leeb and N. Lynch. Proving safety properties of the Steam Boiler Controller: Formal methods for industrial applications: A case study. In J.-R. Abrial, et al., eds., Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control, vol. 1165 of Lect. Notes in Comp. Sci. Springer-Verlag, 1996.
V. Luchangco. Using simulation techniques to prove timing properties. Master's thesis, Massachusetts Institute of Technology, June 1995.
N. Lynch. Simulation techniques for proving properties of real-time systems. In REX Workshop '93, volume 803 of Lecture Notes in Computer Science, pages 375–424, Mook, the Netherlands, 1994. Springer-Verlag.
N. Lynch and F. Vaandrager. Forward and backward simulations — Part II: Timing-based systems. To appear in Information and Computation.
N. Lynch and F. Vaandrager. Forward and backward simulations for timing-based systems. In Proc. of REX Workshop “Real-Time: Theory in Practice”, volume 600 of Lecture Notes in Computer Science, pages 397–446. Springer-Verlag, 1991.
K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.
S. Owre, N. Shankar, and J. Rushby. User guide for the PVS specification and verification system (Draft). Technical report, Computer Science Lab., SRI Intl., Menlo Park, CA, 1993.
P. Rudnicki. An overview of the MIZAR project. In Proc. 1992 Workshop on Types and Proofs for Programs, pages 311–332, June 1992. Also available through anonymous ftp as pub/cs-reports/Bastad92/proc.ps.Z on ftp.cs.chalmers.se.
P. Rudnicki and A. Trybulec. A note on “How to Write a Proof”. In Proc. 1992 Workshop on Types and Proofs for Programs, June 1996. Available through P. Rudnicki's web page at http://www.cs.ualberta.ca/-piotr/Mizar/.
J. Rushby. Private communication. NRL, Jan. 1997.
N. Shankar, S. Owre, and J. Rushby. The PVS proof checker: A reference manual. Technical report, Computer Science Lab., SRI Intl., Menlo Park, CA, 1993.
J. Skakkebaek and N. Shankar. Towards a duration calculus proof assistant in PVS. In Third Intern. School and Symp. on Formal Techniques in Real Time and Fault Tolerant Systems, Lect. Notes in Comp. Sci. 863. Springer-Verlag, 1994.
H. B. Weinberg. Correctness of vehicle control systems: A case study. Master's thesis, Massachusetts Institute of Technology, February 1996.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Archer, M., Heitmeyer, C. (1997). Human-style theorem proving using PVS. In: Gunter, E.L., Felty, A. (eds) Theorem Proving in Higher Order Logics. TPHOLs 1997. Lecture Notes in Computer Science, vol 1275. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0028384
Download citation
DOI: https://doi.org/10.1007/BFb0028384
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63379-2
Online ISBN: 978-3-540-69526-4
eBook Packages: Springer Book Archive