並列処理を検証する、CSP関連のまとめ

　並列処理関係の検証をするとき、CSPで記述して、確認するけど、その一連＆関係するもののまとめ

---

■CSPで検証する手順

１．CSPで、関係を記述する
　　→状態遷移図なんかを応用して記述できる

２．記述したCSPをType Checkerで確認する
　　→文法ミスを確認してくれる。FDRに直接かけると、エラーだらけの場合、よくわからない

３．FDR2にかける
　　　３－１．まず、読み込ます
　　　３－２．デッドロックフリーとか、詳細化関係(同じかどうか）のチェック
　　　３－３．もし、問題あれば、デバッガでトレース確認
　　　３－４．ちなみに、計算とかもさせられる（Evaluate機能）

４．状態遷移を詳細に見たいのであれば、状態遷移導出ツールProBEが使える

５．Javaでシミュレーションさせたいとなると、JCSPを使う。

---

■CSPと、そのほかのモノとの関係

CSPで記述してFDRで調べる方法も、モデル検査の１つ。
モデル検査としては、他に、SPIN、SMV、UPPAAL、LTSAなどがある。

まず、このちがいについて。

SPIN、SMVとCSPの大きな違いは、前者が、時相論理を使うこと。
時相論理で表現できないような性格のものは、SPIN,SMVでは扱えない。
一方、CSPは、モデルはCSPで記述する（詳細化関係を調べるが、それもCSP）。
時相論理がかけないヒトも（かけないコトも）チェックできる。

LTSAは、FSPという記述言語で状況を記述する。このFSPは、CSPに似ている。
で、LTSAは、LTSっていう図にしてくれるんだけど、あれは、図を楽しむものなの？？
→よくわかってない・・

UPPAALは、そもそも時間概念が扱えるので、かなり違う。

---

■JCSPとJPFについて

　JCSPは、並行システムのシュミレーションをするけど、同じく並行システムを調べるものとして、
JPF（Java PathFinder）がある。

　この違いについて。

　JCSPは、CSP表現したものをJavaでシミュレートしやすくしたもの。
　なので、楽しむことは出来ても、エラーについては、実機確認の域を出ない。

　一方、JPFは、ある程度のケースについて（深さは自分で設定仕様と思えばできるけど、普通デフォルトで使うよな）自動的に検証してくれる。

　たとえば、哲学者の食事問題の戦略について調べようとする。

　CSPで記述し、FDRにかければ、デッドロックするかどうかはわかる。
　このCSP記述を元に、JCSPを記述した場合、対応関係を持ちながら記述することは出来るが、
　楽しめるだけで、必ずしもデッドロックするかどうかはわからない。

　一方、哲学者の食事問題をJavaで記述し（CSPの記述と離れてしまってもよい）
　JPFで検証した場合、ある程度のケースを(場合わけして）検証して、
　デッドロックをちゃんと検出する。

EventBの書き方について

前に、ツールの話は書いたので、今回は、書き方について。

Event-Bは、Bとちがって、２つの部分に分かれる。
MachineとContext（別々のファイルになる）

Contextは、おもにSet（集合）の内容を記述する。記述項目は、こんなかんじ

CONTEXT
EXTENDS
SETS
CONSTANTS
AXIOMS

一方、MACHINEは、Contextを取り込んで、実際にいろんな記述をしていく。項目内容はこんな感じ
MACHINE
(REFINES)
SEES
VARIABLES
INVARIENTS
THEOREMS
EVENT
(VARIANT)
END

このうち、REFINESとVARIANTはリファインメント（あるEvent-B記述をさらに詳細化したもの）で使用します。
SEESで、参照するCONTEXTを指定する。

ってことで、以下、CONTEXTから。

---

■CONTEXTの内容について

CONTEXTは、以下のことを書く。
CONTEXT
EXTENDS
SETS
CONSTANTS
AXIOMS

　つまり、集合と定数という、型とか、固定的な値（変数のように、インスタンスでないもの。クラス定義するようなもの）を宣言する。
　以下、それぞれについてみていく。

●CONTEXT
　CONTEXT　コンテキスト名
　コンテキストの名前を指定する
　
●SETS
　SETS
　　　集合名１;
　　　　：
　　　集合名N

　集合を宣言していく。

●CONSTANTS
　CONSTANTS
　　　定数名１;
　　　　：
　　　定数名N
　定数を「宣言」していく。

●AXIOMS
AXIOMS
ラベル１: 定数１：型１

　ここで、定数の型を指定する。
　型は、NAT1など、あらかじめあるものか、上記SETSで指定したもの

(例）
CONTEXT SampleContext1
SETS
MYSET
CONSTATNTS
val1
AXIOMS
　　axm1 : val1 : MYSET
END

---

■MACHINEの内容について

　実際の記述は、MACHINEでやる。Bとちがい、リファインメントしたものでもなんでも
MACHINE。MACHINEには、以下の内容を書く。

MACHINE
(REFINES)
SEES
VARIABLES
INVARIENTS
THEOREMS
EVENT
(VARIANT)
END

以下、こんなかんじ。
●MACHINE
　MACHINE マシン名

　マシン名を適当に決めて書く

●SEES
　SEES
　　コンテキスト名

　利用するコンテキストを指定する

●VARIABLES
　VARIABLES
　　変数名

　利用する変数を宣言する

●INVARIANTS
　INVARIANTS
　　ラベル名：変数：不変条件
　変数の不変条件をかく。つまり、変数が満たすべき制約を書く。
　ということは、変数の型とか、範囲とか、変数間の関係とか。
　条件をいくつか書くと、条件間のANDとなる
　（ORは条件内にORと書く）

●EVENTS
　イベントをかく。
　はじめに、INITIALIZATIONがあるので、そこに初期化条件を書く。
　BEGINのあとに、
　　　ラベル名：式
　の形。代入は：＝

　INITIALIZATIONを書いたら、つぎから、書きたいイベント（処理）をかく。
　処理自体は、BEGINの中に、同じように書く。

●VARIANT
　変わっていく変数(負のすうにはならない）で、どんどん減少していくもの
　停止性を証明するためには、必要

---

こんなかんじかな。一部しか書いてないけど・・・
まちがってたら、ごめん。