Combining CSP and Object-Z: Finite or Infinite Trace Semantics?
Clemens Fischer, Graeme Smith · 1997
In this paper we compare and contrast two alternative semantics as a means of combining CSP with Object-Z. The purpose of this combination is to more effectively specify complex, concurrent systems: while CSP is ideal for modelling systems of concurrent processes, Object-Z is more suitable for modelling the data structures often needed to model the processes themselves. The first semantics, the finite trace model, is compatible with the standard CSP semantics but does not allow all forms of unbounded nondeterminism to be modelled (i. e. where a choice is made from an infinite set of options). The second semantics, the infinite trace model, overcomes this limitation but is no longer compatible with the standard CSP semantics. Issues involving specification, refinement and modelling fairness are discussed.