A wide variety of tools haven been well developed to support refinement, type checking and transformation of Circus programs.
This tool is a syntax type checker for Circus specifications, which is implemented in Java.
A Circus Parser in Community Z Tools.
ClawCircus is a collection of Java-based tools with the primary function of generating Circus models from Simulink diagrams.
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.
A verification toolbox for Isabelle/HOL based on Unifying Theories of Programming.
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.
RoboTool supports graphical modelling, validation, and automatic generation of mathematical definitions for proof of properties of RoboChart models, with proof automated using model checking. The RoboChart notation is distinctive in its features that support architectural modelling as well as timed constructs in state machines.
s2c is a tool that reads Stateflow models (in .mdl format) and calculates their Circus semantics.
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.
Department of Computer Science
Deramore Lane, University of York, Heslington, York, YO10 5GH, UK
Tel: 01904 325500 | Fax: 01904 325599
