Communicating Sequential Processes
長年に渡って、CSPを使ってシステムを表現することで解析するツールがいくつも生み出されてきた。初期のツールはコンピュータが理解できるCSPの表現もまちまちだったため、ツール間で情報を共有できなかった。しかし最近では Bryan Scattergood の記法 CSPM が多くのCSPツールで使われている。CSPM には操作的意味論の形式定義があり、組み込みの関数型言語が含まれる。
もっとも有名なCSPツールとして Formal Systems Europe Ltd. が開発した商用製品である Failures/Divergence Refinement 2 (FDR2) がある。FDR2 はモデルチェッカとされることが多いが、技術的には改良チェッカである。すなわち、2つのCSPプロセス表現をラベル付き遷移系に変換し、指定された意味論モデル(トレース、失敗、失敗/発散)において、一方がもう一方の改良となっているかを調べる。
他にも以下のようなCSPツールがある。
ProBE
ARC
Casper
( a → P ) | [ { a } ] | ( a → Q ) {\displaystyle \left(a\rightarrow P\right)\left\vert \left[\left\{a\right\}\right]\right\vert \left(a\rightarrow Q\right)}
は、イベント a {\displaystyle {\mathit {a}}} を扱うことができ、次のように表せる。
P | [ { a } ] | Q {\displaystyle P\left\vert \left[\left\{a\right\}\right]\right\vert Q}
一方
( a → P ) | [ { a , b } ] | ( b → Q ) {\displaystyle \left(a\rightarrow P\right)\left\vert \left[\left\{a,b\right\}\right]\right\vert \left(b\rightarrow Q\right)}
は、単純なデッドロックを意味する。
インターリーブ演算子は、完全に独立した並行動作を表す。次のプロセス
P | | | Q {\displaystyle P\;\vert \vert \vert \;Q}
は、 P {\displaystyle {\mathit {P}}} と Q {\displaystyle {\mathit {Q}}} が同時並行に動作することを意味する。両方のプロセスが発生するイベントは時系列上でインターリーブされる。
非決定的(または内部)選択演算子は、プロセスの将来を2つのコンポーネントプロセス間の選択で定義可能とするものだが、環境がどちらのコンポーネントプロセスを選択するかを制御できない。たとえば
( a → P ) ⊓ ( b → Q ) {\displaystyle \left(a\rightarrow P\right)\sqcap \left(b\rightarrow Q\right)}
は、 ( a → P ) {\displaystyle \left(a\rightarrow P\right)} または ( b → Q ) {\displaystyle \left(b\rightarrow Q\right)} のどちらかとして振舞う。 a {\displaystyle {\mathit {a}}} または b {\displaystyle {\mathit {b}}} を受容することを拒否でき、環境が a {\displaystyle {\mathit {a}}} と b {\displaystyle {\mathit {b}}} の両方を提供する場合にそれとやり取りするだけである。