Communicating sequential processes

An early and important application of CSP was its use for specification and verification of elements of the INMOS T9000 Transputer, a complex superscalar pipelined processor designed to support large-scale multiprocessing. CSP was employed in verifying the correctness of both the processor pipeline and the Virtual Channel Processor, which managed off-chip communications for the processor.[9]

Industrial application of CSP to software design has usually focused on dependable and safety-critical systems. For example, the Bremen Institute for Safe Systems and Daimler-Benz Aerospace modeled a fault-management system and avionics interface (consisting of about 23,000 lines of code) intended for use on the International Space Station in CSP, and analyzed the model to confirm that their design was free of deadlock and livelock.[15][16] The modeling and analysis process was able to uncover a number of errors that would have been difficult to detect using testing alone. Similarly, Praxis High Integrity Systems applied CSP modeling and analysis during the development of software (approximately 100,000 lines of code) for a secure smart-card certification authority to verify that their design was secure and free of deadlock. Praxis claims that the system has a much lower defect rate than comparable systems.[10]

Since CSP is well-suited to modeling and analyzing systems that incorporate complex message exchanges, it has also been applied to the verification of communications and security protocols. A prominent example of this sort of application is Lowe's use of CSP and the FDR refinement-checker to discover a previously unknown attack on the Needham–Schroeder public-key authentication protocol, and then to develop a corrected protocol able to defeat the attack.[17]

CSP provides two classes of primitives in its process algebra:

Events

Events represent communications or interactions. They are assumed to be indivisible and instantaneous. They may be atomic names (e.g. on, off), compound names (e.g. valve.open, valve.close), or input/output events (e.g. mouse?xy, screen!bitmap).

Primitive processes

Primitive processes represent fundamental behaviors: examples include STOP (the process that communicates nothing, also called deadlock), and SKIP (which represents successful termination).

CSP has a wide range of algebraic operators. The principal ones are:

Prefix

The prefix operator combines an event and a process to produce a new process. For example,

$${\displaystyle a\to P}$$

is the process that is willing to communicate a with its environment and, after a, behaves like the process P.

Deterministic choice

The deterministic (or external) choice operator allows the future evolution of a process to be defined as a choice between two component processes and allows the environment to resolve the choice by communicating an initial event for one of the processes. For example,

$${\displaystyle (a\to P)\Box (b\to Q)}$$

is the process that is willing to communicate the initial events a and b and subsequently behaves as either P or Q, depending on which initial event the environment chooses to communicate. If both a and b were communicated simultaneously, the choice would be resolved nondeterministically.

Nondeterministic choice

The nondeterministic (or internal) choice operator allows the future evolution of a process to be defined as a choice between two component processes, but does not allow the environment any control over which one of the component processes will be selected. For example,

$${\displaystyle (a\to P)\sqcap (b\to Q)}$$

can behave like either ${\displaystyle (a\to P)}$ or ${\displaystyle (b\to Q)}$. It can refuse to accept a or b and is only obliged to communicate if the environment offers both a and b. Nondeterminism can be inadvertently introduced into a nominally deterministic choice if the initial events of both sides of the choice are identical. So, for example,

$${\displaystyle (a\to a\to {\text{STOP}})\Box (a\to b\to {\text{STOP}})}$$

is equivalent to

$${\displaystyle a\to {\big (}(a\to {\text{STOP}})\sqcap (b\to {\text{STOP}}){\big )}}$$

Interleaving

The interleaving operator represents completely independent concurrent activity. The process

$${\displaystyle P\;|||\;Q}$$

behaves as both P and Q simultaneously. The events from both processes are arbitrarily interleaved in time.

Interface parallel

The interface parallel operator represents concurrent activity that requires synchronization between the component processes: any event in the interface set can only occur when all component processes are able to engage in that event. For example, the process

$${\displaystyle P\;|[\{a\}]|\;Q}$$

requires that P and Q must both be able to perform event a before that event can occur. So, for example, the process

$${\displaystyle (a\to P)\;|[\{a\}]|\;(a\to Q)}$$

can engage in event a and become the process

