A TLA solution to the RPC-Memory Specification Problem
- Abstract
- We present a complete solution to the
Broy-Lamport specification problem.
Our specifications are written in TLA+, a formal language
based on TLA. We give the high levels of structured proofs and
sketch the lower levels, which are sketched
here.
- See also
other solutions,
Isabelle proofs
- Reference
- M. Broy, S. Merz, K. Spies (eds.):
Formal Systems Specification: The RPC-Memory Specification Case Study.
Berlin etc.: Springer-Verlag, 1996, LNCS 1169, pp. 21-66
BibTeX reference
- Download
(gzip'ped) Postscript
Stephan Merz