CSP-OZ: A Combination of Object-Z and CSP

Abstract

In this paper we define a combination of Object-Z and CSP called CSP-OZ. The basic idea is to define a CSP-semantics for every Object-Z class. Special care is taken to capture the characteristics of input and output parameters properly and to preserve the expected refinement rules. CSP-OZ is well suited for the specification and development of communicating distributed systems. It provides powerful techniques to model data- and control-aspects in a common framework. The language is easy to use for Z and Object-Z users. A shorter version of this paper appeared as [10].