連続したプロセスを伝達する

Hoareが1978年に発表した最初の論文で提示されたCSPのバージョンは、本質的にはプロセス計算ではなく並行プログラミング言語でした。後のバージョンのCSPとは構文が大きく異なり、数学的に定義された意味論を持たず^{[ 12 ]} 、無制限の非決定性を表現することもできませんでした^{[ 13 ]}。オリジナルのCSPのプログラムは、同期メッセージパッシングのみで相互に通信する固定数の逐次プロセスの並列合成として記述されていました。後のバージョンのCSPとは対照的に、各プロセスには明示的な名前が割り当てられ、メッセージの送信元または宛先は、意図する送信または受信プロセスの名前を指定することによって定義されました。たとえば、プロセス

コピー = *[c:文字; west?c → east!c]

という名前のプロセスから文字を繰り返し受信しwest、その文字をという名前のプロセスに送信するeast。並列合成

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

westプロセスDISASSEMBLE、XプロセスCOPY、eastプロセスにそれぞれ名前を割り当てASSEMBLE、これら 3 つのプロセスを同時に実行します。^{[ 7 ]}

CSP のオリジナル版の発表後、Hoare、Stephen Brookes、AW Roscoe はCSP の理論を現代のプロセス代数形式に発展させ、改良しました。CSP をプロセス代数に発展させるアプローチは、 Robin Milnerの通信システム計算(CCS) の研究に影響を受け、またその逆も然りです。CSP の理論版は、1984 年に Brookes、Hoare、Roscoe による論文^{[ 14 ]}で最初に発表され、その後、1985 年に出版されたHoare の著書Communicating Sequential Processes [ ^{12 ]で紹介されました。2006}年 9 月の時点で、この本はCiteseerによると、史上3 番目に多く引用されたコンピュータ サイエンスの参考文献でした(ただし、サンプリングの性質上、信頼性の低い情報源です)。CSP の理論は、Hoare の著書の出版以来、いくつかの小さな変更を受けています。これらの変更のほとんどは、CSP プロセスの分析と検証のための自動化ツールの出現によって動機づけられたものです。Roscoe のThe Theory and Practice of Concurrency ^{[ 1 ]}では、この新しいバージョンの CSP について説明しています。

CSPの初期の重要な応用例の一つは、大規模マルチプロセッシングをサポートするように設計された複雑なスーパースカラパイプラインプロセッサであるINMOS T9000トランスピュータの要素の仕様と検証に使用されたことである。CSPは、プロセッサパイプラインと、プロセッサのオフチップ通信を管理する仮想チャネルプロセッサの両方の正しさを検証するために使用された。^{[ 9 ]}

CSP のソフトウェア設計への産業応用は、通常、信頼性と安全性が重要なシステムに焦点を当ててきました。たとえば、ブレーメン安全システム研究所とダイムラー・ベンツ・エアロスペースは、国際宇宙ステーションで使用することを目的とした障害管理システムとアビオニクスインターフェース (約 23,000 行のコードで構成) をCSP でモデル化し、モデルを分析して、設計にデッドロックやライブロックがないことを確認しました。^{[ 15 ] [ 16 ]}モデリングと分析のプロセスにより、テストだけでは検出が困難だった多くのエラーが明らかになりました。同様に、Praxis High Integrity Systems は、セキュアなスマートカード認証局のソフトウェア (約 100,000 行のコード) の開発中に CSP モデリングと分析を適用し、設計が安全でデッドロックがないことを検証しました。Praxis は、このシステムは同等のシステムよりもはるかに欠陥率が低いと主張しています。^{[ 10 ]}

CSPは複雑なメッセージ交換を含むシステムのモデリングと分析に適しているため、通信およびセキュリティプロトコルの検証にも適用されています。この種の応用の顕著な例として、LoweがCSPとFDRリファインメントチェッカーを使用して、 Needham–Schroeder公開鍵認証プロトコルに対するこれまで知られていなかった攻撃を発見し、その攻撃を阻止できる修正プロトコルを開発したことが挙げられます。^{[ 17 ]}

CSPは、そのプロセス代数において、イベントとプリミティブプロセスという2種類のプリミティブを提供する。

イベント

