CPS-IoTゼミ 発表資料
確率的モデル検査ツール PRISMの検証
2017/08/31
種村 嘉高
猿渡 真之介
図司 達まえがき
CPS/IoTソリューションではセンサーから膨大で多様データを収集/解析する必要があるため、IoT固有の非機能要件(例：セキュリティ、転送速度、データ処理速度)を満たす必要がある。
これらはシステム開発初期の段階からパフォーマンスを事前検証できることが望ましいが、時間面/費用面の制約から難しい場合が多い。
確率モデル検査ツールは時間要素と確率要素を含めたモデルの定量的評価を行う事が出来るため、CPS/IoTソリューションのパフォーマンス検証に有効と考えられる。
例として簡易なネットワークモデルを題材とし、確率モデル検査ツールの有効性2を検証する。

目的
確率モデル検査ツールとしてPRISMを選定した。
PRISMを使って、以下の検証を実施する事を目的とする。
1.PRISMの有効性○ 今回の例題に対する、確率モデルの定量的評価の有効性

2.PRISMの使い方○ 確率モデル検査ツールとしての利用方法、ノウハウ

3

背景PRISMの選定理由●確率モデルを扱うための代表的なツールであるためその他のモデル検査器として・Process Analysis Toolkit
・Uppaalを検討したが、確率モデルを扱うことが出来なかったため、 採用を見送った。

4

PRISMとは
PRISMはランダムまたは確率的な挙動を示すシステムのモデリングと分析のための確率モデル検査ツールである。
PRISMはいくつかのタイプの確率モデルを構築し、論理式が真となる確率を検査できる。
状態遷移系として、以下３種類のマルコフ連鎖を対象とすることができる。
●離散時間マルコフ連鎖（DTMC）●連続時間マルコフ連鎖（CTMC）●マルコフ決定プロセス（MDP）

5

作成モデル(1/2)
l モデルの「登場人物」と「イベント」を以下のように定義
Message [No.]

受け渡されるデータ

Server

データの作成/処理/転送を実施

Path

データの転送路

Switch

データの転送を実施

登場人物

Create(r)データの作成Pass(r)

データの転送Process(r)データの処理イベント ()内は発生確率

6

作成モデル(2/2)
その他制約事項lメッセージの生成・転送・処理は非同期に規定確率に基いて実行される
lメッセージはネットワーク中複数存在することが可能
lメッセージが作成されてから処理されるまでの間は必ずいずれかのサーバ、もしくはスイッチ上に存在するlサーバ、スイッチは一度に一つのメッセージしか保有できない
p メッセージ生成時や転送時に既にメッセージが存在する場合
7
はイベントを発生させない(発生確率を0とする)…先が詰まっている状態

評価環境● 現実的に起こりうるネットワークのトポロジーを想定して、以下の3パターンでモデル化。(Case3が最速になると想定)

Z

S

S

S

X

X

X

Y

E

Case1:STP
シングルパス(非最短経路)

Z

Y

E

Case2:STP
シングルパス(最短経路)

Z

Y

E

Case3:SDN
マルチパス

8

評価環境
● 前頁3パターンでS-X,Z-E間でPassが発生する確率を変化させ遅延を評価○X-Y,Y-Z,X-Z間でのPassの発生確率を5(回/秒)○SでのCreate、EでのProcessの発生確率はともに100(回/秒)○メッセージを10個作成・処理されるまでに要した時間の期待値を評価(評価時間は30秒)

9

実験結果
SX

スイッチ間転送 5(回/秒)
サーバ処理 100(回/秒)

Z

SX
YE

Z

S
X
Y

E

Z

Y

E

S-X Z-E間 転送

Case1

Case2

Case3

50(回/秒)9.24±0.18

4.41±0.10

3.75±0.08

5(回/秒)

13.18±0.21

9.40±0.17

9.33±0.18

10メッセージの総滞在時間

・より効率的な転送パス(1<2<3)を活用することで生まれる速度差を定量的に評価・効率的な転送パスを採用しても他にボトルネックがある場合(Case3のZ-E間の下段)10
大きな差が生まれないケースが存在する事も確認

