システム検証基礎演習 10/1
モデル検査システムとは何か Model Checking system Model Checker その名の通り、モデルを検査する モデルとは何かというと ほとんどのシステムでそれはオートマトン Model = オートマトン オートマトンの性質を検証・検査する 性質は、論理式で記述する SPINの場合は内部的にはオートマトン Promelaという並行プログラミング言語で記述できる これが特徴 モデルチェッカーによってはオートマトンをグラフィカルに書くものもある どちらがいいかは議論の分かれるところ モデルの調べたい性質を記述する論理式はLTL(Linar Temporal Logic) そんなに難しいものではない []P Pが常に成り立つ <>P Pがいつか成り立つ オートマトンが時間で遷移していく中で 時間に関する様相記号がある 教科書『4日で学ぶモデル検査』 重視したいのが5章 人食い土人と宣教師問題と排他制御問題を中心にやっていく 「人食い土人」という言葉を使うとまずいので 教科書ではうさぎちゃんとおおかみちゃんの問題になっている 排他制御の問題は、 OSの授業で出てくるDekkerのアルゴリズムなどを書いて 排他制御がきちんと出来ているか確認する SPINのしくみ foo.pml ↓spin.exe モデル検査をするプログラムを作るプログラム pan.c ↓gcc pan.exe ↓実行 モデル検査 ↓ デッドロックする計算過程 ↓spin.exe シミュレート 計算過程を再現するシミュレート 単純なシミュレートもできる 非決定的な動作ときにはランダマイズして実行される SPIN自体のインストールは簡単 だけどgccが必要 授業の前半はまったりとSPINを使っていく
