目 錄
第1章 緒論\t1
1．1 形式化方法的需求\t1
1．2 硬件與軟件驗證\t1
1．3 模型檢測的流程\t3
1．4 時序邏輯與模型檢測\t3
1．5 符號算法\t4
1．6 偏序約簡\t6
1．7 緩解狀態(tài)爆炸問題的其他方法\t7
第2章 系統(tǒng)建模\t8
2．1 并發(fā)系統(tǒng)建模\t8
2．2 并發(fā)系統(tǒng)\t11
2．3 程序翻譯的實例\t16
第3章 時序邏輯\t18
3．1 計算樹邏輯CTL*\t18
3．2 CTL和LTL邏輯\t20
3．3 公正性\t22
第4章 模型檢測\t24
4．1 CTL模型檢測\t24
4．2 基于tableau結(jié)構(gòu)的LTL模型檢測\t29
4．3 CTL*模型檢測\t33
第5章 二叉判定圖\t36
5．1 布爾公式的表示方法\t36
5．2 Kripke結(jié)構(gòu)的表示方法\t40
第6章 符號模型檢測\t42
6．1 不動點表示\t42
6．2 CTL符號模型檢測\t45
6．3 符號模型檢測中的公正性\t48
6．4 反例和診斷信息\t50
6．5 一個ALU的例子\t52
6．6 關(guān)系積的計算\t54
6．7 符號化的LTL模型檢測\t61
第7章 基于? 演算的模型檢測\t68
7．1 簡介\t68
7．2 命題? 演算\t68
7．3 求不動點公式的值\t71
7．4 用OBDD表示? 演算公式\t74
7．5 將CTL公式轉(zhuǎn)化為? 演算\t75
7．6 復(fù)雜度問題\t76
第8章 實踐中的模型檢測\t77
8．1 SMV模型檢測器\t77
8．2 一個實際的例子\t80
第9章 模型檢測和自動機理論\t85
9．1 有限字與無限字上的自動機\t85
9．2 使用自動機進行模型檢測\t86
9．3 檢查Büchi自動機接受的語言是否為空\t90
9．4 LTL公式轉(zhuǎn)化為自動機\t93
9．5 采用“On-the-Fly”技術(shù)的模型檢測\t97
9．6 檢測語言包含的符號方法\t98
第10章 偏序約簡\t100
10．1 異步系統(tǒng)中的并發(fā)\t101
10．2 獨立性與不可見性\t102
10．3 LTL?X的偏序約簡\t104
10．4 一個例子\t107
10．5 計算充足集(ample)集合\t109
10．6 算法的正確性\t114
10．7 SPIN系統(tǒng)中的偏序約簡\t117
第11章 結(jié)構(gòu)間的等價性和擬序\t122
11．1 等價和擬序算法\t128
11．2 構(gòu)建tableau結(jié)構(gòu)\t129
第12章 組合推理\t133
12．1 多個結(jié)構(gòu)的組合\t134
12．2 判斷假設(shè)保證證明方法的正確性\t136
12．3 CPU控制器的驗證\t136
第13章 抽象\t139
13．1 影響錐化簡\t139
13．2 數(shù)值抽象\t141
第14章 對稱性\t154
14．1 群和對稱性\t154
14．2 商模型\t156
14．3 對稱性和模型檢測\t159
14．4 復(fù)雜度問題\t160
14．5 實驗結(jié)果\t164
第15章 有限狀態(tài)系統(tǒng)的無限簇\t166
15．1 無限簇上的時序邏輯\t166
15．2 不變量\t167
15．3 再次分析Futurebus+\t169
15．4 圖和網(wǎng)絡(luò)文法\t171
15．5 令牌環(huán)簇的不確定性結(jié)果\t179
第16章 離散實時系統(tǒng)和定量時序分析\t183
16．1 實時系統(tǒng)和單調(diào)變化率調(diào)度\t183
16．2 實時系統(tǒng)的模型檢測\t184
16．3 RTCTL模型檢測\t185
16．4 量化時序的分析：最小或最大延遲\t185
16．5 飛行控制器\t187
第17章 連續(xù)實時系統(tǒng)\t192
17．1 時間約束自動機\t192
17．2 并行組合\t194
17．3 使用時間約束自動機進行建模\t195
17．4 時鐘域\t198
17．5 時鐘區(qū)\t203
17．6 邊界可區(qū)分矩陣\t208
17．7 復(fù)雜度問題\t211
第18章 結(jié)論\t213
參考文獻\t215