%T Refining Industrial Scale Systems in Circus
%A  Marcel Oliveira,  Ana Cavalcanti,  Jim Woodcock
%E Ian R. East, David Duce, Mark Green,  Jeremy M. R. Martin, Peter H. Welch
%B Communicating Process Architectures 2004
%X Circus is a new notation that may be used to specify both
   data and behaviour aspects of a system, and has an
   associated refinement calculus. Although a few case studies
   are already available in the literature, the industrial fire
   control system presented in this paper is, as far as we
   know, the largest case study on the Circus refinement
   strategy. We describe the refinement and present some new
   laws that were needed. Our case study makes extensive use of
   mutual recursion; a simplified notation for specifying such
   systems and proving their refinements is proposed here.