Computer Laboratory

Technical reports

Formal specification and verification of asynchronous processes in higher-order logic

Jeffrey J. Joyce

June 1988, 45 pages

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. We also describe how our model could be revised to include some of the detailed timing requirements found in real systems such as the M68000 microprocessor. One enhancement uses non-determinism to model minimum setup times for asynchronous inputs. Experience with this example suggests that higher-order logic may also be a suitable formalism for reasoning about more abstract forms of concurrency.

Full text

PDF (2.3 MB)

BibTeX record

@TechReport{UCAM-CL-TR-136,
  author =	 {Joyce, Jeffrey J.},
  title = 	 {{Formal specification and verification of asynchronous
         	   processes in higher-order logic}},
  year = 	 1988,
  month = 	 jun,
  url = 	 {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-136.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  number = 	 {UCAM-CL-TR-136}
}