University | Computer Science  

      Circus Family 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.



       Department of Computer Science

       University of York, Deramore Lane, York, YO10 5GH, UK

       Tel: 01904 325500 | Fax:01904 325599                                                                                                                     Last updated on 05 March 2012