The Formal Classification and Verification of Simpson's 4-slot Asynchronous Communication Mechanism
- Lookup NU author(s)
- Neil Henderson
- Dr Stephen Paynter
|
|
|
|
| Author(s) | | Henderson N, Paynter S |
| Publication type | | Report |
| Series Title | | Department of Computing Science Technical Report Series |
| Year | | 2002 |
| Date | | January 2002 |
| Report Number | | 756 |
| Pages | | 54 |
|
|
|
| Full text is available for this publication: |
|
|
|
|
| This paper critiques and extends Lamport's taxonomy of asynchroous registers. This extended taxonomy is used to characterise Simpson's 4-slot asynchronous communication mechanism. A formalisation of the Lamport atomic property and Simpson's original 4-Slot implementation is given in the PVS logic. We prove that the 4-slot is atomic using Nipkow's retrieve relation proof rules. A description is given of the formal proofs, which have been discharged in the PVS theorem prover. |
|
|
|
| Institution | | Department of Computing Science, University of Newcastle upon Tyne |
| Place Published | | Newcastle upon Tyne |
| URL | | http://www.cs.ncl.ac.uk/publications/trs/papers/756.pdf |
| Actions | |  |
