Refinement and decomposition of value-passing action systems in the refinement calculus

The action system formalism [3] is a state-based approach to distributed computing. In this paper, it is shown how the action system formalism may be used to describe systems that interact with their environment through synchronised value-passing. Definitions and rules are presented for refining and decomposing such action systems into distributed implementations in which internal communication is also based on synchronised value-passing. Specification and refinement is similar to the refinement calculus approach [1, 10, 12]. The theoretical basis for communication and distribution is Hoare's CSP [6]. Use of the refinement and decomposition rules is illustrated by the design of an unordered buffer