そのあと、モデル検査の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:タイムドオートマトンテスト中

モデル検査のPATの話を聞いてきた！

きのう、第73回先端ソフトウェア科学・工学に関するGRACEセミナー[4/17開催]に行って、モデル検査のPATの話を聞いてきた。

内容をメモメモ（英語できいたのを日本語で書いているので、間違いとかあるかもしれないし、おかしいところがあると思う。ごめん）

---

Event Analytics and verification : PAT Approach

Intel Pentium 1994 Bug
4195835 - 4195835 / 3145727 * 3145727 = 0
0でなく256を返す？
ルックアップテーブルのミス

Airbus A380 のソフト問題

Therac-25 放射線当てすぎ
Proton Therapyのマシンクラッシュ２０１４

これらのもんだいにたいして→形式仕様
１９４９　アランチューリング
　Checking Large Routine
１９６７　フロイド
１９６９　ホーア

モデルチェッキング
・２００７年　ＡＣＭのチューリングしょう
・２００９年　インテル　i7のモデルチェッキング
・The Slam Project（まいくろそふとリサーチ）
→産業界のメインストリートへ

ＰＡＴシステム
分散アルゴリズム、Ｗｅｂサービス・・・
モデリング：コンカレントモジュール
抽象化
Intermediate
分析

ＰＡＴはホーアのＣＳＰがもと

アクション a→P　プロセス
ＶＭＵ（ベンディングマシン）＝coin→STOP
ＶＭＵ（ベンディングマシン）＝coin→Choc→STOP
　　（choc:チョコレート：チョコがかえる自販機）

他のＣＳＰのかきかた
・ P;Q
・P||X||Q
・外部選択：チョコか緑茶かコカコーラか→コントロール不可
　内部選択：どの緑茶をだすか→機械が選択する
・インタラプト：P1が起こっていたのにeが起こるとP2に変わる

パラレル　コンポジション
(a→Ｐ）｜｜a｜｜（C→a→ｑ）のとき、はじめにおこるのは？
　　→Ｃ、でないとＣが起こるまで待ってしまう

こんかれんしーの法則
　aはＰに属し、Ｑに属さない
　bはＰに属さず、Ｑに属す
　C,dはＰも属し、Ｑに属す
としたとき、
c→Ｐ｜｜ｄ→Ｑ　デッドロックでとまる

リアルなはなし
・オバマとプーチン
オバマ：チェスボード→チェス[]テニスラケット→テニスする
プーチン：チェスのこま→テニスする[]ボール→テニスする　
このとき＜チェスのこま、テニスラケット＞　　デッドロック

ＣＳＰはデッドロックを解決する

国連：チェスボード→チェスのこま[]テニスラケット→テニスボール

で、オバマ｜｜プーチン｜｜ＵＮにする！

デッドロックを機械で探す

ケーススタディー：キーレスシステム（自動車）

ＰＡＴでは、捨象してかんがえる（ショッピングモールはどうでもよく、遠くにいるでいい）

[コンデション]イベント→アクション

define
var
define 状態
assume　なると困る状態

デモンストレーション

最近のワーク
・pervasive Model Checking
・Towards Event Analytics

数字を動かすパズルゲームへの応用

実験結果
・ＰＡＴとNuSMVとSatPlanの時間比較

モデルチェキング
ぱっとの学生がＣＳ４２１１で勝った
・ＰＡＴは学ぶの簡単


プロバブリスティックモジュール
・ごめん、ナダルがすごいという話・・・よくわかんなかった。
　　ナダルとフェドラ？どっちが勝つか、ＰＡＴのモデルで
→確率が書ける！！（実際の結果から持ってきた）

ＭＤＰ：マカオ　ディシジョン　プロセス？？

・ナダルの実際の状況でシミュレーション
・エラーを少なくするという戦略に変えて、シミュレーション

このデータ（確率）をリアルタイムで自動的に取れたら？

リアルタイムモジュール
・日本人の行動と・・・（自主的に省略）のシミュレーション


リアルタイム＆プロバビリティー
　リフト（エレベーター）
・Ｃ＃でのインプリメント
・ＰＡＴチェッキング：
　　　　リフトのすべてが、同じ（１）


http://pat.comp.nus.edu.sg
３０００を超える登録ユーザー
　マイクロソフト、ＨＰ，ソニー、日立

ＦＭ２０１４は、シンガポールで！

質疑は、ごめん、英語力より形式仕様の力がなくてわかんなかった。

ビッグデータでは、人が呼べない？

今、富士通フォーラムのセミナー申し込み

http://forum.fujitsu.com/2014/tokyo/seminar/

を見て思った。
（セミナーを申し込むボタンをクリックすると、満席かどうか見れる。
　４月１８日１１時現在の話）

仮想化、クラウドは、いっぱい満席出てる（セミナーもたくさん）。
オープンデータも満席率高い。

だけど、ビッグデータ、S12-1,S17-3,S21-2,S24-1のうち、
満席なのは、S24-1のみ・・・
（ビッグデータという言葉は入ってないが、S27-3も
ビッグデータ関連。でも満席になってない）

マイナーな、オープンデータは
S13-1,S14-1,W15-1
このうち満席はS14-1,W15-1
（S13-1は富士通でなく、総務省の人が話す）

ビッグデータの満席率、低くないか？
昔は、ビッグデータといったら、もっと満席率、高かったような・・・
ビッグチャネルの関連としては、M2M、オムニチャネルだろうが
オムニチャネルも満席になっていない・・・

ビッグデータでは、人が呼べない？