The Formal Classification and Verification of Simpson's 4-slot Asynchronous Communication Mechanism

  1. Lookup NU author(s)
  2. Neil Henderson
  3. Dr Stephen Paynter
Author(s)Henderson N, Paynter S
Publication type Report
Series TitleDepartment of Computing Science Technical Report Series
Year2002
Legacy DateJanuary 2002
Report Number756
Pages54
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.
InstitutionDepartment of Computing Science, University of Newcastle upon Tyne
Place PublishedNewcastle upon Tyne
URLhttp://www.cs.ncl.ac.uk/publications/trs/papers/756.pdf
ActionsLink to this publication