Circus - Z, CSP and Refinement Calculus

The Circus family of notations has at its core a flexible combination of Z, CSP, Morgan’s specification statements, and Dijkstra’s guarded commands. It is a language for specification, programming, and verification by refinement. Its semantics is based on Hoare and He’s Unifying Theories of Programming.

The design of Circus goes back to 2000, and was motivated by the need for a notation and techniques to reason about designs and implementations of state-rich reactive processes. The best account of the core notation can be found in here, and more in-depth information refers to the documentation.

Over the years, research on Circus has covered many extensions to the core notation and interesting industrial applications. We have versions to cover time, object-orientation, synchronicity, mobility, and sharing. Industrial applications have focused on control systems. Tool support has followed to enable such work.

Many have joined in the effort to provide a fully integrated and sound family of notations to support refinement-based reasoning for modern systems. Most of the Circus group is in the University of York, but there is work being carried out also at the University of Newcastle, and in Brazil, China, France, the USA, Ireland, and Singapore.

Circus is a live notation. We are investing in its use for reasoning about Safety-critical Java programs (SCJ), avionics control systems, and Systems of Systems. We are also defining a testing theory and model-based testing techniques for Circus. Together, we push forward the Circus notation, its UTP model, and its tools. This page gives an overview of what is available and what is going on.

Recent news