STEPWISE REFINEMENT OF COMMUNICATING SYSTEMS

The action system formalism [6] is a state-based approach to distribut ed computing. In this paper, it is shown how the action system formali sm may be used to describe systems that communicate with their environ ment through synchronised value-passing. Definitions and rules are pre sented for refining and decomposing such action systems into distribut ed implementations in which internal communication is also based on sy nchronised value-passing. An important feature of the composition rule is that parallel components of a distributed system may be refined in dependently of the rest of the system. Specification and refinement is similar to the refinement calculus approach [4, 26, 28]. The theoreti cal basis for communication and distribution is Hoare's CSP [16]. Use of the refinement and decomposition rules is illustrated by the design of an unordered buffer, and then of a distributed message-passing sys tem.