模型檢測

目 錄第1章 緒論1.1 形式化方法的需求1.2 硬件與軟件驗證1.3 模型檢測的過程1.4 時序邏輯與模型檢測1.5 符號算法1.6 偏序約簡1.7 緩解狀態(tài)爆炸問題的其他方法第2章 系統(tǒng)建模2.1 并發(fā)系統(tǒng)建模2.2 并發(fā)系統(tǒng)2.3 一個并發(fā)程序的Kripke模型第3章 時序邏輯3.1 計算樹邏輯CLT*3.2 CTL和LTL3.3 公正性第4章 模型檢測4.1 CTL模型檢測4.2 用tableau進(jìn)行LTL模型檢測4.3 CTL*模型檢測第5章 二叉判定圖5.1 布爾公式的表示方法5.2 Kripke結(jié)構(gòu)的表示方法第6章 符號模型檢測6.1 不動點(diǎn)表示6.2 CTL符號模型檢測6.3 符號模型檢測中的公正性6.4 反例和診斷信息6.5 一個ALU的例子6.6 關(guān)系積的計算6.7 符號化的LTL模型檢測第7章 基于μ-演算的模型檢測7.1 簡介7.2 命題μ-演算7.3 求不動點(diǎn)公式的值7.4 用OBDD表示μ-演算公式7.5 將CTL公式轉(zhuǎn)化為μ-演算7.6 復(fù)雜度問題第8章 實際中的模型檢測8.1 模型檢測器——SMV8.2 一個實際的例子第9章 模型檢測和自動機(jī)理論9.1 有限字與無限字上的自動機(jī)9.2 用自動機(jī)進(jìn)行模型檢測9.3 檢查Büchi自動機(jī)接受的語言是否為空9.4 LTL公式轉(zhuǎn)化為自動機(jī)9.5 “on-the-fly”模型檢測9.6 檢測語言包含的符號方法第10章 偏序約簡10.1 異步系統(tǒng)中的并發(fā)10.2 獨(dú)立性與不可見性10.3 LTL-X的偏序約簡10.4 一個例子10.5 計算Ample集合10.6 算法的正確性10.7 SPIN系統(tǒng)中的偏序約簡第11章 結(jié)構(gòu)間的等價性和擬序11.1 等價和擬序算法11.2 構(gòu)建tableau結(jié)構(gòu)第12章 組合推理12.1 結(jié)構(gòu)的組合12.2 假設(shè)保證方法的證明12.3 CPU控制器的驗證第13章 抽象13.1 影響錐化簡13.2 數(shù)值抽象第14章 對稱性14.1 群和對稱性14.2 商模型14.3 對稱性和模型檢測14.4 復(fù)雜性問題14.5 試驗結(jié)果第15章 有限狀態(tài)系統(tǒng)的無限簇15.1 無限簇上的時序邏輯15.2 不變量15.3 再次分析Futurebus+15.4 圖和網(wǎng)絡(luò)文法15.5 令牌環(huán)簇的不確定性結(jié)果第16章 離散實時系統(tǒng)和定量時序分析16.1 實時系統(tǒng)和單調(diào)變化率調(diào)度16.2 實時系統(tǒng)的模型檢測16.3 RTCTL模型檢測16.4 量化時序的分析： 最小或最大延遲16.5 飛行控制器第17章 連續(xù)實時系統(tǒng)17.1 時間約束自動機(jī)17.2 并行組合17.3 使用時間約束自動機(jī)進(jìn)行建模17.4 時鐘域17.5 時鐘區(qū)17.6 邊界可區(qū)分矩陣17.7 對復(fù)雜度的考慮第18章 結(jié)論參考文獻(xiàn)