Work on state-based refinement relations for concurrent systems goes back to the end of the '80s. He Jifeng [129] and Josephs [134] both developed refinement relations for state-based transition systems which are complete and sound with respect to CSP failures-divergences refinement. Similar results for action systems with a weakest precondition semantics were also derived by Woodcock and Morgan around the same time [211].
The use of these results in the context of Object-Z components in an integrated CSP/Object-Z specification is due to Smith and Derrick [183,182]. As stated earlier these results have been generalised in [70] to a set of structural refinement rules, where a development step can now change the granularity of components and introduce additional Object-Z classes communicating and synchronising via CSP operators.
Simulation methods have also been developed for the CSP-OZ language. In [86] Fischer derives downward and upward simulations for use on the components in a CSP-OZ specification. Instead of structural simulation rules, model checking techniques based upon the CSP model checking tool FDR [91] have been developed [88] to verify simulations where the structure of the specification changes.