The growing interest in a scientifically based method for the
specification, refinement, implementation, and verification of distributed,
concurrent, interacting systems is caused by the wide areas of their
applications. These include operating systems, computer networks,
telecommunications, wide-area nets, and all kinds of reactive systems embedded in
technical devices. The subject of distributed interactive systems also leads to intricate
theoretical problems, which have stimulating relationships to many areas of
mathematics, logics, and electrical engineering. Over the
years a large variety of different approaches have been
developed. This richness, reflecting the large amount of creativity and new
ideas of researchers, provides us with an overwhelming variety of aspects for
the design and the analysis of systems.
Case studies can provide a basis for comparing, relating, and evaluating various
approaches. They provide a very
valuable opportunity to improve the possibilities to compare and further
develop the different methods. First of all, they provide a real basis to evaluate
approaches. And, more than the examples presented by the various methods by
themselves, they really test how far a method is able to adapt to particular
requirements and methodological needs.
Based on these considerations
Manfred Broy
and
Leslie Lamport decided in fall 1993
that they again do an experiment by providing a further case study.
After several meetings and discussions, they present
the RPC-Memory Specification
Problem Statement as an example which makes sure that several steps of
development were part of the exercise to look not only at the pure specification task
but also at refinement and verification.
The problem statement was sent out together with the
invitations to a workshop on " Specification and
Refinement of Reactive Systems" in
Schloss Dagstuhl.
After the workshop, which took place in September 1994,
through several iterations written versions of
the presented
solutions are collected. All solutions went through two
stages of a careful cross-refereeing process and
finally came to the text presented in the
LNCS 1169.
The volume includes a short
synopsis paper in which the approaches were roughly
explained and related.
Table of Contents and Abstracts