Henderson, N.; Paynter, S. E. The formal classification and verification of Simpson’s 4-slot asynchronous communication mechanism. (English) Zbl 1064.68534 Eriksson, Lars-Henrik (ed.) et al., FME 2002: Formal methods - getting IT right. International symposium of formal methods Europe, Copenhagen, Denmark, July 22–24, 2002. Proceedings. Berlin: Springer (ISBN 3-540-43928-5). Lect. Notes Comput. Sci. 2391, 350-369 (2002). Summary: This paper critiques and extends Lamport’s taxonomy of asynchronous registers. This extended taxonomy is used to characterise Simpson’s 4-slot asynchronous communication mechanism (ACM). 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.For the entire collection see [Zbl 0997.68675]. Cited in 5 Documents MSC: 68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) 68Q60 Specification and verification (program logics, model checking, etc.) 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) Keywords:asynchronous communication; reification; refinement; retrieve relation Software:MASCOT; PVS PDFBibTeX XMLCite \textit{N. Henderson} and \textit{S. E. Paynter}, Lect. Notes Comput. Sci. 2391, 350--369 (2002; Zbl 1064.68534) Full Text: Link