Refining Industrial Scale Systems in Circus

Oliveira, Marcel V. M. and Cavalcanti, Ana L. C. and Woodcock, Jim (2004) Refining Industrial Scale Systems in Circus. In: Communicating Process Architectures 2004, Sep 05-08, 2004, Oxford Brooks Univ, Oxford, England. (Full text available)

Download (363kB) Preview


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.

Item Type: Conference or workshop item (Paper)
Uncontrolled keywords: Refinement Calculus, Circus, Case Study
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Sciences > School of Computing > Systems Architecture Group
Depositing User: Mark Wheadon
Date Deposited: 24 Nov 2008 18:01 UTC
Last Modified: 21 May 2014 10:54 UTC
Resource URI: (The current URI for this page, for reference purposes)
  • Depositors only (login required):


Downloads per month over past year