Advertisement

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.

Keywords

Inference Rule Decision Procedure Proof System Sequent Calculus Proof Obligation 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    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.Google Scholar
  2. 2.
    R. S. Boyer and J. S. Moore. A Computational Logic. Academic Press, New York, NY, 1979.Google Scholar
  3. 3.
    K. Mani Chandy and Jayadev Misra. Parallel Program Design: A Foundation. Addison-Wesley, Reading, MA, 1988.Google Scholar
  4. 4.
    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.Google Scholar
  5. 5.
    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.Google Scholar
  6. 6.
    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.Google Scholar
  7. 7.
    J.H. Gallier. Logic for Computer Science: Foundations of Automatic Theorem Proving. Harper and Row, New York, 1986.Google Scholar
  8. 8.
    D. Goldschlag. Mechanizing unity. In M. Broy and C. B. Jones, editors, Programming Concepts and Methods. North-Holland, 1990.Google Scholar
  9. 9.
    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.Google Scholar
  10. 10.
    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.Google Scholar
  11. 11.
    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.Google Scholar
  12. 12.
    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.Google Scholar
  13. 13.
    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.Google Scholar
  14. 14.
    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.Google Scholar
  15. 15.
    C. A. R. Hoare. An axiomatic basis of computer programming. Communications of the ACM, 12(10):576–580, October 1969.Google Scholar
  16. 16.
    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.Google Scholar
  17. 17.
    B. Moszkowski. A temporal logic for multilevel reasoning about hardware. IEEE Transactions on Computers, 18(2):10–19, 1985.Google Scholar
  18. 18.
    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.Google Scholar
  19. 19.
    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.Google Scholar
  20. 20.
    J.U. SkakkebÆk, S. Owre, and N. Shankar. A user guide for the Duration Calculus proof checker, 1994. In Manuscript.Google Scholar
  21. 21.
    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.Google Scholar
  22. 22.
    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.Google Scholar
  23. 23.
    L. Wallen. Automated Deduction in Nonclassical Logics. MIT Press, 1990.Google Scholar
  24. 24.
    Zhou Chaochen, C. A. R. Hoare, and A. P. Ravn. A calculus of durations. Information Processing Letters, 40(5):269–276, December 1991.Google Scholar
  25. 25.
    Zhou Chaochen, C. A. R. Hoare, and A. P. Ravn. A calculus of durations, 1992.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1994

Authors and Affiliations

  • Jens Ulrik SkakkebÆk
    • 1
  • Natarajan Shankar
    • 2
  1. 1.Department of Computer ScienceTechnical University of DenmarkLyngbyDenmark
  2. 2.Computer Science LaboratorySRI InternationalMenlo ParkUSA

Personalised recommendations