模型檢測是一種用于自動(dòng)驗(yàn)證有限狀態(tài)并發(fā)系統(tǒng)的技術(shù)，與基于模擬、測試和演繹推理的傳統(tǒng)技術(shù)相比，具有許多方面的優(yōu)勢。本書共分18章，涵蓋的主要內(nèi)容包括模型檢測的基本知識(shí)、模態(tài)邏輯、符號(hào)化技術(shù)、SATSolver、限界模型檢測、自動(dòng)機(jī)上的模型檢測、抽象解釋、程序分析、實(shí)時(shí)系統(tǒng)驗(yàn)證，同時(shí)介紹NuSMV和UPPAAL兩個(gè)流行的模型檢測器。
Edmund M.Clarke教授，美國卡內(nèi)基 ? 梅隆大學(xué)計(jì)算機(jī)科學(xué)系教授，并且是ACM和IEEE會(huì)士。他在軟硬件驗(yàn)證、自動(dòng)定理證明、形式方法等方面享有崇高的國際聲譽(yù)，2007年獲得ACM圖靈獎(jiǎng)。
吳盡昭，廣西大學(xué)副校長，長期從事高效能高可信計(jì)算與推理理論與工具的研究和開發(fā)，研究領(lǐng)域涉及符號(hào)計(jì)算、自動(dòng)推理、形式化方法及其交叉、融合與應(yīng)用；在國內(nèi)外學(xué)術(shù)刊物和國際會(huì)議論文集上發(fā)表研究論文107篇，出版專著3部，獲得軟件著作權(quán)6項(xiàng)，申請專利3項(xiàng)；近年來承擔(dān)國家自然科學(xué)基金、863、973子課題等國家、省部級(jí)科研項(xiàng)目10余項(xiàng)。
目 錄
第1章 緒論 1
1.1 形式化方法的需求 1
1.2 硬件與軟件驗(yàn)證 1
1.3 模型檢測的流程 3
1.4 時(shí)序邏輯與模型檢測 3
1.5 符號(hào)算法 4
1.6 偏序約簡 6
1.7 緩解狀態(tài)爆炸問題的其他方法 7
第2章 系統(tǒng)建模 8
2.1 并發(fā)系統(tǒng)建模 8
2.2 并發(fā)系統(tǒng) 11
2.3 程序翻譯的實(shí)例 16
第3章 時(shí)序邏輯 18
3.1 計(jì)算樹邏輯CTL* 18
3.2 CTL和LTL邏輯 20
3.3 公正性 22
第4章 模型檢測 24
4.1 CTL模型檢測 24
4.2 基于tableau結(jié)構(gòu)的LTL模型檢測 29
4.3 CTL*模型檢測 33
第5章 二叉判定圖 36
5.1 布爾公式的表示方法 36
5.2 Kripke結(jié)構(gòu)的表示方法 40
第6章 符號(hào)模型檢測 42
6.1 不動(dòng)點(diǎn)表示 42
6.2 CTL符號(hào)模型檢測 45
6.3 符號(hào)模型檢測中的公正性 48
6.4 反例和診斷信息 50
6.5 一個(gè)ALU的例子 52
6.6 關(guān)系積的計(jì)算 54
6.7 符號(hào)化的LTL模型檢測 61
第7章 基于? 演算的模型檢測 68
7.1 簡介 68
7.2 命題? 演算 68
7.3 求不動(dòng)點(diǎn)公式的值 71
7.4 用OBDD表示? 演算公式 74
7.5 將CTL公式轉(zhuǎn)化為? 演算 75
7.6 復(fù)雜度問題 76
第8章 實(shí)踐中的模型檢測 77
8.1 SMV模型檢測器 77
8.2 一個(gè)實(shí)際的例子 80
第9章 模型檢測和自動(dòng)機(jī)理論 85
9.1 有限字與無限字上的自動(dòng)機(jī) 85
9.2 使用自動(dòng)機(jī)進(jìn)行模型檢測 86
9.3 檢查Büchi自動(dòng)機(jī)接受的語言是否為空 90
9.4 LTL公式轉(zhuǎn)化為自動(dòng)機(jī) 93
9.5 采用“On-the-Fly”技術(shù)的模型檢測 97
9.6 檢測語言包含的符號(hào)方法 98
第10章 偏序約簡 100
10.1 異步系統(tǒng)中的并發(fā) 101
10.2 獨(dú)立性與不可見性 102
10.3 LTL?X的偏序約簡 104
10.4 一個(gè)例子 107
10.5 計(jì)算充足集(ample)集合 109
10.6 算法的正確性 114
10.7 SPIN系統(tǒng)中的偏序約簡 117
第11章 結(jié)構(gòu)間的等價(jià)性和擬序 122
11.1 等價(jià)和擬序算法 128
11.2 構(gòu)建tableau結(jié)構(gòu) 129
第12章 組合推理 133
12.1 多個(gè)結(jié)構(gòu)的組合 134
12.2 判斷假設(shè)保證證明方法的正確性 136
12.3 CPU控制器的驗(yàn)證 136
第13章 抽象 139
13.1 影響錐化簡 139
13.2 數(shù)值抽象 141
第14章 對(duì)稱性 154
14.1 群和對(duì)稱性 154
14.2 商模型 156
14.3 對(duì)稱性和模型檢測 159
14.4 復(fù)雜度問題 160
14.5 實(shí)驗(yàn)結(jié)果 164
第15章 有限狀態(tài)系統(tǒng)的無限簇 166
15.1 無限簇上的時(shí)序邏輯 166
15.2 不變量 167
15.3 再次分析Futurebus+ 169
15.4 圖和網(wǎng)絡(luò)文法 171
15.5 令牌環(huán)簇的不確定性結(jié)果 179
第16章 離散實(shí)時(shí)系統(tǒng)和定量時(shí)序分析 183
16.1 實(shí)時(shí)系統(tǒng)和單調(diào)變化率調(diào)度 183
16.2 實(shí)時(shí)系統(tǒng)的模型檢測 184
16.3 RTCTL模型檢測 185
16.4 量化時(shí)序的分析：最小或最大延遲 185
16.5 飛行控制器 187
第17章 連續(xù)實(shí)時(shí)系統(tǒng) 192
17.1 時(shí)間約束自動(dòng)機(jī) 192
17.2 并行組合 194
17.3 使用時(shí)間約束自動(dòng)機(jī)進(jìn)行建模 195
17.4 時(shí)鐘域 198
17.5 時(shí)鐘區(qū) 203
17.6 邊界可區(qū)分矩陣 208
17.7 復(fù)雜度問題 211
第18章 結(jié)論 213
參考文獻(xiàn) 215
書單推薦
