Text size
  • Small
  • Medium
  • Large
  • Standard
  • Blue text on blue
  • High contrast (Yellow text on black)
  • Blue text on beige

    A Concurrent Language for Refinement

    5th Irish Workshop on Formal Methods

    Dublin, Ireland. 16-17 July 2001


    Jim Woodcock & Ana Cavalcanti


    We present a combination of the well-established formal specification languages Z and CSP; our objective is to provide support for the specification of both data and behaviour aspects of concurrent systems, and a development technique.

    The resulting language, Circus, distinguishes itself in that it is aimed at the calculational refinement of specifications to programs written in a language similar to occam and Handel-C.

    In this paper, we present Circus, the rationale for its design, and a case study in its use.


    PDF filePDF Version of this Paper (238kb)