In computer science, communicating sequential processes (CSP) is a formal language for describing patterns of interaction in concurrent systems.
[11] The version of CSP presented in Hoare's original 1978 article was essentially a concurrent programming language rather than a process calculus.
It had a substantially different syntax than later versions of CSP, did not possess mathematically defined semantics,[12] and was unable to represent unbounded nondeterminism.
[13] Programs in the original CSP were written as a parallel composition of a fixed number of sequential processes communicating with each other strictly through synchronous message-passing.
The approach taken in developing CSP into a process algebra was influenced by Robin Milner's work on the Calculus of Communicating Systems (CCS) and conversely.
In September 2006, that book was still the third-most cited computer science reference of all time according to Citeseer[citation needed] (albeit an unreliable source due to the nature of its sampling).
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.
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.
[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.
[17] As its name suggests, CSP allows the description of systems in terms of component processes that operate independently, and interact with each other solely through message-passing communication.
Using this algebraic approach, quite complex process descriptions can be easily constructed from a few primitive elements.
The hiding operator provides a way to abstract processes by making some events unobservable by the environment.
The existence of hiding introduces an additional behaviour called divergence, where an infinite sequence of τ-actions is performed.
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.
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.
process, which represents divergence, as well as various operators such as alphabetized parallel, piping, and indexed choices.
[19] The CSPM dialect of CSP possesses a formally defined operational semantics, which includes an embedded functional programming language.
ARC differs from FDR2 in that it internally represents CSP processes as Ordered Binary Decision Diagrams (OBDDs), which alleviates the state explosion problem of explicit LTS representations without requiring the use of state-space compression algorithms such as those used in FDR2.
The ProB project,[23] which is hosted by the Institut für Informatik, Heinrich-Heine-Universität Düsseldorf, was originally created to support analysis of specifications constructed in the B method.
However, it also includes support for analysis of CSP processes both through refinement checking, and LTL model-checking.
Mutable shared variables and asynchronous channels provide a convenient syntactic sugar for well-known process modelling patterns used in standard CSP.
[26] The principal differences between the PAT syntax and standard CSPM are the use of semicolons to terminate process expressions, the inclusion of syntactic sugar for variables and assignments, and the use of slightly different syntax for internal choice and parallel composition.
The result of checking are also reported graphically as computation-trees and can be analyzed interactively with peripheral inspecting tools.
However, the two models make some fundamentally different choices with regard to the primitives they provide: Note that the aforementioned properties do not necessarily refer to the original CSP paper by Hoare, but rather the modern incarnation of the idea as seen in implementations such as Go and Clojure's core.async.
In the original paper, channels were not a central part of the specification, and the sender and receiver processes actually identify each other by name.
In 1990, “A Queen’s Award for Technological Achievement has been conferred ... on [Oxford University] Computing Laboratory.
The founder had the vision that the CSP ideas were ripe for industrial exploitation, and he made that the basis of the language for programming Transputers, which was called Occam.
They applied for and won a Queen’s award for technological achievement, in conjunction with Oxford University Computing Laboratory.”