6.2 時相的な振舞いの自動解析

6.2.1 時相論理

LTL: Linear Temporal Logic

P.137中～

(1)Xp : 次にp

(2)◇p : いつかp

(3)□p : 常にp

(4)p U q : qになるまでp

(5)p R q : ずっとqか、いつかp

P.138上～

シーケンスによるシステム表現とともに時相論理を利用できる

6.2.2 有界モデル検査

(1) 過小近似

自動でできるが網羅的ではない

(2) 簡単な例による説明

安全性の検査

常に「11でない」 → 成り立たないはず

P.140上～

P.140中～

P.140下～

P1: 値が11か？

P.140下～

3step ⇒ 反例見つかる

2step ⇒ 見つからない

[ex11-1] ◇Pと同じ意味となるものはどれですか

[ex11-2] □Pと同じ意味となるものはどれですか

[ex11-3] 初期状態S1で値a→状態S2で値b→状態S3で値a→状態S1に戻る、というシステムで成立しないものは

進行性の検査

いつかP2となるか？

P.141下～

経路が投げ縄型でなければ網羅できない

P.142中～

S2→S2

P.142中～

いつか11となるか？＝ずっと「0か0」か？

P.142下～

3stepで、閉じている方の経路の検査

⇒ 成立

P.143上～

投げ縄型でなければ探索範囲依存

6.2.3～

省略

[ex11-4] 初期S1でa → S2でb → S3でa → S1、というシステムで反例が見つかるのはどれですか

[ex11-5] 初期S1でa → S2でb → S3でa → S1、というシステムで網羅的に検査できないのはどれですか

教科書（図はすべてこちらより引用）：
　中島震，「形式手法入門―ロジックによるソフトウェア設計―」，オーム社