A Concurrent Language for Refinement

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.

Content

Author and article information

Contributors

Jim Woodcock

Ana Cavalcanti

Conference

Publication date: July 2001

Publication date (Print): July 2001

Pages: 1-16

Affiliations

[0001]Oxford University/OUCL

Wolfson Building, Parks Road

Oxford OX1 3QD, England

[0002]Centro de Informática/UFPE

P.O. Box 7851

50740-540 Recife - PE Brazil

Article

DOI: 10.14236/ewic/IWFM2001.7

SO-VID: 5c24b659-c914-405e-b198-e3a317bd8ad1

License:

This work is licensed under a Creative Commons Attribution 4.0 Unported License. To view a copy of this license, visit http://creativecommons.org/licenses/by/4.0/

Conference name: 5th Irish Workshop on Formal Methods

Conference acronym: IWFM

Conference number: 5

Conference location: Dublin, Ireland

Conference date: 16-17 July 2001

Conference sponsor: Electronic Workshops in Computing (eWiC)

Conference theme: Irish Workshop on Formal Methods

History

Product

1477-9358 BCS Learning & Development

Self URI (article page): https://www.scienceopen.com/hosted-document?doi=10.14236/ewic/IWFM2001.7

Self URI (journal page): https://ewic.bcs.org/

Studying business & IT? Drive your professional career forwards with BCS books - for a 20% discount click here: shop.bcs.org

A Concurrent Language for Refinement

Abstract