Circus combines Z and CSP with a refinement calculus to support development of state-rich reactive systems. It includes a theory and a technique of refinement that support the calculation of concurrent implementations from centralised specifications. The semantics of Circus is based on Hoare and He's unifying theories of programming.
The development of Circus started in 2000 as a result of collaborative work with the Universidade Federal de Pernambuco, Brazil. Since, then we have had the enthusiastic support of many collaborators from around the world (Ireland, Macau, Brazil) and from British industry. Together, we have investigated both the theoretical underpinnings of an integrated refinement languages and its applications.
Click here for further details of the Circus project.