Chapter PDF
References
Dimitri Bertsekas and Robert Gallagher. Data Networks. Prentice-Hall International, Englewood Cliffs, NJ, 1987.
A. Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5, 1940.
Rachel Cardell-Oliver. Formal verification of real-time protocols using higher order logic. Technical Report 206, University of Cambridge Computer Laboratory, August 1990.
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.
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.
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.
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.
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.
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.
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.
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.
Ben Moszkowski. Executing Temporal Logic Programs. Cambridge University Press, 1986.
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.
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.
Faran Moller and Chris Tofts. A Temporal Calculus of Communicating Systems, pages 401–415. Springer Verlag, August 1990. Lecture Notes in Computer Science 458.
A. Udaya Shankar. Verified data transfer protocols with variable flow control. ACM Transactions on Computer Systems, 7(3):281–316, August 1989.
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.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cardell-Oliver, R. (1991). Using higher order logic for modelling real-time protocols. In: Abramsky, S., Maibaum, T.S.E. (eds) TAPSOFT '91. TAPSOFT 1991. Lecture Notes in Computer Science, vol 494. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3540539816_71
Download citation
DOI: https://doi.org/10.1007/3540539816_71
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-53981-0
Online ISBN: 978-3-540-46499-0
eBook Packages: Springer Book Archive