Tools
A wide variety of tools haven been well developed to support refinement, type checking and transformation of Circus programs.
ProofPower is a suite of tools supporting specification and proof in Higher Order Logic (HOL) and in the Z notation. By means of embedding the theories (relations, designs, reactive processes) of UTP in the theorem prover ProofPower-Z, formal proofs can be mechanically constructed. This work also provides a fundamental support for the refinement of Circus specifications.
CRefine is a tool that can be used throughout the refinement of concurrent systems in a calculational approach. In other word, it verifies Circus specifications purely by applying various well-proved refinement laws. CRefine is implemented in Java.
This tool is a syntax type checker for Circus specifications, which is implemented in Java.
JCircus is a tool that can automatically translate Circus programs into Java, for the purpose of animation and simulation. It is based on a translation strategy that uses the JCSP library to implement some of the CSP constructs of Circus.
ClawCircus is a collection of Java-based tools with the primary function of generating Circus models from Simulink diagrams.
A Circus Parser in Community Z Tools.