Communicating Sequential Processes

Communicating Sequential Processes (CSP)詳解

Communicating Sequential Processes（CSP）は、並行計算におけるプロセス代数の代表的な理論であり、並行システムの設計・検証に用いられる形式手法です。1978年にアントニー・ホーアによって考案され、その後、Stephen BrookesやBill Roscoeらによる改良を経て、理論的基盤が確立されました。Occamなどのプログラミング言語にも影響を与え、産業においても、T9000トランスピュータやセキュアな電子商取引システムなど、様々なシステムの仕様記述や検証に活用されてきました。

歴史

ホーアの初期のCSPは、並行プログラミング言語としての側面が強く、現在のCSPとは構文や意味論が大きく異なっていました。初期のCSPでは、有限個の逐次プロセスが、名前付きのメッセージパッシングを通じて通信するプログラム記述方法が中心でした。例えば、`COPY = *[c:character; west?c → east!c]` は、westプロセスから文字を受信し、eastプロセスへ送信するプロセスを表しています。

その後、ホーアらはBrookes、Roscoeらと共にCSPの理論的改良に取り組み、プロセス代数的な枠組みを構築しました。これは、Robin MilnerによるCalculus of Communicating Systems（CCS）の研究とも相互に影響を与え合いました。1984年に理論的基盤が発表され、1985年のホーアの著書『Communicating Sequential Processes』によって広く知られるようになりました。この著書は、長年にわたり計算機科学分野で高く評価されています。

概要

CSPは、独立したプロセス群がメッセージパッシングによって通信することで相互作用するシステムを記述します。「Sequential」という名称は、プロセスが必ずしも逐次的な処理のみを行うとは限らないことを示唆しており、基本的なプロセス群の並列合成によって複雑なプロセスを構築できます。プロセス間の関係や通信方法は、プロセス代数演算子によって表現されます。この代数的なアプローチにより、少ないプリミティブ要素から複雑なシステムを容易に構築できます。

プリミティブ

CSPは、イベントとプリミティブプロセスの2種類のプリミティブを提供します。

イベント

イベントは、通信や相互作用を表す不可分な瞬間的なものです。不可分名（`on`, `off`）、複合名（`valve.open`, `valve.close`）、入出力イベント（`mouse?xy`, `screen!bitmap`）などがあります。

プリミティブプロセス

プリミティブプロセスは、基本的な振る舞いを表します。`STOP`（通信を行わずデッドロック状態となる）、`SKIP`（成功裡に終了する）などが代表的です。

代数演算子

CSPには、様々な代数演算子があり、これらを組み合わせることで複雑なプロセスを表現できます。主な演算子を以下に示します。

プレフィックス (`→`)

イベントとプロセスを結合します。`a → P` は、イベント`a` と通信した後、プロセス`P` として動作します。

決定的選択 (`◻`)

複数のプロセスから環境が選択します。`(a → P) ◻ (b → Q)` は、`a` か `b` のいずれかのイベントと通信し、それぞれ`P`, `Q`として動作します。

非決定的選択 (`⊓`)

複数のプロセスからプロセス自身が選択します。`(a → P) ⊓ (b → Q)` は、`a` か `b` のいずれかのイベントと通信し、`P` か `Q` のいずれかとして動作します。

インターリーブ (`|||`)

プロセスを完全に独立して並列実行します。`P ||| Q` は、`P` と `Q` が同時に動作し、イベントはインターリーブされます。

インタフェース並列 (`|[X]|`)

プロセスを並列実行しますが、イベント集合`X`に含まれるイベントは、全てのプロセスがそのイベントを扱える状態のときにのみ発生します。

隠蔽 (`∖`)

イベントを非可観測とします。`(a → P) ∖ {a}` は、イベント`a` を隠蔽し、`P` と等価になります。

例：チョコレート自動販売機

コイン投入(`coin`)とチョコレート排出(`choc`)イベントを持つ自動販売機と、コインまたはカードで支払う利用者をモデル化し、それらを並列合成することでシステム全体の振る舞いを記述できます。

形式的定義

構文

CSPの構文は、プロセスとイベントの結合方法を定義します。様々な演算子を組み合わせることで、複雑なプロセスを表現できます。

形式意味論

CSPの形式意味論には、トレースモデル、安定失敗モデル、失敗/発散モデルなどがあります。これらのモデルを用いて、CSP表現の意味を厳密に定義します。トレースモデルは、プロセスが実行するイベント列を表現し、安定失敗モデルと失敗/発散モデルは、拒絶集合や発散の概念を含めてより詳細なプロセス動作を表現します。

応用

CSPは、INMOS T9000トランスピュータの検証や、国際宇宙ステーションのシステム、セキュアなスマートカード認証システムなど、様々なクリティカルシステムの設計・検証に用いられています。また、通信プロトコルやセキュリティプロトコルの検証にも有効です。

ツール

CSPを用いたシステム解析のためのツールが多数開発されています。FDR2は、モデルチェッカとして広く利用されています。他にも、ProBE、ARC、Casperなどのツールがあります。

関連する形式手法

Timed CSP、Receptive Process Theory、Wright、TCOZ、Circus、CspCASLなどが、CSPの影響を受けて開発された形式手法です。

まとめ

CSPは、並行システムの設計と検証において強力なツールです。メッセージパッシングに基づく直感的なモデルと、厳密な数学的基盤を備えているため、信頼性の高いシステム開発に貢献します。様々なツールや関連手法も開発されており、今後もその重要性は増していくでしょう。

もう一度検索