模型檢測

模型檢測是一種用於自動驗證有限狀態併發系統的技術，與基於模擬、測試和演繹推理的傳統技術相比，具有許多方面的優勢。本書共分18章，涵蓋的主要內容包括模型檢測的基本知識、模態邏輯、符號化技術、SATSolver、限界模型檢測、自動機上的模型檢測、抽象解釋、程序分析、實時系統驗證，同時介紹NuSMV和UPPAAL兩個流行的模型檢測器。 ^[1] 

第1章 緒論 1

1.1 形式化方法的需求 1

1.2 硬件與軟件驗證 1

1.3 模型檢測的流程 3

1.4 時序邏輯與模型檢測 3

1.5 符號算法 4

1.6 偏序約簡 6

1.7 緩解狀態爆炸問題的其他方法 7

第2章 系統建模 8

2.1 併發系統建模 8

2.2 併發系統 11

2.3 程序翻譯的實例 16

第3章 時序邏輯 18

3.1 計算樹邏輯CTL* 18

3.2 CTL和LTL邏輯 20

3.3 公正性 22

第4章 模型檢測 24

4.1 CTL模型檢測 24

4.2 基於tableau結構的LTL模型檢測 29

4.3 CTL*模型檢測 33

第5章 二叉判定圖 36

5.1 布爾公式的表示方法 36

5.2 Kripke結構的表示方法 40

第6章 符號模型檢測 42

6.1 不動點表示 42

6.2 CTL符號模型檢測 45

6.3 符號模型檢測中的公正性 48

6.4 反例和診斷信息 50

6.5 一個ALU的例子 52

6.6 關係積的計算 54

6.7 符號化的LTL模型檢測 61 ^[1] 

第7章 基於? 演算的模型檢測 68

7.1 簡介 68

7.2 命題? 演算 68

7.3 求不動點公式的值 71

7.4 用OBDD表示? 演算公式 74

7.5 將CTL公式轉化為? 演算 75

7.6 複雜度問題 76

第8章 實踐中的模型檢測 77

8.1 SMV模型檢測器 77

8.2 一個實際的例子 80

第9章 模型檢測和自動機理論 85

9.1 有限字與無限字上的自動機 85

9.2 使用自動機進行模型檢測 86

9.3 檢查Büchi自動機接受的語言是否為空 90

9.4 LTL公式轉化為自動機 93

9.5 採用“On-the-Fly”技術的模型檢測 97

9.6 檢測語言包含的符號方法 98

第10章 偏序約簡 100

10.1 異步系統中的併發 101

10.2 獨立性與不可見性 102

10.3 LTL?X的偏序約簡 104

10.4 一個例子 107

10.5 計算充足集(ample)集合 109

10.6 算法的正確性 114

10.7 SPIN系統中的偏序約簡 117

第11章 結構間的等價性和擬序 122

11.1 等價和擬序算法 128

11.2 構建tableau結構 129

第12章 組合推理 133

12.1 多個結構的組合 134

12.2 判斷假設保證證明方法的正確性 136

12.3 CPU控制器的驗證 136 ^[1]