Specification and (property) inheritance in CSP-OZ. (English) Zbl 1075.68051

Olderog, Ernst-Rüdiger; Wehrheim, Heike

Sci. Comput. Program. 55, No. 1-3, 227-257 (2005).

Summary: CSP-OZ 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.

MSC:

68Q60	Specification and verification (program logics, model checking, etc.)
68Q55	Semantics in the theory of computing
68Q85	Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Keywords:

CSP; Object-Z; Failures divergence semantics; Inheritance; Safety and liveness properties; Model-checking; FDR

Software:

Bandera