目 錄 第1章 緒論 1 1.1 形式化方法的需求 1 1.2 硬件與軟件驗證 1 1.3 模型檢測的流程 3 1.4 時序邏輯與模型檢測 3 1.5 符號算法 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 程序翻譯的實例 16 第3章 時序邏輯 18 3.1 計算樹邏輯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章 符號模型檢測 42 6.1 不動點表示 42 6.2 CTL符號模型檢測 45 6.3 符號模型檢測中的公正性 48 6.4 反例和診斷信息 50 6.5 一個ALU的例子 52 6.6 關(guān)系積的計算 54 6.7 符號化的LTL模型檢測 61 第7章 基于? 演算的模型檢測 68 7.1 簡介 68 7.2 命題? 演算 68 7.3 求不動點公式的值 71 7.4 用OBDD表示? 演算公式 74 7.5 將CTL公式轉(zhuǎn)化為? 演算 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公式轉(zhuǎn)化為自動機 93 9.5 采用“On-the-Fly”技術(shù)的模型檢測 97 9.6 檢測語言包含的符號方法 98 第10章 偏序約簡 100 10.1 異步系統(tǒng)中的并發(fā) 101 10.2 獨立性與不可見性 102 10.3 LTL?X的偏序約簡 104 10.4 一個例子 107 10.5 計算充足集(ample)集合 109 10.6 算法的正確性 114 10.7 SPIN系統(tǒng)中的偏序約簡 117 第11章 結(jié)構(gòu)間的等價性和擬序 122 11.1 等價和擬序算法 128 11.2 構(gòu)建tableau結(jié)構(gòu) 129 第12章 組合推理 133 12.1 多個結(jié)構(gòu)的組合 134 12.2 判斷假設保證證明方法的正確性 136 12.3 CPU控制器的驗證 136 第13章 抽象 139 13.1 影響錐化簡 139 13.2 數(shù)值抽象 141 第14章 對稱性 154 14.1 群和對稱性 154 14.2 商模型 156 14.3 對稱性和模型檢測 159 14.4 復雜度問題 160 14.5 實驗結(jié)果 164 第15章 有限狀態(tài)系統(tǒng)的無限簇 166 15.1 無限簇上的時序邏輯 166 15.2 不變量 167 15.3 再次分析Futurebus+ 169 15.4 圖和網(wǎng)絡文法 171 15.5 令牌環(huán)簇的不確定性結(jié)果 179 第16章 離散實時系統(tǒng)和定量時序分析 183 16.1 實時系統(tǒng)和單調(diào)變化率調(diào)度 183 16.2 實時系統(tǒng)的模型檢測 184 16.3 RTCTL模型檢測 185 16.4 量化時序的分析：最小或最大延遲 185 16.5 飛行控制器 187 第17章 連續(xù)實時系統(tǒng) 192 17.1 時間約束自動機 192 17.2 并行組合 194 17.3 使用時間約束自動機進行建模 195 17.4 時鐘域 198 17.5 時鐘區(qū) 203 17.6 邊界可區(qū)分矩陣 208 17.7 復雜度問題 211 第18章 結(jié)論 213 參考文獻 215