Using higher order logic for modelling real-time protocols

  • Rachel Cardell-Oliver
CCPSD Colloquium On Combining Paradigms For Software Development
Part of the Lecture Notes in Computer Science book series (LNCS, volume 494)


  1. [BG87]
    Dimitri Bertsekas and Robert Gallagher. Data Networks. Prentice-Hall International, Englewood Cliffs, NJ, 1987.Google Scholar
  2. [Chu40]
    A. Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5, 1940.Google Scholar
  3. [CO90]
    Rachel Cardell-Oliver. Formal verification of real-time protocols using higher order logic. Technical Report 206, University of Cambridge Computer Laboratory, August 1990.Google Scholar
  4. [GMW79]
    M.J.C. Gordon, A.J.R.G. Milner, and C.P. Wadsworth. Edinburgh LCF: a mechanized logic of Computation, volume 78 of Lecture Notes in Computer Science. Springer Verlag, 1979.Google Scholar
  5. [Gor86]
    M.J.C. Gordon. Why higher-order logic is a good formalism for specifying and verifying hardware. In Formal Aspects of VLSI Design, Proceedings of the 1985 Edinburgh Conference on VLSI, pages 153–177. North Holland, 1986.Google Scholar
  6. [Gor88]
    Mike Gordon. A proof generating system for higher-order logic. In VLSI Specification, Verification and Synthesis, Proceedings of the Workshop on Hardware Verification, Calgary, 12–16 January, 1987, G.M. Birtwistle and P.A. Subrahmanyam, eds. Kluwer International Series in Engineering and Computer Science, SECS35, pages 73–128. Kluwer Academic Publishers, 1988.Google Scholar
  7. [Hal87]
    Roger Hale. Using temporal logic for prototyping: the design of a lift controller. In Temporal Logic in Specification 1987, pages 375–408, 1987. Lecture Notes in Computer Science 398.Google Scholar
  8. [HD86]
    F.K. Hanna and N. Daeche. Specification and verification of digital systems using higher-order predicate logic. IEE Proceedings E, 133 Part E(5):242–254, September 1986.Google Scholar
  9. [JM86]
    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.Google Scholar
  10. [Joy89]
    Jeffrey J. Joyce. Multi-Level Verification of Microprocessor-Based Systems. PhD thesis, Computer Laboratory, University of Cambridge, December 1989. also published as Computer Laboratory Technical Report 195.Google Scholar
  11. [Mel89]
    Thomas F. Melham. Formalizing Abstraction Mechanisms for Hardware Verification in Higher Order Logic. PhD thesis, Computer Laboratory, University of Cambridge, August 1989. also published as Computer Laboratory Technical Report 201.Google Scholar
  12. [Mos86]
    Ben Moszkowski. Executing Temporal Logic Programs. Cambridge University Press, 1986.Google Scholar
  13. [MS87]
    P.M. Melliar-Smith. Extending interval logic to real time systems. In Temporal Logic in Specification 1987, pages 224–242, 1987. Lecture Notes in Computer Science 398.Google Scholar
  14. [MS88]
    Glenn H. MacEwen and David B. Skillicorn. Using Higher Order Logic for Modular Specification of Real-Time Distributed Systems, pages 37–66. Springer Verlag, September 1988. Lecture Notes in Computer Science 331.Google Scholar
  15. [MT90]
    Faran Moller and Chris Tofts. A Temporal Calculus of Communicating Systems, pages 401–415. Springer Verlag, August 1990. Lecture Notes in Computer Science 458.Google Scholar
  16. [Sha89]
    A. Udaya Shankar. Verified data transfer protocols with variable flow control. ACM Transactions on Computer Systems, 7(3):281–316, August 1989.Google Scholar
  17. [SL87]
    A. Udaya Shankar and Simon S. Lam. Time-dependent distributed systems: proving safety, liveness and real-time properties. Distributed Computing, 2(2):61–79, August 1987.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1991

Authors and Affiliations

  • Rachel Cardell-Oliver
    • 1
  1. 1.Computer LaboratoryUniversity of CambridgeCambridgeU.K.

Personalised recommendations