Refinement in integrated specifications of CSP-OZ

Formal specification provides the means to verify a system´s correctness and this can be done by the development technique of refinement of formal specification. Considering the multiple views of a system, in integrated formal specifications, will introduce more than one refinement that can be applied to the specification. This paper investigates the interaction of the different parts of an integrated specification under refinement. The integrated notation of CSP-OZ integrates the behaviour based language CSP with the state based notation, Object-Z. In such integrated notation, not only different views of a system are available, but the refinement relations in both parts are also of different basis.