並列処理を検証する、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で検証した場合、ある程度のケースを(場合わけして）検証して、
　デッドロックをちゃんと検出する。