Skip to main content

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: East, Ian R. and Martin, Jeremy and Welch, Peter H. and Duce, David and Green, Mark, eds. Communicating Process Architectures 2004. Concurrent Systems Engineering Series . IOS Press, pp. 281-309. ISBN 978-1-58603-458-0.


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: Book section
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: 28 Aug 2019 09:03 UTC
Resource URI: (The current URI for this page, for reference purposes)
  • Depositors only (login required):


Downloads per month over past year