Model Checking

Systems and Software
Verification
3. Model Checking
システム情報科学府情報工学専攻
荒木研究室修士2年住田辰雄
目次
• 3.1 モデル検査 CTL
• 3.2 モデル検査 PLTL
• 3.3 状態爆発問題
2006/9/14
モデル検査勉強会
2
3.1 モデル検査 CTL
• CTLのモデル検査アルゴリズム
– Queile, Sifakis, Clarke, Emerson and Sistlaらが提案
– 検証の分野においてとても重要な役割を果たす
• アルゴリズムが線形時間で走る
– オートマトン
– CTL式
• 状態式
• marking
– オートマトンに対して与えられたCTL式φがオートマトンの各状態qに
対してφのサブ論理式ψが満たされているか検査する
2006/9/14
モデル検査勉強会
3
3.1 モデル検査 CTL
• marking
– 原始命題，否定，論理積
• O(|Q|)
Procedure marking(phi)
case 1: phi = P
for all q in Q, if P in l(q) then do q.phi := true, else do q.phi := false.
case 2: phi = not psi
do marking(psi);
for all q in Q, do q.phi := not(q.psi).
case 3: phi = psi1 ∧ psi2
do marking(psi1); marking(psi2);
for all q in Q, do q.phi := and(q.psi1, q.psi2).
2006/9/14
モデル検査勉強会
4
3.1 モデル検査 CTL
• marking
– EX ψ
• O(|Q| + |T|) 以下
• AX ψ≡￢EX ￢ψ
case 4: phi = EX psi
do marking(psi);
for all q in Q, do q.phi := false;
/* initialisation */
for all (q, q’) in T, if q’.psi = true then do q.phi := true.
2006/9/14
モデル検査勉強会
5
3.1 モデル検査 CTL
• marking
– Eψ1Uψ2
• O(|Q| + |T|)
2006/9/14
case 5:phi = E psi1 U psi2
do marking(psi1); marking(psi2);
for all q in Q,
q.phi := false; q.seeenbefore := false; /* initialisation */
L := {};
for all q in Q, if q.psi2 = true then do L := L + { q };
while L nonempty {
draw q from L;
L := L – { q };
q.phi := true;
for all (q’, q) in T {
if q’.seenbefore = false then do {
q’ seenbefore := true;
if q’.psi1 = true then do L := L + { q’ };
}
}
}
モデル検査勉強会
6
3.1 モデル検査 CTL
• marking
– Aψ1Uψ2
• (a)
– qがψ2を満たす
• (b)
– qがψ1を満たす
– qから始まる遷移状態が一つ以上存在する
– qから始まる全ての遷移状態がAψ1Uψ２を満たす
2006/9/14
モデル検査勉強会
7
3.1 モデル検査 CTL
• marking
– Aψ1Uψ2
2006/9/14
case 6: phi = A psi1 U psi2
do marking(psi1); marking(psi2);
L := {}
for all q in Q, /* initialization */
q.nb := degree(q); /* the number of successors of q */
q.phi := false;
for all q in Q, if q.psi2 = true then do L := L + { q };
while L nonempty {
draw q from L;
L := L – { q };
q.phi := true;
for all (q’, q) in T {
q’.nb := q’nb – 1;
if (q’.nb = 0) and (q’psi1 = true) and (q’phi = false)
then do L := L + { q’ };
}
}
モデル検査勉強会
8
3.1 モデル検査 CTL
• CTLアルゴリズムの正しさ
– φ: Aψ1Uψ2について証明する
• 前提
– ψ1とψ2に対するmarkingは正しく行われている
• q.phiがmarkingによってtrueに設定されている
– q |= φ
• q.phiがmarkingによってfalseに設定されている
– q |≠ φ
» q |≠ ψ2 そのとき q |≠ ψ1
» q |= ψ1ならば(q, q’)∈T かつ q’ |≠φ
2006/9/14
モデル検査勉強会
9
3.1 モデル検査 CTL
• CTLアルゴリズムの複雑さ
– O(|A|×|φ|)
• O(|A|)
– O(|Q| + |T|)
• O(|φ|)
– CTL式φのサブ論理式の数
2006/9/14
モデル検査勉強会
10
3.2 モデル検査 PLTL
• Lichtenstein, Pnueli, Vardi and Wolperが提
案
• 経路論理式
2006/9/14
モデル検査勉強会
11
3.2 モデル検査 PLTL
• φ: GF P
– φを満たさない実行系列 :
– φを満たす実行系列 :
• ω-正規表現
 P  P  . P 
*
   P  .P 
*

– 正規表現
• + : 選択
• * : 任意の有限数の繰り返し
–ω
• 任意の無限数の繰り返し
2006/9/14
モデル検査勉強会
12
3.2 モデル検査 PLTL
• PLTLアルゴリズムの基本的な原理
– A |= φ
• Aの全ての実行系列はεφの形式で記述することができる
• A  B￢φが空である
– εφ
• φを満足するω-正規表現
– B￢φ
• φを満足しない全ての実行系列を認識するオートマトン
– ε￢φ
• サイズは最悪の場合でO(2^|φ|)
2006/9/14
モデル検査勉強会
13
3.2 モデル検査 PLTL
u1:
P, Q
u0: P, ￢Q
￢P, Q
￢P, ￢Q
P, Q
P, ￢Q
q0
q0
u2:
P, ￢Q
￢P, ￢Q
φ : G(P ⇒ XF Q)
2006/9/14
モデル検査勉強会
14
3.2 モデル検査 PLTL
￢P
￢Q
t1
t4
￢P
￢Q
P
Q
t5
t2
t3
￢P
￢Q
2006/9/14
モデル検査勉強会
15
3.2 モデル検査 PLTL
t1
 u0
￢P
￢Q
t2
t4
t4
t5
u
2006/9/14
￢P
￢Q
u
￢P
￢Q
u
1
t1
 u2
￢P
￢Q
P
Q
0
t3
0
 u0
u
0
t2
モデル検査勉強会
￢P
￢Q

t5
u
u
2
t3
2
￢P
￢Q
P
Q
u
2
16
3.2 モデル検査 PLTL
• PLTLアルゴリズムの複雑さ
– O(|A|×2^|φ|)
• サイズ：O(|A|×|B￢φ|)
• 時間：O(|A  B￢φ|)
• B￢φ
– 最悪でO(2^|φ|)
» PLTL式φのサブ論理式の数
2006/9/14
モデル検査勉強会
17
3.3 状態爆発問題
• モデル検査の最大の欠点
– 状態爆発問題
• オートマトンの作成
– marking (CTL)
– B￢φ
(PLTL)
• 状態は指数的に増加する
2006/9/14
モデル検査勉強会
18

Download Report