4 形式的設計検証技術 検証 verification 形式的検証 (4.1.2) 求められる機能や性質を，設計が満たしているかどうかを調べること 求められる機能や性質　＝　仕様 Specification 形式的検証 (4.1.2) 設計や仕様を形式的に(≒数学的に)記述し，形式的に検証を行う すべての可能な動作を考慮 比較．シミュレーション (4.1.1)

4.1.2 形式的検証 モデル検査 Model Checking 定理証明 Theorem Proving (4.4) 状態探索による検証 仕様は時相論理(temporal logic)で記述 4.3 CTLモデル検査 4.4 LTLモデル検査 定理証明 Theorem Proving (4.4) CTL LTL

例．図4.2 ia FF1 oa 0 0 1 0 0 1 1 1

例．図4.2 ia FF1 oa ob FF2 ib 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) LTLモデル検査 (4.3) 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モデル検査 SMVでの記述例 ia FF1 oa ob ib FF2 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) ia FF1 oa ob FF2 ib

SMVの特徴 ＣＴＬ (4.2.1) 記号モデル検査 (4.2.2~4.2.6) 論理関数で記号的に状態探索を実行 ＣＴＬ　(4.2.1) 記号モデル検査 (4.2.2~4.2.6) 論理関数で記号的に状態探索を実行 グラフ構造を明示的に取り扱わない 2分決定グラフ (BDD) (4.2.5) 論理関数処理に適したデータ構造

状態グラフ (クリプキ構造) q p,q p q s1 s2 s3 s4 状態集合: S 初期状態集合: I S 遷移関係: R SS (注．必ず次状態が存在するものとする) 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: ～まで

計算木とパス パス 計算木 E: あるパスで A: すべてのパスで F: いずれ G: ずっと U: ～まで q p,q p q s1 s2

SMVがすること すべての初期状態において， CTL式fが成り立つかどうかを調べる s  I, s ⊨ f s1 s2 s3 s4 q MODULE main VAR s : {s1, s2, s3, s4}; DEFINE p := s = s2 | s = s3; q := s = s1 | s = s2 | s = s4; ASSIGN init(s) := s1; next(s) := case s = s1 : s2; s = s2 : {s3, s4}; s = s3 : {s3, s4}; s = s4 : s4; esac; s1 s2 s3 s4 q p,q p

セマンティクス EX, AX 計算木 EXf fがある次状態で成り立つ AXf fがすべての次状態で成り立つ f 計算木 f f

例 q p,q p q s1 s2 s3 s4 EXp EXp EXp AXp EXq, AXqは？

セマンティクス EF, AF EFf fがあるパスでいずれ成り立つ AFf fがすべてのパスでいずれ成り立つ f f

例 q p,q p q s1 s2 s3 s4 EFp EFp EFp AFp AFp AFp EFq, AFqは？

セマンティクス EG, AG EGf fがあるパスで常に成り立つ AGf fがすべてのパスで常に成り立つ f f f f

例 q p,q p q s1 s2 s3 s4 EGp EGp EGq, AGqは？

セマンティクス EU, AU E(f Ug) A(f Ug) あるパスについて，どこかでgが成り立ち，それまでfが成り立ち続けている すべてのパスについて，．．． f f f g f g f g g

例 q p,q p q s1 s2 s3 s4 E(pUq) E(pUq) E(pUq) E(pUq) A(pUq) A(pUq)

例 (p.110) EF ( q  EX(q))が成り立つのは？ EX(q) EX(q) q  EX(q) p,q p q s1 s2 s3 s4 q EX(q) EX(q) q  EX(q) EF(q  EX(q)) EF(q  EX(q))

簡易アービタ AG(oa  ob) AG(ib  AF(ib  ob)) 常に，oaとobが同時に1にならない どの状態でも，ibが1ならば，いずれ必ず，ibが0になるか，obが1になる ia FF1 oa ob FF2 ib

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 !EF bit2.carry_out MODULE counter_cell(carry_in) 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) output: boolean; ASSIGN init(output) := 0; next(output) := !input; FAIRNESS running どのプロセスも無限に多くの回数選ばれる