Combining Object-Z and CSP

摘要

The process algebra CSP (Communicating Sequential Processes) [13] has been developed to describe the communication behaviour of distributed systems. The formal language Z [24] is designed for the specification of the states and the state transformations of a system in a predicative style. Object-Z [6] is an object-oriented extension of Z. In this paper we report on a combination of Object-Z and CSP that preserves the refinement methods of both languages. The basic idea is to define a CSP-style semantics for a Object-Z class. Thereby all CSP operators like hiding and parallel composition can be applied to Object-Z. The resulting language is called CSP-OZ.