The RPC-Memory Case Study: A Synopsis

Manfred Broy, Stephan Merz, Katharina Spies
Abstract
The RPC-Memory specification problem was proposed by Broy and Lamport as a case study in the formal design of distributed and concurrent systems. The idea was to use it as a basis for comparing various approaches to formal specification, refinement, and verification.

This article attempts to classify the solutions contained in the proceedings volume. It does not attempt to provide an in-depth analysis of the solutions to the case study. Nevertheless, we hope that our classification can be helpful to researchers and even practicing software engineers who try to apply formal methods to concrete problems, and can perhaps even indicate links between formal methods developed from different theoretical backgrounds. On the other hand, we are aware that our subjective backgrounds and predilections have influenced the presentation of the contributions in this overview. Any misrepresentations are entirely our fault.

© Springer-Verlag
Available as:  gzip'ed Postscript 
See also:  RPC-Memory Case Study
Reference
@InCollection{broy:synopsis,
  author =    {Manfred Broy and Stephan Merz and Katharina Spies},
  title =     {The {RPC}-{M}emory Case Study: A Synopsis},
  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,
  pages =     "5--20",
  series =    {{L}ecture {N}otes in {C}omputer {S}cience}
}

Stephan Merz
Last modified: Mon Feb 17 14:42:30 MET 2003