| Abstract: | Circus is a new notation that may be used to specify both data and behavioural aspects of a system, and has an associated refinement calculus. In this work, we present rules to translate Circus programs to Java programs that use JCSP, a library that implements Communicating Sequential Processes constructs. These rules can be used as a complement to the Circus algebraic refinement technique, or as a guideline for implementation. They are a link between the results on refinement in the context of Circus and a practical programming language in current use. The rules can also be used as the basis for a tool that mechanises the translation. Although a few case studies are already available in the literature, the industrial fire control system, whose refinement and implementation is discussed in this paper, is, as far as we know, the largest case study on the Circus refinement strategy. |
