×

zbMATH — the first resource for mathematics

Specification and (property) inheritance in CSP-OZ. (English) Zbl 1075.68051
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.)
Software:
Bandera
PDF BibTeX XML Cite
Full Text: DOI