Result: Refinement in Circus

Title:
Refinement in Circus
Authors:
SAMPAIO, Augusto, WOODCOCK, Jim, CAVALCANTI, Ana
Source:
FME 2002 : formal methods - getting IT right (Copenhagen, 22-24 July 2002)Lecture notes in computer science. :451-470
Publisher Information:
Berlin: Springer, 2002.
Publication Year:
2002
Physical Description:
print, 21 ref
Original Material:
INIST-CNRS
Subject Terms:
Computer science, Informatique, Sciences exactes et technologie, Exact sciences and technology, Sciences appliquees, Applied sciences, Informatique; automatique theorique; systemes, Computer science; control theory; systems, Informatique théorique, Theoretical computing, Théorie programmation, Programming theory, Affinement, Refinement, Afinamiento, Commande processus, Process control, Control proceso, Langage impératif, Imperative language, Lenguaje imperativo, Langage spécification, Specification language, Lenguaje especificación, Satisfaction contrainte, Constraint satisfaction, Satisfaccion restricción, Simultanéité informatique, Concurrency, Simultaneidad informatica, Système réparti, Distributed system, Sistema repartido, Théorie programmation, Programming theory, CIRCUS process, Distribution donnée, Data distribution
Document Type:
Conference Conference Paper
File Description:
text
Language:
English
Author Affiliations:
Centro de Informática/UFPE, Recife PE, Brazil
University of Kent, Canterbury, United Kingdom
ISSN:
0302-9743
Access URL:
http://pascal-francis.inist.fr/vibad/index.php?action=search&terms=14934356
Rights:
Copyright 2003 INIST-CNRS
CC BY 4.0
Sauf mention contraire ci-dessus, le contenu de cette notice bibliographique peut être utilisé dans le cadre d’une licence CC BY 4.0 Inist-CNRS / Unless otherwise stated above, the content of this bibliographic record may be used under a CC BY 4.0 licence by Inist-CNRS / A menos que se haya señalado antes, el contenido de este registro bibliográfico puede ser utilizado al amparo de una licencia CC BY 4.0 Inist-CNRS
Notes:
Computer science; theoretical automation; systems
Accession Number:
edscal.14934356
Database:
PASCAL Archive

Further Information

We describe refinement in Circus, a concurrent specification language that integrates imperative CSP, Z, and the refinement calculus. Each Circus process has a state and accompanying actions that define both the internal state transitions and the changes in control flow that occur during execution. We define the meaning of refinement of processes and their actions, and propose a sound data refinement technique for process refinement. Refinement laws for CSP and Z are directly relevant and applicable to Circus, but our focus here is on new laws for processes that integrate state and control. We give some new results about the distribution of data refinement through the combinators of CSP. We illustrate our ideas with the development of a distributed system of cooperating processes from a centralised specification.