Communicating Sequential Processes
初期の重要な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を使って検証し、未知の脆弱性を発見し、それに対処した新たなプロトコルを開発した例がある。
決定的選択で選択肢である2つの初期イベントが同一である場合、非決定性が生じる。したがってたとえば、
( a → a → S T O P ) ◻ ( a → b → S T O P ) {\displaystyle \left(a\rightarrow a\rightarrow STOP\right)\Box \left(a\rightarrow b\rightarrow STOP\right)}
は次と等価である。
a → ( ( a → S T O P ) ⊓ ( b → S T O P ) ) {\displaystyle a\rightarrow \left(\left(a\rightarrow STOP\right)\sqcap \left(b\rightarrow STOP\right)\right)}