Symbolic Model Checking

Systems and Software Verification
4. Symbolic Model Checking
システム情報科学府情報工学専攻
荒木研究室修士2年住田辰雄
目次
•
•
•
•
•
4.0 記号モデル検査
4.1 状態集合の記号計算
4.2 二分決定グラフ (BDD)
4.3 BDDsによるオートマトンの表現
4.4 BDDに基づくモデル検査
2006/9/28
モデル検査勉強会
2
4.0 記号モデル検査
• 記号モデル検査
– 検証を目的とするオートマトンの状態や遷移
を記号的に表現するモデル検査手法を指す
– 本書では，特に二分決定グラフを用いるモデ
ル検査手法について言及する
2006/9/28
モデル検査勉強会
3
4.1 状態集合の記号計算
• Sat(φ)
– φを満たす状態の集合
– Sat(φ)はPre演算子とSat(ψ) の集合によって求
めることができる
• Pre(S)
– Sの前の状態の集合
» A = <Q, T, q0, l>
» S⊆Q
2006/9/28
モデル検査勉強会
4
4.1 状態集合の記号計算
• Sat(φ)
Sat ( )
 Q \ Sat ( )
Sat (  ' )
Sat ( EX )
Sat ( AX )
 Sat ( )  Sat ( ' )
 Pre( Sat ( ))
 Q \ Pre(Q \ Sat ( ))
Sat ( EF )
 Pre* ( Sat ( ))
...
• Q\X
– Qのサブ集合Xの補集合
• Pre*(S)
– Sの0回以上前の状態の集合
2006/9/28
モデル検査勉強会
5
4.1 状態集合の記号計算
/ *  Computatio n of Pre * (S) (for Sat [EF psi])  * /
X : S;
Y : {};
while (Y ! X) {
/ * Y is not a fixed point * /
Y : X;
X : X \ / Pre(X);
/ * \ /  set union * /
}
return X;
Aが有限であれば，停止性は保証される
2006/9/28
モデル検査勉強会
6
4.1 状態集合の記号計算
/ *  Computatio n of Sat [A psi1 U psi2]  * /
P1 : Sat[psi1];
P2 : Sat[psi2];
X : P2;
Y : {};
while (Y ! X) {
Y : X;
/ * not yet stabilized * /
/ * / \  set intersecti on * /
X : X \ / (P1 / \ (Q \ Pre(Q \ X)));
}
Aψ1Uψ2 ≡ ψ2 ∨ (ψ1 ∧ EX true ∧ AX(Aψ1Uψ2))
return X;
2006/9/28
モデル検査勉強会
7
4.1 状態集合の記号計算
• 時相結合子は不動点として定義することが
できるため，全てのCTL結合子はこのよう
な計算で扱うことができる
2006/9/28
モデル検査勉強会
8
4.1 状態集合の記号計算
•
Sat(φ)の反復計算を実装するには，以下
の基本が必要である
1. 各命題P ∈ Propに対するSat(P)の記号表現
2. Sの記号表現からPre(S)（の記号表現）を計
算するアルゴリズム
3. 状態の記号表現の補集合，和，積を計算す
るアルゴリズム
4. 2つの記号表現が等しい集合がどうかを判
断するアルゴリズム
2006/9/28
モデル検査勉強会
9
4.1 状態集合の記号計算
• 例：オートマトンA
– 2変数 a, b:0..255
– <q, v, v’>
•q
: コントロール状態
• v, v’ : それぞれaとbの値に対応するバイト
• <*, *, *>
– <q2, 3, *>
» q = q2, v = 3, v’ = 任意
– QAは何万もの状態をもつ
2006/9/28
モデル検査勉強会
10
4.1 状態集合の記号計算
• 補集合
– <q2, 3, *>の補集合
• <q1, *, *> + <q2, [0;2], *> + <q2, [4;255], *> + <q3, *, *>
• Pre(S)
– Pre(<q1, [100;250], [8;109]>)
• <q1, [110;255], [8;109]>
2006/9/28
モデル検査勉強会
11
4.1 状態集合の記号計算
• 記号モデル検査の論理
– 状態論理式に基づく論理は記号モデル検査
に適している
• CTL
• mu-calculus
– PLTLはSat(ψi)の反復計算によって記述するこ
とができる
• 実際には用いられない
2006/9/28
モデル検査勉強会
12
4.1 状態集合の記号計算
• 無限システムに対する記号モデル検査の
抱える課題
– 集合操作が計算可能である記号表現を提案
するのが困難である
– Sat(φ)の反復計算の停止性を保証することが
できない
2006/9/28
モデル検査勉強会
13
4.2 二分決定グラフ (BDD)
• 二分決定グラフ
– Bryantが提案
– 能力
• 基本演算（論理積，補集合，比較，投影など）のコストが安価である
– 線形，2次，もしくは即時（equality testの場合）
– データ構造がとても簡潔である
– 単純
• データ構造とアルゴリズムが記述・実装ともに単純である
– 容易な適応
• BDDsは状態変数などを扱う問題に適している
– 一般性
• BDDsは特定のオートマトンに限定されず，いかなる種類の有限シ
ステムに対しても簡潔な表現が可能である
2006/9/28
モデル検査勉強会
14
4.2 二分決定グラフ (BDD)
2006/9/28
モデル検査勉強会
15
4.2 二分決定グラフ (BDD)
• 二分決定グラフ
– 長所
• 与えられたn個組みのタプルが満たすかどうか，n
回の検査で判断することができる
– 短所
• サイズが常に指数である
2006/9/28
モデル検査勉強会
16
4.2 二分決定グラフ (BDD)
• 二分決定グラフ
– 集約
• 規則
– 等価な部分木は同定し共有する
» Ex. n8とn10
– 余分な内部節点は削除する
» Ex. n7
• 利点
– 表現が小さくなるため，スペースが小さくなる
– 規範性(canonicity)
» 変数xiの順番が決定されれば，各集合Sに対する唯一の
BDDが存在する
2006/9/28
モデル検査勉強会
17
4.2 二分決定グラフ (BDD)
2006/9/28
モデル検査勉強会
18
4.2 二分決定グラフ (BDD)
• BDDsに対する操作
– 空検査
• 一つの葉Fに集約されている
– 比較
• 2つのBDDが同一である
– 補集合
• 全ての葉Tを葉Fと交換する
• 全ての葉Fを葉Tと交換する
– 論理積
• 各組(n1, n2)に対して，n1∩n2を計算する
2006/9/28
モデル検査勉強会
19
4.2 二分決定グラフ (BDD)
• BDDsに対する操作
– 論理和と他のブール演算
• 論理積と同様に行う
• 2次のコスト
– 投影と抽象化
• 投影 S[xi := T]
– i番の節点にTを割り当てる
• 抽象化 ∃xi.S
– Sのn個組みのタプルに対して，xiに適当な値biを挿入すること
によって，全てのn-1個組みのタプルを集める
• 最悪の場合，2次のコスト
2006/9/28
モデル検査勉強会
20
4.3 BDDsによるオートマトンの表現
• オートマトンA
– Q = {q0, …, q6}
• var digit:0..9
• var ready:bool
– 状態<q, k, b>
•
•
•
•
2006/9/28
q - 3ビット: b11, b12, b13
k - 4ビット: b21, b22, b23, b24
b - 1ビット: b31
<q3, 8, F>
モデル検査勉強会
21
4.3 BDDsによるオートマトンの表現
2006/9/28
モデル検査勉強会
22
4.3 BDDsによるオートマトンの表現
– 遷移
• <s, s’>
– 状態と遷移先の状態
• 最も単純な方法
– 状態をエンコードするのに必要な2倍のビットを割り当て
る
– <q3, 8, F> -> <q5, 0, F>
2006/9/28
モデル検査勉強会
23
4.3 BDDsによるオートマトンの表現
• (<q, k, b>, <q’, k’, b’>)
– q = q1, k ≠ 0, q’ = q2, k’ = k, b’ = T
2006/9/28
モデル検査勉強会
24
4.4 BDDに基づくモデル検査
•
Pre(S)の計算
– S
•
•
q = q1 ∧ k = 0
BS : SのBDD
– T
•
•
q = q0 ∧ q’ = q1 ∧ k’ = k
BT : TのBDD
1. BSのコピー（B’S）を作成する
•
bij = b’ij
2. BT∩B’Sを計算する
•
q = q0 ∧ q’ = q1 ∧ k’ = k ∧ q’ = q1 ∧ k’ = 0
3. 抽象化∃q’∃k’を適用する
•
2006/9/28
q = q0 ∧ k = 0
モデル検査勉強会
25
4.4 BDDに基づくモデル検査
• 二分決定グラフに基づいたモデル検査ツール
– SMV
• 能力はいくつかの要因に依存する
– BDD BTの作成
• Tは状態の組である
• BT1, …,BTmをそれぞれ作成するのが賢明である
– Pre(S) = Pre[T1](S)∪…∪Pre[Tm](S)
– ブール変数の順番の決定
• bij <=> b’ij
– bijがb’ijの近接でなければサイズが指数的に増加する
2006/9/28
モデル検査勉強会
26
4.4 BDDに基づくモデル検査
• 記号モデル検査に対する現在の取り組み
– より多くの検証問題を解決するためにBDD技
術を適用する
– BDDに基づくモデル検査固有の限界を伸ば
すような技術を開発する
2006/9/28
モデル検査勉強会
27

Download Report