Abstract
The Duration Calculus (DC) is an interval temporal logic for reasoning about real-time systems. This paper describes a tool for constructing DC specifications and checking DC proofs. The proof assistant is implemented by encoding the semantics of DC within the higher-order logic of a general-purpose specification and verification environment called PVS. We develop a Gentzen style sequent proof system for DC which we show to be sound with respect to the semantic encoding. We exploit the similarity between the sequent calculus of PVS and the sequent calculus of DC to obtain a DC proof system where the proofs are carried out in PVS at the semantic level, but appear as proofs in the DC proof system. The resulting system, called PC/DC, retains the specification and verification capabilities of PVS within the framework of the Duration Calculus. We present an example of a DC proof whose PC/DC presentation closely follows the lines of the corresponding pencil-and-paper DC arguments. Our approach can be applied to specification logics other than DC.
The work of the first author was partially funded by the Danish Research Academy, SRI International, and ESPRIT BRA 7071: Provably Correct Systems (ProCoS). The second author was partially funded by NSF Grant CCR-930044 and by the US Naval Research Laboratory under contract N00015-92-2177.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
F. Andersen. A Theorem Prover for UNITY in Higher Order Logic. PhD thesis, Technical University of Denmark, Lyngby, Denmark, 1992. Available as ID-TR: 1992-106.
R. S. Boyer and J. S. Moore. A Computational Logic. Academic Press, New York, NY, 1979.
K. Mani Chandy and Jayadev Misra. Parallel Program Design: A Foundation. Addison-Wesley, Reading, MA, 1988.
Ching-Tsun Chou. A sequent formulation of a logic of predicates in HOL. In L. J.M. Claesen and M.J.C. Gordon, editors, Higher Order Logic Theorem Proving and Its Applications, 5th International Workshop, number A-20 in IFIP Transactions, pages 71–80. North-Holland, 1992.
U. Engberg, P. GrØnning, and L. Lamport. Mechanical verfication of concurrent systems with TLA. In Computer Aided Verification 1992, volume 663 of Lecture Notes in Computer Science, pages 44–55. Springer-Verlag, 1992.
M. Engel, A.P. Ravn, and H. Rischel. Timed-Z specification language for real-time systems. ProCoS II, ESPRIT BRA 7071 ID/DTH ME 1/1, Department of Computer Science, Technical University of Denmark, September 1993.
J.H. Gallier. Logic for Computer Science: Foundations of Automatic Theorem Proving. Harper and Row, New York, 1986.
D. Goldschlag. Mechanizing unity. In M. Broy and C. B. Jones, editors, Programming Concepts and Methods. North-Holland, 1990.
M.J.C. Gordon. HOL: A proof generating system for higher-order logic. In G. Birtwistle and P. A. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis, pages 73–128. Kluwer Academic Publishers, Boston, MA, 1988.
M.J.C. Gordon. Mechanizing programming logics in Higher-Order Logic. In G. Birtwistle and P. A. Subrahmanyam, editors, Current Trends in Hardware Verification and Theorem Proving, pages 387–439, New York, NY, 1989. Springer-Verlag.
R. Hale, R. Cardell-Oliver, and J. Herbert. An embedding of timed transition systems in HOL. Formal Methods in System Design, 3(1/2):151–174, August 1993.
J. Halpern, B. Moszkowski, and Z. Manna. A hardware semantics based on temporal intervals. In J. Díaz, editor, 10th ICALP. Automata, Languages and Programming, volume 154 of Lecture Notes in Computer Science, pages 278–291. Springer-Verlag, 1983.
M. R. Hansen and Zhou Chaochen. Semantics and completeness of Duration Calculus. In W.-P. de Roever J. W. de Bakker, C. Huizing and G. Rozenberg, editors, Real-Time: Theory in Practice, REX Workshop, volume 600 of Lecture Notes in Computer Science, pages 209–225. Springer-Verlag, 1992.
M. R. Hansen, Zhou Chaochen, and J. Staunstrup. A real-time duration semantics for circuits. In TAU 1992 ACM/SIGDA Workshop on Timing Issues in the Specification and Synthesis of Digital Systems, March 1992.
C. A. R. Hoare. An axiomatic basis of computer programming. Communications of the ACM, 12(10):576–580, October 1969.
P. Lee, F. Pfenning, J. Reynolds, G. Rollins, and D. Scott. Research on semantically based program-design environments: The ERGO project in 1988. Technical Report CMU-CS-88-118, Department of Computer Science, Carnegie Mellon University, 1988.
B. Moszkowski. A temporal logic for multilevel reasoning about hardware. IEEE Transactions on Computers, 18(2):10–19, 1985.
S. Owre, N. Shankar, and J. M. Rushby. User Guide for the PVS Specification and Verification System, Language, and Proof Checker (Beta Release). Computer Science Laboratory, SRI International, Menlo Park, CA 94025, USA, February 1993. Three volumes.
A.P. Ravn, H. Rischel, and K. M. Hansen. Specifying and verifying requirements of real-time systems. IEEE Trans. Software Engineering, 19(1):41–55, Jan. 1993.
J.U. SkakkebÆk, S. Owre, and N. Shankar. A user guide for the Duration Calculus proof checker, 1994. In Manuscript.
J.U. SkakkebÆk, A.P. Ravn, H. Rischel, and Zhou Chaochen. Development of provably correct systems. In IEEE Workshop on Real-Time Systems, pages 116–121, June 1991.
J.U. SkakkebÆk and N. Shankar. A Duration Calculus proof checker: Using PVS as a semantic framework. Technical Report SRI-CSL-93-10, Computer Science Laboratory, SRI International, Menlo Park, CA 94025, USA, December 1993.
L. Wallen. Automated Deduction in Nonclassical Logics. MIT Press, 1990.
Zhou Chaochen, C. A. R. Hoare, and A. P. Ravn. A calculus of durations. Information Processing Letters, 40(5):269–276, December 1991.
Zhou Chaochen, C. A. R. Hoare, and A. P. Ravn. A calculus of durations, 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
SkakkebÆk, J.U., Shankar, N. (1994). Towards a duration calculus proof assistant in PVS. In: Langmaack, H., de Roever, WP., Vytopil, J. (eds) Formal Techniques in Real-Time and Fault-Tolerant Systems. FTRTFT ProCoS 1994 1994. Lecture Notes in Computer Science, vol 863. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58468-4_189
Download citation
DOI: https://doi.org/10.1007/3-540-58468-4_189
Revised:
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58468-1
Online ISBN: 978-3-540-48984-9
eBook Packages: Springer Book Archive