Refinement in Circus

Abstract

We describe refinement in Circus, a concurrent specification language that integrates imperative CSP, Z, and the refinement calculus. Each Circus process has a state and accompanying actions that define both the internal state transitions and the changes in control flow that occur during execution. We define the meaning of refinement of processes and their actions, and propose a sound data refinement technique for process refinement. Refinement laws for CSP and Z are directly relevant and applicable to Circus, but our focus here is on new laws for processes that integrate state and control. We give some new results about the distribution of data refinement through the combinators of CSP. We illustrate our ideas with the development of a distributed system of cooperating processes from a centralised specification.