昨日（３月１７日）、プロセス分析ツールPATによるモデリングとモデル検査を聞いてきた！その内容をメモメモ
■ごあいさつ 石川先生（日本語）
・今日は２部構成
・第一部は、大御所Jin-Song Dong先生
・テニスにつかってみよう！という話
■Event-Strategy Analytics based on formal analystic and verification with a new application domain on sports analytics
講師：Jin-Song Dong先生（英語）
・PATの紹介と新しい適用（スポーツ分析）
・形式使用の例
宇宙
がんちりょう
・形式仕様の初期の論文
アランチューリング
ホーア
E.クラーク：モデルちぇっキング→インテルなんかもつかってるよね
・PATの８年間
日本のユーザーグループ
・はじめの例：（車の）キーレスシステム（KCSとするみたい）
キーの問題：
鍵を車において、ロックしちゃったとき
買い物などで、手にいっぱい物持っているとき
→中にキーがあるなら、ロックできないようにすればいい！
PATを使ってといてみよう！
・PATにおけるKCSの変数と定数
#define
var
しなりお：平行に流れる
オーナーの状態とシナリオ
キーの状態とシナリオ
ドアの状態とシナリオ
モーターの状態とシナリオ
・Reasoning
鍵が中にあるケース
奥さんが車、自分が遠くで、かぎもっている
→これらをないようにしたいassertで調べる
・デモ
PATで実行
→PATはエレガントなストーリーを生成してくれる
・AIのプランニング、問題解決としてのモデルチェッキング
数字のパズルの例
AIプランニングツール、PAT,NuSMVとの比較
・学生さんがやった、旅行プランについて
確率的モデルチェッキング
モンティホール問題
３つのドアのうち、１つに車が入っている
選ぶ
１つあける＝くるまない
そのあと選択を変えたほうがいい、わるい？
（→説明してくれたけど、よくわかんない）
PATでといてみる
・モデルチェッキングが意思決定にやくだつ
新しいドメインへの適用－スポーツ分析
・２０１４年、ブラジル VS ドイツ
ドイツが勝った理由、１３人目の選手は・・・SAP
・スポーツ分析にモデルチェッキングを適用する
→モンティホールのように
→テニス
シナリオ：フェドラーとナダル
数字ならフェドラー
ところが、このくみあわせ、ナダルが２３勝１０敗
→ストラテジーの問題
ナダルの戦略
フェドラーの戦略
モデル記述
→パブリックドメインのオンラインデータを使う
デモ（このPATプログラムはパブリックではない？）
ナダルが勝つが、ここの数字を２かえると、フェドラーがかつ
・確率的モデルチェッキングのケーススタディ：４人のKuhnポーカー
・イベント分析
意思決定のモデルチェッキングに基づいている
データ分析は内部ブラックボックス
・スポーツ分析を超えて
Q&A
・プロジェクトの予測に使える？
・どのくらいの抽象度で記述する？
テニスはドメイン知識があった
■PATハンズオン～PATによるモデリングとモデル検査の実際～
藤本さん（日本語）
PATの概要
・モデル検査の対象と表現・ツール
振る舞いモデル
オートマトン
・とりえる状態の遷移：SPIN
プロセス代数
・プロセスを数式として定義：CSPなｄｐ
・通信しながら並行動作するシステム
スレッドができる言語でないとできないけど
→車載システム：ECU
これから重要：バグの再現性
・CSPについて
こみゅにけーてぃんぐ・しーけんしゃる・プロセスの略
ホーアさんがつくった
TOPSE:並列システムの検証と実装
・式としての並行プロセス
CSPではプロセスを式で表す
式は演算子と被演算子で構成される
プロセスP,Qの並行合成 P || Q （PとQが並行で動く）
・PATとは
ぷろせす あなりしす つーるきっとの略
CSPの方言（CSP#)
→だけど、CSP以外の言語も入れられる（拡張モジュール）
モデル検査：
時相論理式のモデル検査
詳細化関係を使った検査
・PATのアーキテクチャ
コンカレントモジュール
リアルタイムモジュール；時間要素を含む
確立つきモジュール
Webサービス記述用
いったんまとめる
エンジン
・PATを利用したモデル検査の流れ
モデリング
シミュレーションによる妥当性検討
モデル検査による動作の証明
→凡例：トレース情報
・PAT基本演算子
PATデータの宣言
エディタ
・モデル編集：画面の各部分
モデル編集：作成 File→New→CSP
シミュレーション機能
・適当なタイミングに戻ってみることができる
→デバッグ
・演習
モデル１：硬貨を１ついてると、壊れる自動販売機
VM1=(coin->Stop);
モデル２：２回利用すると壊れる
VM2=(coin->(choc->(coin->(choc->Stop))));
モデル３：こまがいけるところ
CTR=right->up->right->right->down->Stop;
Stop:デッドロック、異常終了
・トレースグラフの編集
・選択、再起を含むモデル
選択により、プロセスの実行が制御される
選択には、外部選択、内部選択がある
P=a->b->Stop[]c->d->Stop;
再帰：繰り返し構造
P=a->b->P;
・決定的な選択と非決定的な選択
・モデル４：選択を含む例
VMCT=coin->(choc->VMCT[]toffee->VMCT);
・並行動作する複数プロセス
P||Q 並行：同期する
P|||Q インターリーブ：同期関係ない
・チャネル通信する並行プロセス
ch!x 送信
ch?y 受信
・演習３．１
P1 = a->x->b->Skip;
Q1= a->y->b->Skip;
Spar=P1||Q1;
Sint=P1|||Q1;
Sseq=P1;Q1;
・例：ギア制御の（ドライバ）モデル（状態遷移図）
絵を見ながら、モデルは機械的にかけます
モデル検査
・２つの流儀
１：詳細化関係：プロセスの等価性→CSPでは伝統的
２：時相論理による検査
・その他：よく使うもの
deadlockfree,reachesなど
#assert P1 deadlockfree;
・モデル７：ドリンク ディスペンサー
DD=(setorange->O [] setlemon->L);
O=(orange->O[]setlemon->L[]setorange->O);
L=(lemon->L[]setorange->O[]setLemon->L);
#assert DD deadlockfree;
・哲学者の食事
資源共有、排他制御、スケジューリング
隠蔽することができる
・状態遷移モデルとの対応
時間制約付きモデル Timed CSP
・デッドライン、タイムアウト
２つある
Timed Automaton：時間変数
Timed CSP：演算子、プロセスの導入
RTSモデルを選ぶ
・プロセス
Delay
Timeout
割り込み interrupt[t]
デッドライン
開始時間 within[t]
Urgency ->>
e1->P2() 時間はわからない（0～無限大）
e1->>P2() ただちに実行
確率的過程モデル
■ごあいさつ 石川先生（日本語）
・今日は２部構成
・第一部は、大御所Jin-Song Dong先生
・テニスにつかってみよう！という話
■Event-Strategy Analytics based on formal analystic and verification with a new application domain on sports analytics
講師：Jin-Song Dong先生（英語）
・PATの紹介と新しい適用（スポーツ分析）
・形式使用の例
宇宙
がんちりょう
・形式仕様の初期の論文
アランチューリング
ホーア
E.クラーク：モデルちぇっキング→インテルなんかもつかってるよね
・PATの８年間
日本のユーザーグループ
・はじめの例：（車の）キーレスシステム（KCSとするみたい）
キーの問題：
鍵を車において、ロックしちゃったとき
買い物などで、手にいっぱい物持っているとき
→中にキーがあるなら、ロックできないようにすればいい！
PATを使ってといてみよう！
・PATにおけるKCSの変数と定数
#define
var
しなりお：平行に流れる
オーナーの状態とシナリオ
キーの状態とシナリオ
ドアの状態とシナリオ
モーターの状態とシナリオ
・Reasoning
鍵が中にあるケース
奥さんが車、自分が遠くで、かぎもっている
→これらをないようにしたいassertで調べる
・デモ
PATで実行
→PATはエレガントなストーリーを生成してくれる
・AIのプランニング、問題解決としてのモデルチェッキング
数字のパズルの例
AIプランニングツール、PAT,NuSMVとの比較
・学生さんがやった、旅行プランについて
確率的モデルチェッキング
モンティホール問題
３つのドアのうち、１つに車が入っている
選ぶ
１つあける＝くるまない
そのあと選択を変えたほうがいい、わるい？
（→説明してくれたけど、よくわかんない）
PATでといてみる
・モデルチェッキングが意思決定にやくだつ
新しいドメインへの適用－スポーツ分析
・２０１４年、ブラジル VS ドイツ
ドイツが勝った理由、１３人目の選手は・・・SAP
・スポーツ分析にモデルチェッキングを適用する
→モンティホールのように
→テニス
シナリオ：フェドラーとナダル
数字ならフェドラー
ところが、このくみあわせ、ナダルが２３勝１０敗
→ストラテジーの問題
ナダルの戦略
フェドラーの戦略
モデル記述
→パブリックドメインのオンラインデータを使う
デモ（このPATプログラムはパブリックではない？）
ナダルが勝つが、ここの数字を２かえると、フェドラーがかつ
・確率的モデルチェッキングのケーススタディ：４人のKuhnポーカー
・イベント分析
意思決定のモデルチェッキングに基づいている
データ分析は内部ブラックボックス
・スポーツ分析を超えて
Q&A
・プロジェクトの予測に使える？
・どのくらいの抽象度で記述する？
テニスはドメイン知識があった
■PATハンズオン～PATによるモデリングとモデル検査の実際～
藤本さん（日本語）
PATの概要
・モデル検査の対象と表現・ツール
振る舞いモデル
オートマトン
・とりえる状態の遷移：SPIN
プロセス代数
・プロセスを数式として定義：CSPなｄｐ
・通信しながら並行動作するシステム
スレッドができる言語でないとできないけど
→車載システム：ECU
これから重要：バグの再現性
・CSPについて
こみゅにけーてぃんぐ・しーけんしゃる・プロセスの略
ホーアさんがつくった
TOPSE:並列システムの検証と実装
・式としての並行プロセス
CSPではプロセスを式で表す
式は演算子と被演算子で構成される
プロセスP,Qの並行合成 P || Q （PとQが並行で動く）
・PATとは
ぷろせす あなりしす つーるきっとの略
CSPの方言（CSP#)
→だけど、CSP以外の言語も入れられる（拡張モジュール）
モデル検査：
時相論理式のモデル検査
詳細化関係を使った検査
・PATのアーキテクチャ
コンカレントモジュール
リアルタイムモジュール；時間要素を含む
確立つきモジュール
Webサービス記述用
いったんまとめる
エンジン
・PATを利用したモデル検査の流れ
モデリング
シミュレーションによる妥当性検討
モデル検査による動作の証明
→凡例：トレース情報
・PAT基本演算子
PATデータの宣言
エディタ
・モデル編集：画面の各部分
モデル編集：作成 File→New→CSP
シミュレーション機能
・適当なタイミングに戻ってみることができる
→デバッグ
・演習
モデル１：硬貨を１ついてると、壊れる自動販売機
VM1=(coin->Stop);
モデル２：２回利用すると壊れる
VM2=(coin->(choc->(coin->(choc->Stop))));
モデル３：こまがいけるところ
CTR=right->up->right->right->down->Stop;
Stop:デッドロック、異常終了
・トレースグラフの編集
・選択、再起を含むモデル
選択により、プロセスの実行が制御される
選択には、外部選択、内部選択がある
P=a->b->Stop[]c->d->Stop;
再帰：繰り返し構造
P=a->b->P;
・決定的な選択と非決定的な選択
・モデル４：選択を含む例
VMCT=coin->(choc->VMCT[]toffee->VMCT);
・並行動作する複数プロセス
P||Q 並行：同期する
P|||Q インターリーブ：同期関係ない
・チャネル通信する並行プロセス
ch!x 送信
ch?y 受信
・演習３．１
P1 = a->x->b->Skip;
Q1= a->y->b->Skip;
Spar=P1||Q1;
Sint=P1|||Q1;
Sseq=P1;Q1;
・例：ギア制御の（ドライバ）モデル（状態遷移図）
絵を見ながら、モデルは機械的にかけます
モデル検査
・２つの流儀
１：詳細化関係：プロセスの等価性→CSPでは伝統的
２：時相論理による検査
・その他：よく使うもの
deadlockfree,reachesなど
#assert P1 deadlockfree;
・モデル７：ドリンク ディスペンサー
DD=(setorange->O [] setlemon->L);
O=(orange->O[]setlemon->L[]setorange->O);
L=(lemon->L[]setorange->O[]setLemon->L);
#assert DD deadlockfree;
・哲学者の食事
資源共有、排他制御、スケジューリング
隠蔽することができる
・状態遷移モデルとの対応
時間制約付きモデル Timed CSP
・デッドライン、タイムアウト
２つある
Timed Automaton：時間変数
Timed CSP：演算子、プロセスの導入
RTSモデルを選ぶ
・プロセス
Delay
Timeout
割り込み interrupt[t]
デッドライン
開始時間 within[t]
Urgency ->>
e1->P2() 時間はわからない（0～無限大）
e1->>P2() ただちに実行
確率的過程モデル
アクセス
トータル
ランキング