イベントは通信または相互作用を表します。イベントは瞬時に発生するものと想定され、外部の「環境」がプロセスについて知ることができるのは、イベントの通信のみです。イベントは、環境が許可する場合にのみ通信されます。プロセスがイベントを提供し、環境がそれを許可する場合、そのイベントは通信されなければなりません。イベントは、原子名（例：on、off）、複合名（例：valve.open、valve.close）、または入出力イベント（例：mouse?xy、screen!bitmap）のいずれかです。すべてのイベントの集合は、次のように表されます。${\displaystyle \Sigma }$[ ^{18 ]​}

原始的なプロセス

原始的なプロセスは基本的な振る舞いを表します。例としては、${\displaystyle \mathrm {停止} }$（即座にデッドロックするプロセス）${\displaystyle \mathrm {スキップ} }$（すぐに正常に終了するプロセス）。^{[ 18 ]}

CSPには幅広い代数演算子があります。主なものは、以下のように非公式に示されます。

接頭辞

接頭辞演算子は、イベントとプロセスを組み合わせて新しいプロセスを生成します。たとえば、${\displaystyle a\to P}$イベントを伝達しようとするプロセス${\displaystyle a}$その環境と、その後${\displaystyle a}$プロセスのように動作する${\displaystyle P}$[ ^{18 ]​}

再帰

プロセスは再帰を使用して定義できます。${\displaystyle F(P)}$CSP 用語には、${\displaystyle P}$プロセス${\displaystyle \mu PF(P)}$方程式で与えられる再帰プロセスを定義する ${\displaystyle P=F(P)}$再帰は相互に定義することもできます。 $${\displaystyle {\begin{aligned}&P_{u}=up\to P_{d}\\&P_{d}=down\to P_{u}\\\end{aligned}}}$$ これは、通信を交互に行う相互再帰的なプロセスのペアを定義する。${\displaystyle up}$そして${\displaystyle down}$[ ^{18 ]​}

決定論的選択

決定論的（または外部）選択演算子を使用すると、プロセスの将来の進化を 2 つのコンポーネント プロセス間の選択として定義でき、環境がプロセスのいずれかに対する初期イベントを伝達することによって選択を解決できます。たとえば、${\displaystyle (a\to P)\ \Box \ (b\to Q)}$初期イベントを伝達しようとするプロセス${\displaystyle a}$そして${\displaystyle b}$そしてその後は、${\displaystyle P}$または${\displaystyle Q}$環境がどの初期イベントを伝達するかによって異なる。^{[ 18 ]}

非決定論的選択

非決定論的（または内部）選択演算子は、プロセスの将来の進化を2つの構成要素プロセス間の選択として定義することを可能にしますが、環境がどちらの構成要素プロセスが選択されるかを制御することを許可しません。たとえば、${\displaystyle (a\to P)\sqcap (b\to Q)}$どちらのようにも振る舞うことができる${\displaystyle a\to P}$または${\displaystyle b\to Q}$受け入れを拒否することができます${\displaystyle a}$または${\displaystyle b}$そして、環境が両方を提供する場合にのみコミュニケーションを行う義務がある。${\displaystyle a}$そして${\displaystyle b}$。

選択の両側の初期事象が同一である場合、一見決定論的な選択に意図せず非決定論が導入される可能性がある。例えば、 $${\displaystyle (a\to a\to \mathrm {STOP} )\ \Box \ (a\to b\to \mathrm {STOP} )}$$そして $${\displaystyle a\to {\big (}(a\to \mathrm {STOP} )\sqcap (b\to \mathrm {STOP} ){\big )}}$$ 同等である。^{[ 18 ]}

インターリーブ

インターリーブ演算子は、完全に独立した並行アクティビティを表します。${\displaystyle P\;|||\;Q}$両方の役割を果たす${\displaystyle P}$そして${\displaystyle Q}$同時に。両方のプロセスのイベントは時間的に任意にインターリーブされます。インターリーブは、たとえ${\displaystyle P}$そして${\displaystyle Q}$両方とも決定論的である:${\displaystyle P}$そして${\displaystyle Q}$両方とも同じイベントを伝えることができる、${\displaystyle P\;|||\;Q}$非決定論的に、どちらのプロセスがそのイベントを伝達したかを選択する。^{[ 18 ]}

インターフェース並列

