Luming Lai and J W Sanders
March 1995, 15pp.
A refinement calculus is introduced to support the top-down development of concurrent systems of a type which abstracts occam's communication structure. The main idea is to use the weakest-environment concept to decompose a concurrent system R into its communicating components: given one component P of R, and a communication interface between P and its partner Q, the weakest possible Q is calculated which, in parallel with P, achieves R. The development of R is thereby decomposed into the development of its components. Laws to support such developments are given in terms of combinators of occam-like CSP, and proved valid within a predicate version of the failures model. The calculus is demonstrated on a simple example.