Abstract
We present an approach to the verification of the real-time behavior of concurrent programs and describe its mechanization using the PVS proof checker. Our approach to real-time behavior extends previous verification techniques for concurrent programs by proposing a simple model for real-time computation and introducing a new operator for reasoning about absolute time. This model is formalized and mechanized within the higher-order logic of PVS. The interactive proof checker of PVS is used to develop the proofs of two illustrative examples: Fischer's real-time mutual exclusion protocol and a railroad crossing controller.
This work was supported by National Aeronautics and Space Administration Langley Research Center and the US Naval Research Laboratory under contract NAS1-18969 and by the US Naval Research Laboratory contract N00015-92-C-2177. Connie Heitmeyer (NRL) suggested the railroad crossing example. Sam Owre (SRI) assisted with the use of PVS. The helpful comments of John Rushby (SRI), Jayadev Misra (University of Texas at Austin), Ralph Jeffords (Locus, Inc.), Jens Skakkebæk (Technical University of Denmark), and the anonymous referees are gratefully acknowledged.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
R. Alur and T. A. Henzinger. Logics and models of real time: A survey. In de Bakker et al. [dBHdRR91], pages 74–106.
M. Abadi and L. Lamport. An old-fashioned recipe for real time. In de Bakker et al. [dBHdRR91], pages 1–27.
Zhou Chaochen, C. A. R. Hoare, and A. P. Ravn. A calculus of durations. Information Processing Letters, 40(5):269–276, 1992.
K. Mani Chandy and Jayadev Misra. Parallel Program Design: A Foundation. Addison-Wesley, Reading, MA, 1988.
J. A. Carruth and J. Misra. Proof of a real-time mutual-exclusion algorithm. Notes on UNITY: 32–92, 1992.
J. W. de Bakker, C. Huizing, W.P. de Roever, and G. Rozenberg, editors. Real Time: Theory in Practice, volume 600 of Lecture Notes in Computer Science, REX Workshop, Mook, The Netherlands, June 1991. Springer Verlag.
T. A. Henzinger, Z. Manna, and A. Pnueli. Timed transition systems. In de Bakker et al. [dBHdRR91], pages 226–251.
Farnam Jahanian and Aloysius Ka-Lau Mok. Safety analysis of timing properties in real-time systems. IEEE Transactions on Software Engineering, SE-12(9):890–904, September 1986.
Leslie Lamport. A fast mutual exclusion algorithm. ACM Transactions on Computer Systems, 5(1):1–11, February 1987.
Leslie Lamport. The temporal logic of actions. Technical Report 57, DEC Systems Research Center, Palo Alto, CA, April 1990. A substantially modified version is available dated January 1991.
O. Maler, Z. Manna, and A. Pnueli. From timed to hybrid systems. In de Bakker et al. [dBHdRR91], pages 447–484.
S. Owre, J. M. Rushby, and N. Shankar. PVS: A prototype verification system. In Deepak Kapur, editor, 11th International Conference on Automated Deduction (CADE), volume 607 of Lecture Notes in Artificial Intelligence, pages 748–752, Saratoga, NY, 1992. Springer Verlag.
A. Pnueli. The temporal logic of programs. In Proc. 18th Symposium on Foundations of Computer Science, pages 46–57, Providence, RI, November 1977. ACM.
F. B. Schneider, B. Bloom, and K. Marzullo. Putting time into proof outlines. In de Bakker et al. [dBHdRR91], pages 618–639.
N. Shankar. Mechanized verification of real-time systems using PVS. Technical Report SRI-CSL-12, SRI International Computer Science Laboratory, Menlo Park, CA, 1992.
J. U. Skakkebæk, A. P. Ravn, H. Rischel, and Zhou Chaochen. Specification of embedded, real-time systems. In Proceedings of 1992 Euromicro Workshop on Real-Time Systems. IEEE Computer Society Press, 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Shankar, N. (1993). Verification of real-time systems using PVS. In: Courcoubetis, C. (eds) Computer Aided Verification. CAV 1993. Lecture Notes in Computer Science, vol 697. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56922-7_23
Download citation
DOI: https://doi.org/10.1007/3-540-56922-7_23
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56922-0
Online ISBN: 978-3-540-47787-7
eBook Packages: Springer Book Archive