そのあと、モデル検査のPATを勉強してきた・・・はず？

そのあと、「プロセス分析ツールPATで学ぶ並行プロセスのモデル検査(4/17)」でPATを習ってきた。その内容をメモメモ

---

基本操作
・編集する
・シミュレーションする
・検査する

PATのモデル
・オートマトン
・CSP：プロセス代数

PATを利用したモデル検査の流れ
・モデリング
　　　テキストエディタ
・シミュレーション
　　　ランダム
　　　合成プロセス
・検査画面
　　　満たすべき性質をassertで並べる

モデル編集
・テキストエディタ
・メッセージボックス
・メインメニュー

モデル編集・作成
Fileメニューから選ぶ
　　CSPモデル
　　RTS
→エディタが開く。保存時のファイル拡張子がモデル選択により違う
　Check Grammerを押すと、構文チェック
　（シミュレーションとかしたときも入る）
　エラーメッセージも

シミュレーション
・真ん中シミュレーショングラフ。
　動的に成長
・トレース出る
・プロセスの名前選べる
　　　→選んでしまうと、そのプロセスのシミュレーション
外部・内部選択
再帰：制御移動

並行動作
P||Q
同じ名前が出てきたら、同期する
インターリーブ
P|||Qまったく非同期

チャネル　ch バッファの大きさ
channel ch 0; 0だと同期通信
! 送信
? 受信　?変数：変数にいれる　?定数：その定数なら先に進む

モデル検査
流行（SPIN,SMV)
　→PATは後続
　　プリズム、うっパール、すぴんと比較

CSPの枠組みの検査
　　プロセス同士の関係の比較
　　　　等価性、リファインメント
時相論理式を書く（LTL)
→PATは、両方　　　　
　　トレース詳細化、失敗詳細化、失敗発散詳細化

Verificationを選ぶ：１枚しか出ない
相互再帰

DP:哲学者の食事問題
＠：しぐまみたいなの

可読化
状態遷移モデル（図・表）と式の対応
　　→機械的な変換でPATで検査できる

時間制約
RTS：動作（ふるまい）をモデル化
非機能要件：時間→コードにはいってくること
　　assertion タイマー
タイムドオートマトン
タイムドCSP→RTS
　ディレイなど使える。
e1->P2()は０～無限大にうごく
　デッドラインは、それを制限できる
　－＞＞は、すぐに遷移する

Train Gateというモデル（サンプルとして入っている）
うっぱーるをPATに移植

NesCモジュール：センサーネットワーク

うっぱーるの使い分け
　うっぱーる：安定していて、事例がある
　PAT:タイムドオートマトンテスト中