Specification and (property) inheritance in CSP-OZ

CSP-OZ [C. Fischer, CSP-OZ: A combination of Object-Z and CSP, in: H. Bowman, J. Derrick (Eds.), Formal Methods for Open Object-Based Distributed Systems, FMOODS’97, vol. 2, Chapman & Hall, 1997, pp. 423–438] is a combination of Communicating Sequential Processes (CSP) and Object-Z (OZ). It enables the specification of systems having both a state-based and a behaviour-oriented view using the object-oriented concepts of classes, instantiation and inheritance. CSP-OZ has a process semantics in the failure divergence model of CSP. In this paper we explain CSP-OZ and investigate the notion of inheritance. Furthermore, we study the issue of property inheritance among classes. We prove in a uniform way that behavioural subtyping relations between classes introduced in [H. Wehrheim, Behavioural subtyping in object-oriented specification formalisms, University of Oldenburg, Habilitation Thesis, 2002] guarantee the inheritance of safety and “liveness” properties.