×

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].

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)

Software:

MASCOT; PVS
PDFBibTeX XMLCite
Full Text: Link