$${\displaystyle P\;|[\{a\}]|\;Q}$$

while

$${\displaystyle (a\to P)\;|[\{a,b\}]|\;(b\to Q)}$$

will simply deadlock.

Hiding

The hiding operator provides a way to abstract processes by making some events unobservable. A trivial example of hiding is

$${\displaystyle (a\to P)\setminus \{a\}}$$

which, assuming that the event a doesn't appear in P, simply reduces to

$${\displaystyle P}$$

One of the archetypal CSP examples is an abstract representation of a chocolate vending machine and its interactions with a person wishing to buy some chocolate. This vending machine might be able to carry out two different events, “coin” and “choc” which represent the insertion of payment and the delivery of a chocolate respectively. A machine which demands payment (only in cash) before offering a chocolate can be written as:

$${\displaystyle \mathrm {VendingMachine} =\mathrm {coin} \rightarrow \mathrm {choc} \rightarrow \mathrm {STOP} }$$

A person who might choose to use a coin or card to make payments could be modelled as:

$${\displaystyle \mathrm {Person} =(\mathrm {coin} \rightarrow \mathrm {STOP} )\Box (\mathrm {card} \rightarrow \mathrm {STOP} )}$$

These two processes can be put in parallel, so that they can interact with each other. The behaviour of the composite process depends on the events that the two component processes must synchronise on. Thus,

$${\displaystyle \mathrm {VendingMachine} \left\vert \left[\left\{\mathrm {coin} ,\mathrm {card} \right\}\right]\right\vert \mathrm {Person} \equiv \mathrm {coin} \rightarrow \mathrm {choc} \rightarrow \mathrm {STOP} }$$

whereas if synchronization was only required on “coin”, we would obtain

$${\displaystyle \mathrm {VendingMachine} \left\vert \left[\left\{\mathrm {coin} \right\}\right]\right\vert \mathrm {Person} \equiv \left(\mathrm {coin} \rightarrow \mathrm {choc} \rightarrow \mathrm {STOP} \right)\Box \left(\mathrm {card} \rightarrow \mathrm {STOP} \right)}$$

If we abstract this latter composite process by hiding the “coin” and “card” events, i.e.

$${\displaystyle \left(\left(\mathrm {coin} \rightarrow \mathrm {choc} \rightarrow \mathrm {STOP} \right)\Box \left(\mathrm {card} \rightarrow \mathrm {STOP} \right)\right)\setminus \left\{\mathrm {coin,card} \right\}}$$

we get the nondeterministic process

$${\displaystyle \left(\mathrm {choc} \rightarrow \mathrm {STOP} \right)\sqcap \mathrm {STOP} }$$

This is a process which either offers a “choc” event and then stops, or just stops. In other words, if we treat the abstraction as an external view of the system (e.g., someone who does not see the decision reached by the person), nondeterminism has been introduced.

The syntax of CSP defines the “legal” ways in which processes and events may be combined. Let e be an event, and X be a set of events. Then the basic syntax of CSP can be defined as:

$${\displaystyle {\begin{array}{lcll}{Proc}&::=&\mathrm {STOP} &\;\\&|&\mathrm {SKIP} &\;\\&|&e\rightarrow {Proc}&({\text{prefixing}})\\&|&{Proc}\;\Box \;{Proc}&({\text{external}}\;{\text{choice}})\\&|&{Proc}\;\sqcap \;{Proc}&({\text{nondeterministic}}\;{\text{choice}})\\&|&{Proc}\;\vert \vert \vert \;{Proc}&({\text{interleaving}})\\&|&{Proc}\;|[\{X\}]|\;{Proc}&({\text{interface}}\;{\text{parallel}})\\&|&{Proc}\setminus X&({\text{hiding}})\\&|&{Proc};{Proc}&({\text{sequential}}\;{\text{composition}})\\&|&\mathrm {if} \;b\;\mathrm {then} \;{Proc}\;\mathrm {else} \;Proc&({\text{boolean}}\;{\text{conditional}})\\&|&{Proc}\;\triangleright \;{Proc}&({\text{timeout}})\\&|&{Proc}\;\triangle \;{Proc}&({\text{interrupt}})\end{array}}}$$

