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}
}