PRISMのベストプラクティス
理想START4)モデルを評価

1)モデルを図で描く
・極力シンプルに・何を確かめたいかを明確に
2)Prism上でモデルを記述
3)モデルの評価項目を定義
現実解＊)振る舞いの結果についての仮説を立てる

4-1)Simulatorでステップバイステップで実行
4-2)Experimentでグラフを描く4-2’)Simulationを処理リソース 使って評価(後述)
不足時4-3)Non probabilistic
propertyで網羅的に今回振る舞いを検査する
施未実

戻る5)仮説を検証する
難易度高検証を行う、決められた手法がないので、工夫が必要
・多人数で検証する・ドメインエキスパートに確認を取る
・実際のシステムから結果を取得して比較11

モデルの記述(1/3)● モデルの記述の仕方○ モデルのモジュールの取り方で記述しやすさが異なった
i. スイッチを基本のモジュールとする● テンプレート→スイッチを追加しやすい● 評価のために各データのモジュールが必要→送るデータを増やす際の記述量が多い
ii. データの状態(位置情報など)を基本のモジュールとする● データをID番号で管理→ID番号をスケーリングすることで送るデータの数を簡単に変更できる(今回はii.が重要)
12モデルの記述(2/3)● モデルの記述の仕方
モジュールのテンプレート
PRISMにはモジュールの記述を置換する記述法がある→モジュールのテンプレートを作成、テンプレートの変数を具体的な変数に置換することで容易にモジュールを追加
テンプレートテンプレートを利用したモジュール13

モデルの記述(3/3)● モデルの記述の仕方
監視モジュールの設置
時間の計測には微小時間ごとにシステムの状態を確認する監視モジュールを用意、計測対象の状態なら微小時間を返す
監視モジュールが返した時間の累積をシステムがその状態であった時間とする
監視モジュール
SX

Z
E

もしシステムが時間を計測したい状態なら、監視する間隔である微小時間を返すY

14

モデルの評価(1/2)● モデルのバリデーション
方式として、ExperimentとSimulationがあり、それぞれの意味はExperiment：確率的に解を求める
Simulation：統計的に解を求めるである。計算量（処理時間）、正確性のトレードオフになっている。
計算量（処理時間）

正確性

Experiment△(⼤きい)◎(⾼い)

Simulation◎(⼩さい)△(低い)

Experimentを実行した際にPRISMが固まる、落ちることがあり、その場合はSimulationで代用した。

15

モデルの評価(2/2)● モデルのバリデーション
モデルの変更後や実験結果の妥当性が疑われるとき→シミュレータで意図しない挙動がないか、実験のパラメータを変化させてグラフの形状の特徴や変化を確認する

16

結論
1.PRISMの有効性
現実の課題をモデル化して広範囲な条件下で確率モデルの定量的評価を行い、仮説を検証する事が出来た。

2.PRISMの使い方
PRISMを使った確率モデルの定量的評価の手順を確立する事が出来た。

17

マルコフ過程/マルコフ連鎖
マルコフ過程（Markov process）
未来の挙動が現在の値だけで決定され、過去の挙動と無関係であるという性質(=マルコフ性)を持つ確率過程を指す。

マルコフ連鎖（Markov chain）
確率過程の一種であるマルコフ過程のうち、とりうる状態が離散的（有限または可算）なもの（離散状態マルコフ過程）を指す。

18

離散時間マルコフ連鎖
離散時間マルコフ連鎖（Discrete-time Markov Chain）
時間が離散的に推移するマルコフ連鎖を指す。

19

連続時間マルコフ連鎖
連続時間マルコフ連鎖（Continuous-time Markov Chain）
時間が連続的に推移するマルコフ連鎖を指す。

20

マルコフ決定過程
マルコフ決定過程（Markov Decision Process）
状態遷移が確率的に生じる動的システム（確率システム）の確率モデルであり、状態遷移がマルコフ性を満たすもの指す。
マルコフ連鎖に（選択可能な）行動、および（行動を計画する動機を与える）報酬を追加し拡張したものである。

3つの状態と2つの行動をもつ簡単な MDP の例

21