Abstract
In this paper we present our pvs implementation of a linear temporal logic verification system. The system includes a set of theories defining a temporal logic, a number of proof rules for proving soundness and response properties, and strategies which aid in conducting the proofs. In addition to implementing a framework for existing rules, we have also derived new methods which are particularly useful in a deductive ltl system. A distributed rank rule for the verification of response properties in parameterized systems is presented, and a methodology is detailed for reducing compassion requirements to justice requirements (strong fairness to weak fairness). Special attention has been paid to the verification of unbounded systems — systems in which the number of processes is unbounded — and our verification rules are appropriate to such systems.
This research was supported in part by the John von Neumann Minerva Center for Verification of Reactive Systems, the European Community IST projects “Omega” and “Advance”, the Israel Science Foundation (grant 106/02-1), and NSF grant CCR-0205571.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
J. Crow, S. Owre, J. Rushby, N. Shankar, and M. Srivas. A tutorial introduction to PVS. Presented at WIFT’ 95: Workshop on Industrial-Strength Formal Specification Techniques, Boca Raton, Florida, Apr. 1995. Available, with specification files, at http://www.csl.sri.com/wift-tutorial.html.
Y. Kesten and A. Pnueli. Control and data abstractions: The cornerstones of practical formal verification. Software Tools for Technology Transfer, 2(1):328–342, 2000.
L. Lamport. A new solution of Dijkstra’s concurrent programming problem. Comm. ACM, 17(8):453–455, 1974.
Z. Manna, A. Anuchitanukul, N. Bjørner, A. Browne, E. Chang, M. Colón, L. D. Alfaro, H. Devarajan, H. Sipma, and T. Uribe. STeP: The Stanford Temporal Prover. Technical Report STAN-CS-TR-94-1518, Dept. of Comp. Sci., Stanford University, Stanford, California, 1994.
Z. Manna and A. Pnueli. Completing the temporal picture. Theor. Comp. Sci., 83(1):97–130, 1991.
Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, New York, 1995.
K. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Boston, 1993.
S. Owre, N. Shankar, J. Rushby, and D. Stringer-Calvert. PVS System Guide. Menlo Park, CA, November 2001.
E. Sedletsky, A. Pnueli, and M. Ben-Ari. Formal verification of the Ricart-Agrawala algorithm. In S. Kapoor and S. Prasad, editors, FST TCS 2000: Foundations of Software Technology and Theoretical Computer Science, volume 1974 of Lect. Notes in Comp. Sci., pages 325-335. Springer-Verlag, 2000.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Pnueli, A., Arons, T. (2003). tlpvs: A pvs-Based ltl Verification System. In: Dershowitz, N. (eds) Verification: Theory and Practice. Lecture Notes in Computer Science, vol 2772. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39910-0_26
Download citation
DOI: https://doi.org/10.1007/978-3-540-39910-0_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21002-3
Online ISBN: 978-3-540-39910-0
eBook Packages: Springer Book Archive