Linking Processes. In [RSM10], the behaviour of the basic components is defined in terms of CSP processes. The lifting of the results to CML (via Circus), requires two map- pings: the first one maps CML processes to corresponding Circus processes; the second mapping is from a subset of Circus processes to corresponding CSP processes. In the first mapping (ρ), we take a subset of CML processes without object- oriented constructs and without undefined expressions and return the se- mantically corresponding Circus process. In the second mapping, we take processes from a state-rich setting, Circus, to a stateless one, CSP. For this reason, our strategy for mapping Circus processes into CSP processes de- picted in Figure 7 is twofold: transforming stateful Circus processes into stateless Circus processes (Ω), and mapping a subset of stateless divergence- free Circus processes with a limited use of predicative specifications into corresponding CSP processes (Υ). Figure 7: Mapping CML into CSP In our mapping strategy from Circus to CSP, we first consider stateful Circus processes, that is, processes with encapsulated states and local xxxx- xxxxx. Instead of mapping such processes directly into CSP, we first transform them, using a function Ω, into stateless processes using the memory model suggested in [NSM12], in which state components and local variables are detached from the processes and moved to memory cells that store their val- ues. The soundness of this transformation is established using the Circus refinement calculus presented in [Oli06]. The function Ω takes a subset of stateful feasible Circus processes, in which:
