Refining Industrial Scale Systems in Circus
Marcel Oliveira, Ana Cavalcanti, Jim Woodcock · Kent Academic Repository (University of Kent) · 2004
Abstract. Circus is a new notation that may be used to specify both data and behaviour aspects of a system, and has an associated refine-ment 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 strat-egy. We describe the refinement and present some new laws that were needed. Our case study makes extensive use of mutual recursion; a sim-plified notation for specifying such systems and proving their refinements is proposed here. 1