CSP is one of a family of process algebras, other similar languages include CCS [160] and the ISO standard LOTOS [24]. Introductions to CSP include the texts by Hoare [121], Roscoe [172] and Schneider [173].
There are a number of possible approaches to combining state-based languages with process algebras. The composition of Object-Z classes with CSP operators was first detailed by Smith in [180], see also the work of Smith and Derrick [183,182] which consider, in addition, refinement and verification in this notation. In [87] Fischer and Smith consider the infinite trace model as an alternative semantics for combinations of CSP and Object-Z.
Alternative approaches to combining Z or Object-Z with CSP or CCS include the work of Fischer [84], Mahony and Dong [155,154], Galloway and Stoddart [93] and Taguchi and Araki [199]. A survey of some of these approaches is given in [85].
The work of Fischer, for example, also combines Object-Z with CSP by using a failure-divergence semantics as the basis for the integration. However, Object-Z classes are extended with channel definitions and a CSP process. In addition, both the precondition and guard of an operation are defined and events can either be atomic or have duration (and therefore have a start and end). The resultant language, called CSP-OZ, is complex but very expressive and benefits from a theory of refinement and tool support (see, for example, [88]).
Mahony and Dong [155] use a combination of Object-Z and timed CSP in their TCOZ language. However, instead of identifying operations and events, operation parameters are mapped to events. Similar approaches, where the granularity of operations and events is different, but using Z and CCS include the work of Galloway [93] and Taguchi and Araki [199].
There has also been similar work on combining CSP with the B notation. Butler [44] uses CSP to control the temporal ordering of B operations in a manner similar to the approach discussed in this chapter. However, to define the meaning of the specification he defines a translation of CSP into B, and therefore uses a restricted subset of CSP.
Treharne and Schneider [201] also consider a combination of CSP and B. However, in addition to controlling the temporal ordering of events, the CSP acts as a control executive for the B machine. That is, in addition to inputs communicated from the environment, internal inputs and outputs are also passed between the CSP process and the B machine parts of the combined specification.