インターフェース並列（または一般化並列）演算子は、コンポーネントプロセス間の同期を必要とする並行アクティビティを表します。${\displaystyle P\;|[X]|\;Q}$インターフェースセット内の任意のイベント${\displaystyle X\subseteq \Sigma }$両方が揃った場合にのみ発生する${\displaystyle P}$そして${\displaystyle Q}$そのイベントに参加することができる。^{[ 18 ]}

例えば、そのプロセス${\displaystyle P\;|[\{a\}]|\;Q}$要求する${\displaystyle P}$そして${\displaystyle Q}$両方ともイベントを実行できる必要がある${\displaystyle a}$そのイベントが発生する前に。つまり、そのプロセスは${\displaystyle (a\to P)\;|[\{a\}]|\;(a\to Q)}$と同等${\displaystyle a\to (P\;|[\{a\}]|\;Q)}$、 その間${\displaystyle (a\to P)\;|[\{a,b\}]|\;(b\to Q)}$と同等${\displaystyle \mathrm {停止} }$（つまり、プロセスがデッドロック状態になる）。

隠蔽

隠蔽演算子は、一部のイベントを環境から観測できないようにすることで、プロセスを抽象化する手段を提供する。${\displaystyle P\setminus X}$プロセスは${\displaystyle P}$イベントが設定されました${\displaystyle X}$隠れた。

隠蔽の簡単な例は${\displaystyle (a\to P)\setminus \{a\}}$このイベントが${\displaystyle a}$表示されません${\displaystyle P}$単純に以下になります${\displaystyle P}$隠蔽されたイベントはτアクションとして内部化され、環境からは見えず、制御もできません。隠蔽の存在は、発散と呼ばれる追加の挙動を引き起こし、τアクションの無限シーケンスが実行されます。これはプロセスによって捉えられます。${\displaystyle \mathbf {div} }$τ アクションを永遠に実行することだけを行う。^{[ 18 ]}例えば、${\displaystyle (\mu Pa\to P)\setminus \{a\}}$と同等${\displaystyle \mathbf {div} }$。

CSPの典型的な例の一つは、チョコレートの自動販売機と、チョコレートを購入したい人とのやり取りを抽象的に表現したものです。この自動販売機は、「コイン」と「チョコレート」という2つの異なるイベントを実行できる可能性があります。これらはそれぞれ、支払いの投入とチョコレートの提供を表します。チョコレートを提供する前に支払い（現金のみ）を要求する機械は、次のように記述できます。

$${\displaystyle \mathrm {自動販売機} =\mathrm {コイン} \rightarrow \mathrm {チョコ} \rightarrow \mathrm {停止} }$$

コインやカードを使って支払いを行う人については、以下のようにモデル化できる。

$${\displaystyle \mathrm {人} =(\mathrm {コイン} \rightarrow \mathrm {STOP} )\;\Box \;(\mathrm {カード} \rightarrow \mathrm {STOP} )}$$

これら2つのプロセスは並列に実行できるため、互いに相互作用することができます。複合プロセスの動作は、2つの構成要素プロセスが同期しなければならないイベントに依存します。したがって、

$${\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} }$$

一方、「コイン」のみで同期が必要な場合は、

$${\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)}$$

この後者の複合プロセスを「コイン」と「カード」のイベントを隠すことによって抽象化すると、

$${\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\}}$$

非決定論的プロセスを得る

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

これは、何らかの「衝撃」イベントが発生して停止するか、あるいは単に停止するかのどちらかのプロセスです。言い換えれば、抽象化をシステムの外部視点（例えば、その人物の決定過程を見ていない人）として扱うと、非決定論が導入されることになります。

CSPの構文は、プロセスとイベントを組み合わせる「合法的な」方法を定義します。eをイベント、bをブール値、Xをイベントの集合とします。すると、CSPの基本構文は次のように定義できます。

$${\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}}}$$

なお、簡潔にするため、上記の構文では、${\displaystyle \mathbf {div} }$分岐を表すプロセス、およびアルファベット順の並列、パイプ処理、インデックス付き選択などのさまざまな演算子。

CSPには、構文的に正しいCSP表現の意味を定義する、いくつかの異なる形式意味論が組み込まれています。CSPの理論には、相互に矛盾のない表示的意味論、代数的意味論、および操作的意味論が含まれます。

