模型檢測（第二版）

目 錄
第1章 第二版概述 1
第2章 第一版概述 2
2.1 形式化方法的需求 2
2.2 硬件與軟件驗證 2
2.3 模型檢測的流程 4
2.4 時序邏輯與模型檢測 4
2.5 符號算法 5
2.6 偏序約簡 7
2.7 緩解狀態空間爆炸問題的其他方法 7
第3章 系統建模 9
3.1 變遷系統和Kripke結構 10
3.2 非確定性和輸入 11
3.3 一階邏輯和符號表示法 11
3.4 布爾編碼 14
3.5 數字電路建模 15
3.5.1 狀態保持單元 15
3.5.2 同步電路 15
3.5.3 異步電路 16
3.6 程序建模 17
3.6.1 順序進程 17
3.6.2 並發進程建模 19
3.7 公平性 23
本章文獻註釋 24
習題 24
第4章 時序邏輯 25
4.1 時序邏輯CTL* 25
4.2 CTL*的語法和語義 27
4.2.1 CTL*的語法 27
4.2.2 CTL*的語義 27
4.2.3 負範式(NNF) 29
4.3 基於CTL*的時序邏輯 29
4.3.1 分支時間邏輯CTL 30
4.3.2 全稱計算樹邏輯ACTL*和ACTL 31
4.3.3 線性時序邏輯LTL 32
4.3.4 各種CTL*子邏輯的關系 32
4.4 命題邏輯的集合型原子命題和集合語義 33
4.5 公正性 33
4.6 反例 34
4.7 安全性和活性 35
本章文獻註釋 36
習題 36
第5章 CTL模型檢測 38
5.1 顯式狀態表示法的CTL模型檢測 38
5.2 基於公正性約束的CTL模型檢測 42
5.3 基於固定點計算的CTL模型檢測 43
5.3.1 固定點理論 43
5.3.2 基於固定點的可達性分析 46
5.3.3 基於固定點的CTL模型檢測算法 47
5.3.4 基於固定點的公正性 49
5.3.5 有限路徑上的固定點特征 51
本章文獻註釋 51
習題 51
第6章 LTL和CTL*模型檢測 52
6.1 構建語義表 52
6.2 基於語義表的LTL模型檢測 55
6.3 構造語義表方法的正確性證明 56
6.4 CTL*模型檢測 60
本章文獻註釋 62
習題 62
第7章 無限字上的自動機和LTL模型檢測 63
7.1 有限字上的有限自動機 63
7.1.1 確定性和補自動機 64
7.2 無限字上的有限自動機 64
7.3 確定性和非確定性Büchi自動機 65
7.4 Büchi自動機的交自動機 66
7.5 空自動機檢測 67
7.5.1 基於雙DFS算法的空自動機檢測 68
7.5.2 雙DFS算法的正確性 69
7.6 廣義Büchi自動機 70
7.7 自動機和Kripke結構 71
7.8 基於自動機的模型檢測 72
7.9 LTL公式轉化為自動機 73
7.10 LTL到自動機的高效轉換 75
7.10.1 算法概述 75
7.10.2 數據結構 76
7.10.3 算法細節 77
7.11 采用即時技術的模型檢測 80
本章文獻註釋 81
習題 82
第8章 二叉決策圖和符號模型檢測 83
8.1 布爾公式的表示 83
8.2 Kripke結構的OBDD 87
8.3 CTL符號模型檢測 88
8.3.1 量化布爾公式 89
8.3.2 符號模型檢測算法 90
8.4 符號模型檢測中的公正性 91
8.5 反例和佐證 91
8.6 關系積的計算 94
8.6.1 分割的變遷關系 95
8.6.2 合並劃分 99
本章文獻註釋 99
習題 100
第9章 命題滿足性 101
9.1 合取範式 101
9.2 命題邏輯譯為CNF的方法 102
9.3 基於二分搜索的命題滿足性 103
9.3.1 遞歸的二分搜索 103
9.3.2 基於跡的二分搜索 105
9.4 布爾約束傳播(BCP) 106
9.5 沖突驅動的子句學習 107
9.5.1 蘊含圖 107
9.5.2 子句學習 108
9.5.3 基於CDCL的歸結證明生成方法 109
9.6 啟發式決策 109
本章文獻註釋 110
習題 111
第10章 基於滿足性的模型檢測 113
10.1 有界模型檢測 113
10.1.1 有界模型檢測總覽 113
10.1.2 可達性 114
10.1.3 最終性 116
10.1.4 LTL的有界模型檢測 117
10.1.5 完備性閾值 118
10.2 基於k歸納的可達性驗證 119
10.2.1 基於命題SAT的歸納 119
10.2.2 泛化的k歸納 120
10.2.3 完備性 121
10.3 基於歸納不變式的模型檢測 121
10.4 基於克雷格插值的模型檢測 122
10.4.1 克雷格插值 122
10.4.2 面向歸結證明的克雷格插值 123
10.4.3 基於克雷格插值的可達性檢測 124
10.4.4 正確性 126
10.5 性質導向的可達性分析 126
10.5.1 概述 126
10.5.2 算法的主循環 127
10.5.3 extendFrontier算法 128
10.5.4 正確性 129
本章文獻註釋 129
習題 130
第11章 結構間的等價性和預序 131
11.1 互模擬等價 131
11.2 公正的互模擬等價 135
11.3 模型間的預序關系 135
11.4 互模擬和模擬關系的博弈 138
11.5 等價和預序算法 138
本章文獻註釋 139
習題 140
第12章 偏序約簡 141
12.1 異步系統中的並發 142
12.2 無關性與隱匿性 143
12.3 LTL?X的偏序約簡 145
12.4 實例分析 148
12.5 充足集的計算 150
12.5.1 條件檢測方法的復雜度 150
12.5.2 計算充足集的啟發式策略 151
12.6 算法的正確性 154
12.7 SPIN系統中的偏序約簡 157
本章文獻註釋 161
第13章 抽象 162
13.1 存在性抽象 162
13.1.1 局部約簡 165
13.1.2 數據抽象 166
13.1.3 謂詞抽象 167
13.2 抽象模型的計算方法 168
13.2.1 軟件程序的抽象 168
13.2.2 基於局部約簡的同步電路抽象 170
13.3 反例引導抽象精化(CEGAR) 172
13.3.1 假反例 172
13.3.2 面向ACTL*的抽象精化框架 173
13.3.3 識別假反例 173
13.3.4 抽象模型的精化 176
本章文獻註釋 178
第14章 軟件的模型檢測 180
14.1 程序的控制流圖表示方法 180
14.2 基於符號執行的斷言檢測方法 181
14.3 基於謂詞抽象的程序驗證 182
14.3.1 布爾程序 183
14.3.2 將普通程序惰性抽象到布爾程序的方法 184
14.4 完整實例 186
14.4.1 程序 186
14.4.2 性質規約 187
14.4.3 抽象程序 189
本章文獻註釋 191
第15章 基於自動學習的驗證 192
15.1 Angluin的L*算法 192
15.1.1 實例分析 194
15.2 組合推理 195
15.3 面向通信組件的假設-保證型推理 196
15.3.1 系統模型 197
15.3.2 性質與滿足性 198
15.3.3 LTS中假設-保證型範式的實現 199
15.3.4 基於學習的假設-保證機制 199
15.3.5 面向假設-保證規則的學習算法實例 201
15.4 黑盒檢測 203
15.4.1 執行模型 203
15.4.2 簡單解決方案 204
15.4.3 基於學習的算法 205
15.4.4 Vasilevskii-Chow算法 205
本章文獻註釋 206
第16章 面向μ演算的模型檢測 208
16.1 概述 208
16.2 命題μ演算 208
16.3 求固定點公式的值 211
16.4 采用OBDD表示μ演算公式 214
16.5 將CTL公式轉換到μ演算 216
本章文獻註釋 216
第17章 對稱性 218
17.1 群和對稱性 218
17.2 商模型 220
17.3 基於對稱性的模型檢測 222
17.4 復雜度問題 224
17.4.1 軌道問題和圖同構 224
17.4.2 軌道關系和OBDD 226
17.5 實驗結果 228
本章文獻註釋 229
第18章 有限狀態系統的無限族 230
18.1 無限族上的時序邏輯 230
18.2 不變式 231
18.3 再次思考Futurebus+ 233
18.4 圖和網絡文法 235
18.5 令牌環族的不確定性結果 242
本章文獻註釋 244
第19章 離散實時系統和定量時序分析 246
19.1 實時系統和單調變化率調度 246
19.2 實時系統的模型檢測 247
19.3 RTCTL模型檢測 247
19.4 量化時序的分析：最小或最大延遲 248
19.4.1 最小延遲算法 248
19.4.2 最大延遲算法 249
19.5 實例：飛行控制器 250
19.5.1 系統描述 250
19.5.2 飛行控制系統的模型 252
19.5.3 驗證結果 252
本章文獻註釋 254
第20章 連續實時系統 255
20.1 定時自動機 255
20.2 並行組合 257
20.3 使用定時自動機建模 258
20.4 時鐘域 260
20.5 時鐘區 265
20.6 邊界可區分矩陣 270
20.7 復雜度問題 274
本章文獻註釋 274
原著參考文獻 275