Document

4 形式的設計検証技術

検証 verification
 求められる機能や性質を，設計が満たしている
かどうかを調べること


求められる機能や性質＝仕様 Specification
形式的検証 (4.1.2)
 設計や仕様を形式的に(≒数学的に)記述し，形
式的に検証を行う
 すべての可能な動作を考慮

比較．シミュレーション (4.1.1)
4.1.2 形式的検証

モデル検査 Model Checking
 状態探索による検証
 仕様は時相論理(temporal
4.3 CTLモデル検査
 4.4 LTLモデル検査


logic)で記述
CTL
定理証明 Theorem Proving (4.4)
LTL
例．図4.2
ia
FF1
00
10
01
oa
11
例．図4.2
ia
ib
FF1
FF2
oa
ob
00 00 01 00 10 00 11 00
00 01 01 01 10 01 11 01
00 11 01 11 10 11 11 11
00 10 01 10 10 10 11 10
モデル検査，モデル検査ツール

CTLモデル検査 (4.2)
 SMV,


NuSMV
1998 ACM Paris Kanellakis Theory and Practice
Award
LTLモデル検査 (4.3)
 SPIN,
LTSA, NuSMV
2001 ACM Software System Award
 2005 ACM Paris Kanellakis Theory and Practice
Award

4.2 CTLモデル検査

ia
ib
SMVでの記述例
FF1
FF2
oa
ob
MODULE main
VAR
ia : boolean;
ib : boolean;
oa : boolean;
ob : boolean;
ASSIGN
init(ia) := 0;
init(ib) := 0;
init(oa) := 0;
init(ob) := 0;
next(oa) := ia;
next(ob) := !ia & ib;
next(ia) := {0, 1};
next(ib) := {0, 1};
SPEC
AG !(oa & ob)
SMVの特徴

ＣＴＬ (4.2.1)

記号モデル検査 (4.2.2~4.2.6)

論理関数で記号的に状態探索を実行


グラフ構造を明示的に取り扱わない
2分決定グラフ (BDD) (4.2.5)

論理関数処理に適したデータ構造
状態グラフ (クリプキ構造)
q
s1

s3
s4
S = {s1, s2, s3, s4}
I = {s1}
遷移関係: R SS (注．必ず次状態が存在するものとする)


s2
q
初期状態集合: I S


p
状態集合: S


p,q
R = {(s1, s2), (s2, s3), (s2, s4), (s3, s3), (s3, s4), (s4, s4)}
原子命題の割当: L: S ↦ 2A

原子命題の集合 A = {p, q}
4.2.1 CTL
シンタックス (f,g はCTL式)
 原子命題 atomic proposition




例．変数ib = 1
f, f  g , f  g , f  g
EXf, EFf, EGf, E(f Ug)
AXf, AFf, AGf, A(fUg)
E: あるパスで
A: すべてのパスで
F: いずれ
G: ずっと
U: ～まで
計算木とパス
q
s1
計算木
s3
p,q
p
s2
s3
s2
パス
s3
s4
s3
s4
s4
s4
s4
s4
q
s4
E: あるパスで
A: すべてのパスで
F: いずれ
G: ずっと
U: ～まで
SMVがすること
すべての初期状態において，
 CTL式fが成り立つかどうかを調べる
MODULE main
s  I, s ⊨ f
VAR

s : {s1, s2, s3, s4};
DEFINE
p := s = s2 | s = s3;
q := s = s1 | s = s2 | s = s4;
ASSIGN
init(s) := s1;
q
s1
p,q
s2
p
s3
q
s4
next(s) := case
s =
s =
s =
s =
esac;
s1
s2
s3
s4
:
:
:
:
s2;
{s3, s4};
{s3, s4};
s4;
セマンティクス EX, AX

EXf


計算木
fがある次状態で成り立つ
f
AXf

fがすべての次状態で成り立つ
計算木
f
f
例
q
p,q
p
s1
s2
s3
EXp
EXp
q
s4
EXp
AXp
EXq, AXqは？
セマンティクス EF, AF

EFf


fがあるパスでいずれ成り立つ
AFf

fがすべてのパスでいずれ成り立つ
f
f
f
f
例
q
p,q
p
s2
s3
EFp
EFp
EFp
AFp
AFp
AFp
s1
q
s4
EFq, AFqは？
セマンティクス EG, AG

EGf


fがあるパスで常に成り立つ
AGf

fがすべてのパスで常に成り立つ
f
f
f
f
例
q
s1
p,q
p
s2
s3
EGp
q
s4
EGp
EGq, AGqは？
セマンティクス EU, AU

E(f Ug)


あるパスについて，どこかでgが成り立ち，それ
までfが成り立ち続けている
A(f Ug)

すべてのパスについて，．．．
f
f
f
f
g
g
g
f
g
例
q
s1
E(pUq)
p,q
p
s2
s3
E(pUq)
A(pUq)
E(pUq)
q
s4
E(pUq)
A(pUq)
例 (p.110)
EF ( q  EX(q))が成り立つのは？
q
s1
p,q
p
s2
s3
q
EX(q) EX(q)
q  EX(q)
EF(q 
EX(q))
EF(q 
EX(q))
q
s4
簡易アービタ

AG(oa  ob)
 常に，oaとobが同時に1にならない

AG(ib  AF(ib  ob))
 どの状態でも，ibが1ならば，いずれ必ず，ibが0
になるか，obが1になる
ia
ib
FF1
FF2
oa
ob
SMVプログラム例1： 3ビットカウンタ
MODULE main
VAR
bit0 : counter_cell(1);
bit1 : counter_cell(bit0.carry_out);
bit2 : counter_cell(bit1.carry_out);
SPEC
AG AF bit2.carry_out
SPEC
!EF bit2.carry_out
MODULE counter_cell(carry_in)
VAR
value : boolean;
ASSIGN
init(value) := 0;
next(value) := value + carry_in mod 2;
DEFINE
carry_out := value & carry_in;
SMVプログラム
例2：非同期システム
1つが非決定的に
選ばれて実行
MODULE main
VAR
gate1: process inverter(gate3.output);
gate2: process inverter(gate1.output);
gate3: process inverter(gate2.output);
SPEC
(AG AF gate1.output) & (AG AF !gate1.output)
MODULE inverter(input)
VAR
output: boolean;
ASSIGN
init(output) := 0;
next(output) := !input;
FAIRNESS
running
どのプロセスも無限に多
くの回数選ばれる

Download Report