CSP：Communicating Sequential Processes
＊PAT3サンプルプログラム付

松井和人（まついかずと）　
　　　NPO 法人CSP コンソーシアム　理事

 ＜略歴＞　
　米国ミネソタ大学コンピュータ科学科卒業。1987 年に英国半導体メーカInmos 社に入社し並列処理プロセッサTransputer、occam のプログラミングの指導をする。その後仏伊STMicroelectronics 社に買収されてからCSP モデルのSoC（System-on-Chip）、高速シリアルリンク（IEEE1394/1355） などの技術を推進する。
WoTUG 委員会（http://www.wotug.org/） のメンバーとして1989 年から1996 年までのTransputer/occam国際会議において東京大学國井利泰名誉教授、東北大学野口正一名誉教授の下で会議の運営に携わり、論文集を作成した。2001 年から独立し、現在NPO 法人CSP コンソーシアム理事、2011 年より法政大学大学院情報科学科の兼任講師を務める。CSP 研究会の幹事として会議の運営とCSP/occam モデルによる並行プログラミング技法の啓蒙を行っている。

まえがき

　大規模高度システムのための組み込みソフトウェア開発では、安全性と信頼性が大きな問題となっています。とりわけ、自動車、エレベータ、ロボット、鉄道、医療、宇宙機器などの産業機器、或いは民生機器では高信頼化が要求されています。組み込みシステムでの機能安全規格として、IEC61508(機能安全規格)、ISO26262(自動車) などの上位レベルでは形式手法(CCS,CSP,HOL,LOTOS,OBJ,VDM,Z, 時相論理, 他) を使う事を高く推奨(HR) されています。従って証明されたシステム設計方法は特別なものではなく、ヨーロッパでは当然のように実施されています。
　自動車、列車の制御、通信、制御、ロボットなどの様に高機能で高性能な領域に入りますと、リアルタイム処理、高度で複雑な並行処理プログラミング技法が要求されます。一般に使われていますZ/B/Event-B/Alloy/ VDM などの形式手法ツールでは要求仕様の検証が主であり、リアルタイム処理、並行処理、通信、割り込み等の振る舞いの検証は十分でないだけでなくアーキテクチャーの検証は非常に難しいです。そこで注目されるのがCSP モデルです。
　CSP（Communicating Sequential Processes ）は、元Oxford 大学のTony Hoare が1978 年 に考案し英国を中心に欧州で研究実用化が進められ、その結果としてInmos 社から並列処理言語occam と並列プロセッサTransputerが生み出されました。90 年代後半にTransputer が消えてからも、2000 年以降CSP モデルを採用したハードウェア、ソフトウェアは数多く見られる様になりました。この背景には、アプリケーションが複雑化するにつれて、CSP モデルの有効性が再注目されている様に思います。
　CSP はプロセス代数の一つでありプロセスの振る舞いを数学的に記述できする事ができます。その後にモデル検証ツールを用いてモデルが正しいかどうかの検証をします。CSP モデルの検証ツールには、LTSA/SPIN/FDR2 /PAT3/Verum/Moby/ProB/CONPASU/CSP-Prover などがあります。特にPAT3 はReal-Time CSP などサポートされていますので、組み込み系のアプリケーションのモデル検証として
使えます。
　PAT3 には多くの機能が用意されていますが、とりわけCSP モデルが中心となってますので、ある程度
CSP の理解が必要とされます。従ってこのテキストでは、第１章でCSP プロセス概論、第２章でトレース
とその意味、第３章で拒否、失敗、失敗発散、第４章でPAT3 の構文と使い方、第５章でCSP モデルのデ
ザインパターンとPAT3 の基本的な使用方法、第６章でTimed-CSP 概要、第７章でTimed-CSP による
PAT3 の事例、第８章でUML 図へのPAT3 の事例、第９章でStateflow 図へのPAT3 の事例について説明します。
　テキストの構成は、英国Surrey 大学のSteve Schneider 教授のテキスト「Concurrent and Real-time
Systems – The CSP Approach」を主として使い、CSP のデザインパターンを用意し、それらをPAT3 の
コードに書き直す事から入ります。
　このデザインパターンはプログラミングの構造と同じなのでoccam-π/JCSP/XC などのプログラミング
技法へと展開する事ができます。基礎的なデザインパターンの構造が理解できますと、更に複雑なプロセスモデルを考える事ができます。この操作はLEGO マシンの仕組みと同じです。プロセスの遷移法則と代数的法則はプログラム言語の意味を理解するのに役立ちますので添付いたしました。
　CSP コンストラクタの法則性に関してTony Hoare、Bill Roscoe、Steve Schneiderのテキストには書かれていますが、もう少し基本的で有益な内容がTony Hoare、Jim Woodcock、Xinbei
Tangらの資料の中にありますので、その中から抽出し追加致しました。

内容項目

まえがき

第1章　CSPプロセス概論
　　　1.1　CSP プロセスとは
　　　1.2　アルファベット（Alphabet）
　　　1.3　正常終了（SKIP）
　　　1.4　停止（STOP） 
　　　1.5　RUN
　　　1.6　混乱（CHAOS） 
　　　1.7　イベントの定義
　　　1.8　接頭辞（Prefix）イベント
　　　1.9　推論規則（Inference Rules）
　　　1.10　Prefix選択
　　　1.11　ラベル付き状態遷移
　　　1.12　LTSの定義
　　　1.13　チャネル（Channel）の入出力
　　　1.14　再帰（Recursion）
　　　1.15　条件（IF コンストラクタ）
　　　1.16　繰り返し（WHILE コンストラクタ） 
　　　1.17　選択（Choice）
　　　1.18　ガード(Guard) 付き選択
　　　1.19　外部選択(External Choice) コンストラクタ
　　　1.20　内部選択(Internal Choice) コンストラクタ
　　　1.21　逐次(Sequence) コンストラクタ
　　　1.22　並行(Concurrent) コンストラクタ
　　　1.23　隠蔽(Hiding)
　　　1.24　リネーム(Renaming)
　　　1.25　パイプ(Pipe)
　　　1.26　奴隷化(Enslavement)
　　　1.27　優先度(Priority)
　　　1.28　割り込み(Interrupt) 
　　　1.29 索引(Index) 付き付き並列、選択、インターリーブ

