●第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.2CTL和LTL邏輯20
3.3公正性22
第4章模型檢測24
4.1CTL模型檢測24
4.2基於tableau結構的LTL模型檢測29
4.3CTL*模型檢測33
第5章二叉判定圖36
5.1布爾公式的表示方法36
5.2Kripke結構的表示方法40
第6章符號模型檢測42
6.1不動點表示42
6.2CTL符號模型檢測45
6.3符號模型檢測中的公正性48
6.4反例和診斷信息50
6.5一個ALU的例子52
6.6關繫積的計算54
6.7符號化的LTL模型檢測61
第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.1SMV模型檢測器77
8.2一個實際的例子80
第9章模型檢測和自動機理論85
9.1有限字與無限字上的自動機85
9.2使用自動機進行模型檢測86
9.3檢查Büchi自動機接受的語言是否為空90
9.4LTL公式轉化為自動機93
9.5采用“On-the-Fly”技術的模型檢測97
9.6檢測語言包含的符號方法98
第10章偏序約簡100
10.1異步繫統中的並發101
10.2獨立性與不可見性102
10.3LTL?X的偏序約簡104
10.4一個例子107
10.5計算充足集(ample)集合109
10.6算法的正確性114
10.7SPIN繫統中的偏序約簡117
第11章結構間的等價性和擬序122
11.1等價和擬序算法128
11.2構建tableau結構129
第12章組合推理133
12.1多個結構的組合134
12.2判斷假設保證證明方法的正確性136
12.3CPU控制器的驗證136
第13章抽像139
13.1影響錐化簡139
13.2數值抽像141
第14章對稱性154
14.1群和對稱性154
14.2商模型156
14.3對稱性和模型檢測159
14.4復雜度問題160
14.5實驗結果164
第15章有限狀態繫統的無限簇166
15.1無限簇上的時序邏輯166
15.2不變量167
15.3再次分析Futurebus+169
15.4圖和網絡文法171
15.5令牌環簇的不確定性結果179
第16章離散實時繫統和定量時序分析183
16.1實時繫統和單調變化率調度183
16.2實時繫統的模型檢測184
16.3RTCTL模型檢測185
16.4量化時序的分析：最小或優選延遲185
16.5飛行控制器187
第17章連續實時繫統192
17.1時間約束自動機192
17.2並行組合194
17.3使用時間約束自動機進行建模195
17.4時鐘域198
17.5時鐘區203
17.6邊界可區分矩陣208
17.7復雜度問題211
第18章結論213
參考文獻215

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

(美)埃德蒙·M.克拉克(Edmund M.Clarke,Jr.) 等 著 吳盡昭 等 譯