Communicating Sequential Processes（CSP）とは、並行性に関するプロセス計算の理論のひとつである。プログラミング言語Occamにも影響を与えた。CSPは1978年、アントニー・ホーアが最初に考案し、その後かなり改良されていった。CSPは様々なシステムにおける並行性を記述し検証する、形式仕様記述ツールとして産業で利用されてきた。たとえば、T9000トランスピュータやセキュアな電子商取引システムなどの例がある。理論としても、応用範囲を広げる（より大規模なシステムの解析に使えるようにする）などの研究が行われている。ホーアの1978年の論文で提示されたCSPは、プロセス計算というよりも本質的には並行プログラミング言語であった。後のCSPとは構文が著しく異なり、数学的に定義された意味論を持っておらず、無制限の非決定性を表現することはできなかった。本来のCSPでは、並列に動作する有限個の逐次プロセスが同期式のメッセージパッシングで相互に通信するという形式でプログラムを記述していた。その後のCSPとは対照的に、各プロセスには名前が付けられ、メッセージには送信元と送信先の名前が指定されている。たとえば次のプロセスは、codice_1 という名前のプロセスから文字を繰り返し受信し、その文字を codice_2 という名前のプロセスに送信する。並列合成では、codice_1 という名前を codice_4 プロセスに割り当て、codice_5 という名前を codice_6 プロセスに割り当て、codice_2 という名前を codice_8 プロセスに割り当て、これらを並行に実行する。その後、ホーアは Stephen Brookes や Bill Roscoe らと共に理論面の改良に取り組み、CSPをプロセス代数的にしていった。この方向性は、同時期にロビン・ミルナーが行っていた Calculus of Communicating Systems（CCS）の研究と相互に影響しあっている。CSPの理論面は1984年に発表され、1985年に出版されたホーアの著書 "Communicating Sequential Processes" で一般に知られるようになった。2006年9月現在でも、Citeseer によればこの本は計算機科学分野での引用回数第3位とされている（ただし、サンプリング方式であるため信頼性は高くない）。このホーアの著書以降、CSPの理論は若干変更されただけである。変更のほとんどは、CSPプロセス解析と検証のための自動化ツールの出現に対応するものである。Roscoe の "The Theory and Practice of Concurrency" ではこの新たなCSPが解説されている。名前が示すとおり、CSPは独立したプロセス群がメッセージパッシングによって通信することで相互にやり取りしているものとしてシステムを記述する。しかし、CSPの名称に含まれる "Sequential"（逐次的）という部分は誤解を生じる可能性がある。というのも最近のCSPでは、プロセスは単なる逐次的プロセスだけでなく、より基本的なプロセス群の並列合成で生成されるプロセスも含まれるからである。プロセス間の関係やプロセスが周囲と通信する方法は、各種プロセス代数演算子を使って表される。このような代数的手法を使うことで、少数のプリミティブ要素から容易に極めて複雑なプロセスを構築できる。CSP は、そのプロセス代数における2種類のプリミティブのクラスを提供する。CSP には様々な代数演算子がある。主なものを以下に挙げる。簡単なCSPの例として、チョコレートの自動販売機の抽象表現とチョコレートを購入しようとしている人との相互作用を考える。この自動販売機は2つのイベント "coin" と "choc" を扱う。"coin" は代金の投入を表し、"choc" はチョコレートの引渡しを表す。チョコレートを渡す前に代金の支払いを要求する機械は次のように記述される。支払いに硬貨またはカードを使う人は、以下のようにモデル化される。これら2つのプロセスを並列に置くことで、互いにやり取りできるようにする。合成プロセスの振る舞いは、2つのプロセスが同期しなければならないイベント依存する。すなわち、ここで、同期が "coin" についてのみ必要とされる場合、以下が得られる。この合成プロセスを "coin" と "card" というイベントを隠蔽することで抽象化すると、次のようになる。以上から、次の非決定性プロセスが得られる。これは、"choc" イベント後に停止するか、単に停止するプロセスである。言い換えれば、システムを外部から見たものとして上記抽象化を扱えば（すなわち、人間が行った決定を無視すれば）、非決定性が生じる。CSPの構文は、プロセスとイベントの結合の「正当な」方法を定義する。formula_50 をイベント、formula_51 をイベントの集合とする。するとCSPの基本構文は以下のように定義される。簡略化するため、上記構文定義では formula_53 プロセス（発散を表す）やアルファベット順の並列演算子やパイピング演算子や索引付き選択演算子などを省略している。文法的に正しいCSPの表現の意味を定義する形式意味論はいくつかある。CSPの理論には、相互に一貫した表示的意味論、代数的意味論、操作的意味論がある。CSPの主な表示的モデルとして、トレースモデル、安定失敗モデル、失敗/発散モデルの3つがある。プロセス表現とこれらモデルとの意味論的マッピングがCSPの表示的意味論となる。トレースモデルは、そのプロセスが扱う一連のイベント（トレース）でプロセス表現の意味を定義する。例えば、より形式的に表せば、プロセス formula_61 のトレースモデルでの意味は formula_62 として定義される。すなわち、ここで、formula_67 は考えられる全てのイベントの有限な並びの集合である。安定失敗モデルはトレースモデルを拒絶集合（refusal set）で拡張したものである。拒絶集合とは、プロセスが実行を拒絶できるイベントの集合 formula_68 である。失敗（failure）は formula_69 という対で表される。ここで formula_70 はトレース、formula_71 は拒絶集合であり、トレース formula_70 が実行されたときそのプロセスが拒絶するイベント群を表す。安定失敗モデルにおけるプロセスの観測された振る舞いは、formula_73 という対で表される。例えば、失敗/発散モデルは、失敗モデルを発散（divergence）を扱えるよう拡張したものである。失敗/発散モデルにおけるプロセスは formula_76 という対で表され、formula_77 は発散を生じさせる全トレースの集合である。また、formula_78 が成り立つ。初期の重要なCSPの応用例として、INMOS T9000 トランスピュータ の仕様記述と検証に使われた例がある。T9000 は複雑なスーパースケーラ型パイプラインプロセッサであり、大規模マルチプロセッシング可能なように設計されている。CSP はパイプラインの正当性検証と、Virtual Channel Processor というチップ間通信管理機能の検証に使われた。ソフトウェア設計におけるCSPの応用は、主に人命に関わるような重要なシステムでなされている。例えば、Bremen Institute for Safe Systems と Daimler-Benz Aerospace は、国際宇宙ステーションで使用予定のシステム（約23,000行のコード）をCSPでモデル化し、デッドロックやライブロックが起きないことを検証した。このモデル化と解析によって、通常のソフトウェアテストでは検出が困難な問題をいくつか発見した。同様に Praxis High Integrity Systems でもセキュアなスマートカード認証システム（約100,000行のコード）の開発でCSPを使い、セキュリティとデッドロックが発生しないことの検証を行った。Praxis はシステムの欠陥率が他の同等のシステムよりも低くなったと主張している。CSP はメッセージ交換を行う複雑なシステムのモデル化と解析に適しているため、通信プロトコルやセキュリティプロトコルの検証にも応用されてきた。特筆すべき応用例として、Needham-Schroeder 公開鍵認証プロトコルをCSPを使って検証し、未知の脆弱性を発見し、それに対処した新たなプロトコルを開発した例がある。長年に渡って、CSPを使ってシステムを表現することで解析するツールがいくつも生み出されてきた。初期のツールはコンピュータが理解できるCSPの表現もまちまちだったため、ツール間で情報を共有できなかった。しかし最近では Bryan Scattergood の記法 CSP が多くのCSPツールで使われている。CSP には操作的意味論の形式定義があり、組み込みの関数型言語が含まれる。もっとも有名なCSPツールとして Formal Systems Europe Ltd. が開発した商用製品である "Failures/Divergence Refinement 2" ("FDR2") がある。FDR2 はモデルチェッカとされることが多いが、技術的には改良チェッカである。すなわち、2つのCSPプロセス表現をラベル付き遷移系に変換し、指定された意味論モデル（トレース、失敗、失敗/発散）において、一方がもう一方の改良となっているかを調べる。他にも以下のようなCSPツールがある。CSP の影響を受けているその他の形式手法や仕様記述言語として、以下のものがある。

出典:wikipedia