A TLA solution to the RPC-Memory Specification Problem

Martín Abadi, Leslie Lamport, Stephan Merz

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.

© Springer-Verlag

Available as:  gzip'ed Postscript 

See also:  other solutions, full proofs, Isabelle proofs

Reference

@InCollection{abadi:memory,
  author =    "Mart\'{\i}n Abadi and Leslie Lamport
               and Stephan Merz",
  title =     "A {TLA} Solution to the {RPC}-{M}emory 
               Specification Problem",
  booktitle = "Formal System Specification:
	       The {RPC}-{M}emory Specification Case Study",
  publisher = "Springer-Verlag",
  year =      1996,
  editor =    "M. Broy and S. Merz and K. Spies",
  volume =    1169,
  series =    "{L}ecture {N}otes in {C}omputer {S}cience",
  pages =     "21--66",
  address =   "Berlin"
}