CRefine: Support for the Circus Refinement Calculus

Circus specifications combine both data and behavioral aspects of concurrent systems using a combination of CSP, Z, and Dijkstrapsilas command language. Its associated refinement theory and calculus distinguishes itself from other such combinations. Recently, tools for Circus like a parser, a type-checker, a model-checker, and a translator to Java have been developed. Nevertheless, tool support for the circus refinement calculus has only been prototyped. In this paper, we present CRefine, a tool that can be used throughout the refinement of concurrent systems in a calculational approach. Its functionalities are described using a simple case study. Furthermore, we also describe CRefinepsilas architecture and its integration to the CZT framework.