Automatic translation from Circus to Java

Abstract

Circus is a combination of Z and CSP that supports the development of state-rich reactive systems based on refinement. In this paper we present JCircus, a tool that automatically translates 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. The tool generates a simple graphical interface; we present a simple example to demonstrate the translation strategy, and the execution of the resulting program. We discuss the class GeneralChannel, which we designed to support the implementation of multi-synchronisation. We also discuss our improvements to the translation strategy, some limitations of the tool, and our approach to prove the correctness of the multi-synchronisation protocol. © Springer-Verlag Berlin Heidelberg 2006.