Document

SMVプログラム例3
MODULE main
VAR
request : boolean;
state : {ready, busy};
ASSIGN
init(state) := ready;
next(state) := case
state = ready & request : busy;
1 : {ready, busy};
esac;
SPEC
AG(request -> AF state = busy)
•上から条件を評価
•1は恒真
背景説明
モデル検査
モデル検査ツール
設計
状態機械
設計誤り
性質(仕様)
状態爆発問題 (p.106)

「モデル規模の増大にともない，探索すべき
状態数が急激に増大する」という問題
X
状態数10の構成要素10個からなるシステム
状態の総数 1010 = 100億
状態削減手法

Partial Order Reduction (例．SPIN)
 遷移の独立性を考慮して検証する性質
に無関係な状態を判断することで計算量
を削減する手法

記号モデル検査 (例．SMV, NuSMV)
 論理関数で状態集合や遷移関係を表し，
それらの操作によって検証を行う手法
構成
集合演算に基づく記号モデル検査 (4.2.2)
 論理関数に基づく表現 (4.2.3, 4.2.4)
 2分決定グラフに基づく記号モデル検査の実
現 (4.2.5, 4.2.6)

集合演算
論理関数
{001, 011, 100,
101, 111}
x1x2  x3
2分決定グラフ
4.2.2 集合演算に基づく記号モデル
検査
a.
b.
c.
d.

EF f ≡ E (true U f)
EG f ≡ AF(f)
AF f ≡ A (true U f)
AG f ≡ EF(f)
EX, EU, AX, AUのみ考える
4.2.2 集合演算に基づく記号モデル
検査
S: 全状態の集合
 Sf :CTL式fが成り立つ状態の集合

EF(q  EXq)

求めたいもの
 検証したい性質ｆについてSf
Sfが求まれば，初期状態集合ISfか
どうかを調べればよい


求め方
 部分式に対して再帰的に求める
q  EXq
q
EXq
q
q
4.2.2 集合演算に基づく記号モデル
検査
2.
3.
Sf = S – Sf
Sf g = Sf Sg, Sf  g = Sf  Sg
q
s1
p,q
p
s2
s3
q
s4
p
p
pq
pq
4.2.2 集合演算に基づく記号モデル
検査
4.
SEXf
SEXf
Sf
f
f
5.
SAXf
Sf
f
SAXf
f
4.2.2 集合演算に基づく記号モデル
検査
6.
T0 = Sg
SE(fUg)
Ti+1= Ti  (Sf  SEXTi )
f
T2
f
T1
f
いずれTi+1 = Tiとなる
f
T0
g
f
f
f
g
f
4.2.2 集合演算に基づく記号モデル
検査
7.
T0 = Sg
SA(fUg)
Ti+1= Ti  (Sf  SAXTi )
いずれTi+1 = Tiとなる
f
f
T2
f
T0
g
T1
f
g
f
例4.3
S EF(q  EXq) = {s1, s2}
T1, T2
EF(q  EXq)
T0
q
s1
p,q
p
s2
s3
q  EXq
q
s4
q
EXq
q
q  EXq
EF(q 
EXq)
EF(q 
EXq)
q
4.2.3 論理関数に基づく表現

状態集合，遷移関係を論理関数で表す
 2分決定グラフを用いて効率良く表現可能

状態の2進表現
q
x1x2
p,q
p
q
s1
s2
s3
s4
00
01
10
11
集合の表現
q
x1x2
p,q
p
q
s1
s2
s3
s4
00
01
10
11
例． Sq = {s1, s2, s4}
fq (x1,x2)= x1x2  x1x2  x1x2
Sqの特性関数 (characteristic function)
遷移関係の表現
q
x1x2
p,q
p
q
s1
s2
s3
s4
00
01
10
11
R = {(s1, s2), (s2, s3), (s2, s4), (s3, s3), (s3, s4), (s4, s4)}
= {(00,01), (01,10), (01,11), (10,10), (10,11), (11,11)}
N (x1,x2,x1’,x2’)= x1x2 x1x2’  …
4.2.4 論理関数に基づく記号モデル
検査
2.
3.
Sp = S – Sp
Sp q = Sp Sq
Sp  q = Sp  Sq
fp =fp
fp q =fp  fq
fpq =fp  fq
q
x1x2
p,q
p
q
s1
s2
s3
s4
00
01
10
11
例． Sq = {s1, s2, s4}, fq (x1,x2)= x1x2  x1x2  x1x2
fq (x1,x2) = fq (x1,x2) = x1x2
4.2.4 論理関数に基づく記号モデ
ル検査
4.
fEXq(x1,x2)=
Exist(N(x1,x2,x1’,x2’)fq(x1’,x2’), {x1’,x2’})
x1,x2,x1’,x2’
0 0 0 0
0 0 0 1
0 0 1 0
0 0 1 1
0 1 0 0
0 1 0 1
0 1 1 0
0 1 1 1
0
1
0
0
0
0
1
1
1
1
0
1
1
1
0
1
0
1
0
0
0
0
0
1
…
…
…
…
fq Nfq
…
N
1
1
q
s1
p,q
s2
p
s3
q
s4
EXq
EXq
EXq
EXq
4.2.4 論理関数に基づく記号モデ
ル検査
q
p,q
p
q
s1
4.
s3
s2
s3
s4
fEXp(x1,x2)=
Exist(N(x1,x2,x1’,x2’)fp(x1’,x2’), {x1’,x2’})
N
s1
s2
fp
s2
Nfp
Exist
s3
s4
s1
s2
s1
s2
s3
s4
s3
辺の始点となっている
頂点のみを取り出す
4.2.5 2分決定グラフ (BDD)
変数の順序がどのパスでも等しいBDDを考える
(Ordered BDD, OBDD)
縮約ルール
ルール1:ノードの除去
ルール2：部分グラフの共有
縮約された（Reduced）BDD
ROBDD

Download Report