Formal specification and verification of asynchronous processes in higher-order logic
The work
| Authors | Jeffrey J. Joyce |
|---|---|
| Editors | |
| Type | techreport |
| Year | 1988 |
| Also known as | joyce1988formalb |
| Citekey | joyce1988asynchronous |
Where it appeared
| Publisher | University of Cambridge Computer Laboratory |
|---|---|
| Number in series | UCAM-CL-TR-136 |
| School | University of Cambridge Computer Laboratory |
Identifiers
| DOI | 10.48456/tr-136 |
|---|
Related
| Distinct from | joyce1988formal |
|---|
From bibtex.
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.
A copy is held
pdf, 2.2 MB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-10-22 19:41 UTC |
| Approved by | a person 2026-10-22 22:41 UTC |
Filed under
Cite it as
@techreport{joyce1988asynchronous,
title = {Formal specification and verification of asynchronous processes in higher-order logic},
author = {Jeffrey J. Joyce},
year = {1988},
publisher = {University of Cambridge Computer Laboratory},
school = {University of Cambridge Computer Laboratory},
doi = {10.48456/tr-136},
}
This record lives at https://refs.drheap.org/joyce1988asynchronous/ and will keep
doing so. It used to be called joyce1988formalb, and those addresses still resolve to this one.