Editing Communicating sequential processes (section)

== History ==
=== Original version ===
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,<ref name="hoare">{{cite book |last=Hoare |first=C. A. R. |author-link=C. A. R. Hoare |title=Communicating Sequential Processes |publisher=Prentice Hall |isbn=978-0-13-153289-2 |date=1985}}</ref> and was unable to represent [[unbounded nondeterminism]].<ref name="clinger1981">{{Cite thesis |first=William |last=Clinger |author-link=William Clinger (computer scientist) |title=Foundations of Actor Semantics |publisher=MIT |type=Mathematics Doctoral Dissertation |date=June 1981 |hdl=1721.1/6935}}</ref> 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. In contrast to later versions of CSP, each process was assigned an explicit name, and the source or destination of a message was defined by specifying the name of the intended sending or receiving process. For example, the process

 COPY = *[c:character; west?c → east!c]

repeatedly receives a character from the process named <code>west</code> and sends that character to process named <code>east</code>. The parallel composition

 [west::DISASSEMBLE || X::COPY || east::ASSEMBLE]

assigns the names <code>west</code> to the <code>DISASSEMBLE</code> process, <code>X</code> to the <code>COPY</code> process, and <code>east</code> to the <code>ASSEMBLE</code> process, and executes these three processes concurrently.<ref name="hoare1978" />

=== Development into process algebra ===

Following the publication of the original version of CSP, Hoare, Stephen Brookes, and [[Bill Roscoe|A. W. Roscoe]] developed and refined the ''theory'' of CSP into its modern, process algebraic form. 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. The theoretical version of CSP was initially presented in a 1984 article by Brookes, Hoare, and Roscoe,<ref>{{cite journal |first1=Stephen |last1=Brookes |author2-link=C. A. R. Hoare |first2=C. A. R. |last2=Hoare |author3-link=Bill Roscoe |author3-first=A. W. |author3-last=Roscoe |title=A Theory of Communicating Sequential Processes |journal=[[Journal of the ACM]] |volume=31 |issue=3 |pages=560–599 |date=1984 |doi=10.1145/828.833 |s2cid=488666 |doi-access=free}}</ref> and later in Hoare's book ''Communicating Sequential Processes'',<ref name="hoare" /> which was published in 1985. In September 2006, that book was still the [http://citeseer.ist.psu.edu/articles.html third-most cited] [[computer science]] reference of all time according to [[Citeseer]]{{Citation needed|date=November 2018}} (albeit an unreliable source due to the nature of its sampling). The theory of CSP has undergone a few minor changes since the publication of Hoare's book. Most of these changes were motivated by the advent of automated tools for CSP process analysis and verification. Roscoe's ''The Theory and Practice of Concurrency''<ref name="roscoe" /> describes this newer version of CSP.

=== Applications ===
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.<ref name="barrett" />

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 [[DaimlerChrysler Aerospace|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 (computer science)|deadlock]] and [[livelock]].<ref>{{cite conference |first=B. |last=Buth |author2=M. Kouvaras |author3=J. Peleska |author4=H. Shi |title=Deadlock analysis for a fault-tolerant system |book-title=Proceedings of the 6th International Conference on Algebraic Methodology and Software Technology (AMAST’97) |pages=60–75 |date=December 1997}}</ref><ref>{{cite conference |first=B. |last=Buth |author2=J. Peleska |author3=H. Shi |title=Combining methods for the livelock analysis of a fault-tolerant system |book-title=Proceedings of the 7th International Conference on Algebraic Methodology and Software Technology (AMAST’98) |pages=124–139 |date=January 1999}}</ref> 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.<ref name="hall" />

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 [[FDR2|FDR refinement-checker]] to discover a previously unknown attack on the [[Needham–Schroeder protocol|Needham–Schroeder public-key authentication protocol]], and then to develop a corrected protocol able to defeat the attack.<ref>{{cite conference |first=G. |last=Lowe |title=Breaking and fixing the Needham–Schroeder public-key protocol using FDR |book-title=Tools and Algorithms for the Construction and Analysis of Systems (TACAS) |pages=147–166 |publisher=Springer-Verlag |date=1996 |url= http://citeseer.ist.psu.edu/lowe96breaking.html}}</ref>