A note on traces refinement and the conf relation in the Unifying Theories of Programming

Abstract. There is a close relation between the failures-divergences and the UTP models of CSP, but they are not equivalent. For example, mira-cles are not available in the failures-divergences model; the UTP theory is richer and can be used to give semantics to data-rich process algebras like Circus. Previously, we have defined functions that calculate the failures-divergences model of a CSP process characterised by a UTP relation. In this note, we use these functions to calculate the UTP characterisations of traces refinement and of the conf relation that is widely used in test-ing. In addition, we prove that the combination of traces refinement and conf corresponds to refinement of processes in Circus. This result is the basis for a formal testing technique based on Circus; as usual in testing, we restrict ourselves to divergence-free processes.