%0 Book Section %1 Sampaio2002 %A Sampaio, Augusto %A Woodcock, Jim %A Cavalcanti, Ana %B FME 2002:Formal Methods—Getting IT Right %D 2002 %E Eriksson, Lars-Henrik %E Lindsay, Peter %I Springer Berlin / Heidelberg %K %P 1-15 %T Refinement in Circus %U http://dx.doi.org/10.1007/3-540-45614-7_26 %V 2391 %X 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.

@incollection{Sampaio2002, abstract = {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.}, added-at = {2010-12-02T00:41:33.000+0100}, affiliation = {Centro de Informática UFPE Recife PE Brazil}, author = {Sampaio, Augusto and Woodcock, Jim and Cavalcanti, Ana}, biburl = {https://www.bibsonomy.org/bibtex/24c6c40156f8390f4a6ec8a0a608489bc/tasawer}, booktitle = {FME 2002:Formal Methods—Getting IT Right}, editor = {Eriksson, Lars-Henrik and Lindsay, Peter}, interhash = {6df3e1fa2296eb7d4fede0de0955bfb0}, intrahash = {4c6c40156f8390f4a6ec8a0a608489bc}, keywords = {}, note = {10.1007/3-540-45614-7_26}, pages = {1-15}, publisher = {Springer Berlin / Heidelberg}, series = {Lecture Notes in Computer Science}, timestamp = {2010-12-02T00:41:34.000+0100}, title = {Refinement in Circus}, url = {http://dx.doi.org/10.1007/3-540-45614-7_26}, volume = 2391, year = 2002 }