第2章　トレースとその意味
　　　2.1　トレース（Traces）
　　　2.2　連結（Catenation）
　　　2.3　制限（Restriction）
　　　2.4　頭尾（Head and tail）
　　　2.5　スター（*Star）
　　　2.6　順序（Ordering）
　　　2.7　長さ（Length）
　　　2.8　選抜（Selection）
　　　2.9　initials/after
　　　2.10　トレースと実行
　　　2.11　充足（Satisfaction）
　　　2.12　TRACE の定義
　　　2.13　STOP
　　　2.14　SKIP
　　　2.15　RUN
　　　2.16　Prefixイベント
　　　2.17　Prefix選択
　　　2.18　チャネル
　　　2.19　条件
　　　2.20　隠蔽
　　　2.21　再帰
　　　2.22　逐次
　　　2.23　選択
　　　2.24　アルファベット並列
　　　2.25　インターフェース並列
　　　2.26　インターリーブ
　　　2.27　割り込み
　　　2.28　トレース等価性

第3章　拒否、失敗、失敗発散
　　　3.1　拒否（Refusals）
　　　3.2　拒否の法則
　　　3.3　安定した拒否（Stable Refusals）
　　　3.4　失敗（Failures）
　　　3.5　安定な失敗（Stable Failures）
　　　3.6　失敗の法則
　　　3.7　失敗・発散・無限のトレース
　　　3.8　詳細化（Refinement）

第4章　PAT3の構文と使い方
　　　4.1　PAT3のインストール
　　　4.2　PAT3のアーキテクチャ
　　　4.3　PAT3のモデルチェック
　　　4.4　定数
　　　4.6　変数
　　　4.6　チャネル
　　　4.7　命題
　　　4.8　Skip、Stop
　　　4.9　Prefixイベント
　　　4.10　アルファベット
　　　4.11　データの操作
　　　4.12　条件、選択
　　　4.13　case文
　　　4.14　while文
　　　4.15　atomic文
　　　4.16　急ぐイベント（Urgent Event）
　　　4.17　外部選択/内部選択
　　　4.18　逐次合成/並列合成
　　　4.19　インターリーブ
　　　4.20　隠蔽
　　　4.21　ガード（Guard）
　　　4.22　プロセスの引数とグローバル変数
　　　4.23　表明（Assertion） の式
　　　4.24　線形時相論理（Linear Temporal Logic）

第5章　デザインパターンとPAT3の使用方法
　　　5.1　碁盤の移動
　　　5.2　到達性（Reaches）
　　　5.3　チャネル入出力
　　　5.4　簡単な通信プロトコル
　　　5.5　プロセスCOPY
　　　5.6　並行
　　　5.7　アルファベットに同期した並行処理
　　　5.8　Stop-and-Wait Protocol
　　　5.9　バッファ
　　　5.10　スタック（Stack）
　　　5.11　ABP（Alternating Bit Protocol）
　　　5.12　パイプ（Pipe）
　　　5.13　プロセスの選択
　　　5.14　多重化されたバッファ
　　　5.15　One2One チャネル（One2N,N2One）
　　　5.16　共有チャネル（One2Any、Any2One、Any2Any）
　　　5.17　同期送信（parSend）と同期受信（parRead）
　　　5.18　インターリーブ
　　　5.19　マトリックスの掛け算
　　　5.20　円卓の哲学者
　　　5.21　PAT3における詳細化

第6章　Timed CSPの概論
　　　6.1　CSP モデルの階層化
　　　6.2　Timed CSPの表記
　　　6.3　Timed CSP とPAT3 
　　　6.4　時間の間隔（Intervals of Time）
　　　6.5　時間付きイベント（Timed Event） 
　　　6.6　時間付きトレース（Timed Traces） 
　　　6.7　時間付き拒否（Timed Refusals） 
　　　6.8　時間付き失敗（Timed Failures）
　　　6.9　時間詳細化（Timewise Refinement）

第7章　Timed-CSPによるPAT3の適用
　　　7.1　時間オートマタ（Timed Automata）
　　　7.2　タイマーとの同期
　　　7.3　時間付きチャネル出力（Timed Output） 
　　　7.4　耐故障システム（Fault Tolerance）
　　　7.5　時間付きバッファ（Timed Buffer）
　　　7.6　列車の踏み切り制御

第8章　UML図へのPAT3の適用
　　　8.1　コンポーネント要素
　　　8.2　遷移
　　　8.3　シーケンス
　　　8.4　シーケンス図
　　　8.5　並行処理
　　　8.6　パラレル図（1）
　　　8.7　パラレル図（2）
　　　8.8　alt図
　　　8.9　通信図
　　　8.10　アクティビティ図
　　　8.11　状態マシン図
　　　8.12　タイミング図
　　　8.13　CDプレーヤー

第9章　Stateflow図へのPAT3の適用
　　　9.1　Stateflow図とは
　　　9.2　排他的（OR）な遷移
　　　9.3　自己ループル遷移

　付録：稲盛財団京都賞受賞
　付録：数学的背景
　付録：CSPで使用される記号と意味
　
　参考文献