Abstract
We model the interaction of a synchronous process with an asynchronous memory process using a four-phase “handshaking” protocol. This example demonstrates the use of higher-order logic to reason about the behaviour of synchronous systems such as microprocessors which communicate requests to asynchronous devices and then wait for unpredictably long periods until these requests are answered. Experience with this example suggests that higherorder logic may also be a suitable formalism for reasoning about more abstract forms of concurrency.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
A. Clements, Microprocessor Systems Design, PWS Publishers, Boston, 1987.
A. Cohn and M. Gordon, “A Mechanized Proof of Correctness of a Simple Counter”, Technical Report No. 94, Computer Laboratory, University of Cambridge, July 1986.
A. Cohn, “A Proof of Correctness of the Viper Microprocessor: The First Level”, VLSI Specification, Verification and Synthesis, Proceedings of the Workshop on Hardware Verification, Calgary, Canada, 12–16 January 1987, G. Birtwistle and P. Subrahmanyam, eds., 1987.
I. Dhingra, “Formal Validation of an Integrated Circuit Design Style”, VLSI Specification, Verification and Synthesis, Proceedings of the Workshop on Hardware Verification, Calgary, Canada, 12–16 January 1987, G. Birtwistle and P. Subrahmanyam, eds., 1987.
M. Gordon, R. Milner and C. Wadsworth. Edinburgh LCF: A Mechanised Logic of Computation, Lecture Notes in Computer Science, Springer-Verlag, 1979.
M. Gordon, “Why Higher-Order Logic is a Good Formalism for Specifying and Verifying Hardware”, Formal Aspects of VLSI Design, Proceedings of the 1985 Edinburgh Conference on VLSI, G.J. Milne and P. Subrahmanyam, eds., North-Holland, Amsterdam, 1986.
M. Gordon, “A Proof Generating System for Higher-Order Logic”, VLSI Specification, Verification and Synthesis, Proceedings of the Workshop on Hardware Verification, Calgary, Canada, 12–16 January 1987, G. Birtwistle and P. Subrahmanyam, eds., 1987.
P. Henderson, Functional Programming, Prentice-Hall, 1980.
J. Herbert, “Application of Formal Methods to Digital System Design”, Ph.D. Thesis, Computer Laboratory, Cambridge University, December 1986.
S. Hill, “Simulating Digital Circuits in Miranda”, University of Kent, 1986.
C. Hoare, Communicating Sequential Processes, Prentice-Hall, 1985.
W. Hunt, “FM8501: A Verified Microprocessor”, PhD Thesis, Institute for Computer Science, University of Texas at Austin, 1986.
J. Joyce, G. Birtwistle, and M. Gordon, “Proving a Computer Correct in Higher Order Logic”, Technical Report No. 100, Computer Laboratory, University of Cambridge, December 1986.
J. Joyce, Ph.D. Research Progress Report, Computer Laboratory, University of Cambridge, December 1987.
J. Joyce, “Formal Specification and Verification of Microprocessor Systems”, EUROMICRO ′88, Proceedings of the 14th Symposium on Microprocessing and Microprogramming, Zurich, Switzerland, 29 August — 1 September, 1988, S. Winter and H. Schumny, eds., North-Holland, 1988.
J. Joyce, “Formal Specification and Verification of Asynchronous Processes in Higher-Order Logic (Full-Length Version)”, Technical Report No. 136, Computer Laboratory, University of Cambridge, 1988.
R. Milner, A Calculus of Communicating Systems, Lecture Notes in Computer Science, Springer-Verlag, 1980.
C. Seitz, “System Timing”, Chapter 7 in Introduction to VLSI Systems, C. Mead and L. Conway, Addison-Wesley, Reading, Massachusetts, 1980.
Paulson, L., Logic and Computation, Cambridge University Press, Cambridge, 1987.
C. Pygott, “Electrical, Environmental and Timing Specification of the Viper Microprocessor”, Memorandum No. 3753 (Unclassified), RSRE (Royal Signals and Radar Establishment), British Ministry of Defense, December 1984.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1990 Springer-Verlag London
About this paper
Cite this paper
Joyce, J.J. (1990). Formal Specification and Verification of Asynchronous Processes in Higher-Order Logic. In: Rattray, C. (eds) Specification and Verification of Concurrent Systems. Workshops in Computing. Springer, London. https://doi.org/10.1007/978-1-4471-3534-0_19
Download citation
DOI: https://doi.org/10.1007/978-1-4471-3534-0_19
Publisher Name: Springer, London
Print ISBN: 978-3-540-19581-8
Online ISBN: 978-1-4471-3534-0
eBook Packages: Springer Book Archive