CSP の 3 つの主要な表示モデルは、トレースモデル、安定障害モデル、および障害/分岐モデルです。プロセス表現からこれら 3 つのモデルへの意味マッピングにより、CSP の表示意味論が提供されます。^{[ 1 ]}

表示的意味論では、プロセスの細分化の部分順序を複数定義することができ、それによってプロセスのいくつかの特性をエレガントに表現することができます。一般に、${\displaystyle P\sqsubseteq Q}$意味する${\displaystyle Q}$精製する${\displaystyle P}$。

最もよく知られている CSP ツールはおそらくFailures–Divergences Refinement (FDR) であり、これは元々 Formal Systems (Europe) Ltd. によって開発された商用製品です。FDR はモデル チェッカーとして説明されることが多いですが、技術的にはリファインメントチェッカーです。これは、2 つの CSP プロセス式をラベル付き遷移システム(LTS) に変換し、特定の意味モデル (トレース、障害、または障害/分岐) 内で、一方のプロセスが他方のプロセスのリファインメントであるかどうかを判定します。^{[ 20 ]} FDR は、リファインメント チェック中に探索する必要のある状態空間のサイズを削減するために、プロセス LTS にさまざまな状態空間圧縮アルゴリズムを適用します。FDR は、FDR2、FDR3、FDR4 に後継されました。^{[ 21 ]}

アデレード改良チェッカー（ARC）^{[ 22 ]}は、アデレード大学の形式モデリングおよび検証グループによって開発されたCSP改良チェッカーです。ARCは、CSPプロセスを順序付き二分決定図（OBDD）として内部的に表現するという点でFDR2とは異なります。これにより、FDR2で使用されるような状態空間圧縮アルゴリズムを使用する必要なく、明示的なLTS表現の状態爆発問題が軽減されます。

デュッセルドルフ大学ハインリッヒ・ハイネ情報科学研究所が運営する ProB プロジェクト [ 23 ] は、元々は B メソッドで構築された仕様の分析をサポートするために作成されました。しかし^{、リファインメント}チェックとLTL モデルチェックの両方による CSP プロセスの分析もサポートしています。ProBは、CSP と B 仕様を組み合わせたものの特性を検証するためにも使用できます。ProBE CSP アニメーターは FDR3 に統合されています。

プロセス分析ツールキット(PAT) ^{[ 24 ] [ 25 ]}は、シンガポール国立大学コンピューティング学部で開発された CSP 分析ツールです。PAT は、CSP および Timed CSP プロセスのリファインメントチェック、LTL モデルチェック、およびシミュレーションを実行できます。PAT プロセス言語は、可変共有変数、非同期メッセージパッシング、および などのさまざまな公平性と定量的時間関連プロセス構造のサポートにより CSP を拡張します。PAT プロセスdeadline言語waituntilの基本的な設計原則は、表現力を高めるために、高レベルの仕様言語と手続き型プログラム (たとえば、PAT のイベントは、シーケンシャル プログラムまたは外部 C# ライブラリ呼び出しである可能性があります) を組み合わせることです。可変共有変数と非同期チャネルは、標準 CSP で使用されるよく知られたプロセスモデリングパターンの便利な構文糖衣を提供します。PAT 構文は CSP _Mと似ていますが、同一ではありません。^{[ 26 ]} PAT構文と標準CSP _Mの主な違いは、プロセス式を終了させるためにセミコロンを使用すること、変数と代入のための構文糖衣を含めること、および内部選択と並列合成にわずかに異なる構文を使用することです。

VisualNets ^{[ 27 ]}は仕様から CSP システムのアニメーションによる視覚化を生成し、時間付き CSP をサポートしています。

CSPsim ^{[ 28 ]}は遅延シミュレーターです。CSP のモデルチェックは行いませんが、非常に大規模な (潜在的に無限の) システムを探索するのに役立ちます。

SyncStitch ^{[ 29 ]}は、対話型のモデリングおよび分析環境を備えた CSP 改良チェッカーです。グラフィカルな状態遷移図エディタを備えています。ユーザーは、プロセスの動作を CSP 式だけでなく状態遷移図としてもモデル化できます。チェック結果は計算ツリーとしてグラフィカルに表示され、周辺の検査ツールと対話的に分析できます。改良チェックに加えて、デッドロックチェックとライブロックチェックも実行できます。