Note that, in the interests of brevity, the syntax presented above omits the ${\displaystyle \mathbf {div} }$ process, which represents divergence, as well as various operators such as alphabetized parallel, piping, and indexed choices.

CSP has been imbued with several different formal semantics, which define the meaning of syntactically correct CSP expressions. The theory of CSP includes mutually consistent denotational semantics, algebraic semantics, and operational semantics.

The three major denotational models of CSP are the traces model, the stable failures model, and the failures/divergences model. Semantic mappings from process expressions to each of these three models provide the denotational semantics for CSP.[1]

The traces model defines the meaning of a process expression as the set of sequences of events (traces) that the process can be observed to perform. For example,

• ${\displaystyle \mathrm {traces} \left(\mathrm {STOP} \right)=\left\{\langle \rangle \right\}}$ since ${\displaystyle \mathrm {STOP} }$ performs no events
• ${\displaystyle \mathrm {traces} \left(a\rightarrow b\rightarrow \mathrm {STOP} \right)=\left\{\langle \rangle ,\langle a\rangle ,\langle a,b\rangle \right\}}$ since the process ${\displaystyle (a\rightarrow b\rightarrow \mathrm {STOP} )}$ can be observed to have performed no events, the event a, or the sequence of events a followed by b

More formally, the meaning of a process P in the traces model is defined as ${\displaystyle \mathrm {traces} \left(P\right)\subseteq \Sigma ^{\ast }}$ such that:

1. ${\displaystyle \langle \rangle \in \mathrm {traces} \left(P\right)}$ (i.e. ${\displaystyle \mathrm {traces} \left(P\right)}$ contains the empty sequence)
2. ${\displaystyle s_{1}\smallfrown s_{2}\in \mathrm {traces} \left(P\right)\implies s_{1}\in \mathrm {traces} \left(P\right)}$ (i.e. ${\displaystyle \mathrm {traces} \left(P\right)}$ is prefix-closed)

where ${\displaystyle \Sigma ^{\ast }}$ is the set of all possible finite sequences of events.

The stable failures model extends the traces model with refusal sets, which are sets of events ${\displaystyle X\subseteq \Sigma }$ that a process can refuse to perform. A failure is a pair ${\displaystyle \left(s,X\right)}$, consisting of a trace s, and a refusal set X which identifies the events that a process may refuse once it has executed the trace s. The observed behavior of a process in the stable failures model is described by the pair ${\displaystyle \left(\mathrm {traces} \left(P\right),\mathrm {failures} \left(P\right)\right)}$. For example,

$${\displaystyle \mathrm {failures} \left(\left(a\rightarrow \mathrm {STOP} \right)\Box \left(b\rightarrow \mathrm {STOP} \right)\right)=\left\{\left(\langle \rangle ,\emptyset \right),\left(\langle a\rangle ,\left\{a,b\right\}\right),\left(\langle b\rangle ,\left\{a,b\right\}\right)\right\}}$$

$${\displaystyle \mathrm {failures} \left(\left(a\rightarrow \mathrm {STOP} \right)\sqcap \left(b\rightarrow \mathrm {STOP} \right)\right)=\left\{\left(\langle \rangle ,\left\{a\right\}\right),\left(\langle \rangle ,\left\{b\right\}\right),\left(\langle a\rangle ,\left\{a,b\right\}\right),\left(\langle b\rangle ,\left\{a,b\right\}\right)\right\}}$$

The failures/divergence model further extends the failures model to handle divergence. The semantics of a process in the failures/divergences model is a pair ${\displaystyle \left(\mathrm {failures} _{\perp }\left(P\right),\mathrm {divergences} \left(P\right)\right)}$ where ${\displaystyle \mathrm {divergences} \left(P\right)}$ is defined as the set of all traces that can lead to divergent behavior and ${\displaystyle \mathrm {failures} _{\perp }\left(P\right)=\mathrm {failures} \left(P\right)\cup \left\{\left(s,X\right)\mid s\in \mathrm {divergences} \left(P\right)\right\}}$.