模型檢測

定　價：￥69.00

作　者：	（美）Edmund M. Clarke Jr.（E. M. 克拉克）Orna Grumberg（O. 格倫貝格）Doron A. Peled（D. A. 佩萊德）
出版社：	電子工業(yè)出版社
叢編項：
標　簽：	工業(yè)技術(shù) 金屬學與金屬工藝

購買這本書可以去

ISBN：	9787121272950	出版時間：	2016-02-01	包裝：	平塑
開本：		頁數(shù)：	236	字數(shù)：

內(nèi)容簡介

　　模型檢測是一種用于自動驗證有限狀態(tài)并發(fā)系統(tǒng)的技術(shù)，與基于模擬、測試和演繹推理的傳統(tǒng)技術(shù)相比，具有許多方面的優(yōu)勢。本書涵蓋的內(nèi)容包括模型檢測的基本知識、模態(tài)邏輯、符號化技術(shù)、SAT Solver、限界模型檢測、自動機上的模型檢測、抽象解釋、程序分析、實時系統(tǒng)驗證，同時介紹NuSMV和UPPAAL兩個流行的模型檢測器。

作者簡介

　　李剛，華北電力大學（保定）計算機系講師，目前從事軟件工程、建模與仿真、智能電網(wǎng)的信息化管理等方面的研究工作，主要內(nèi)容是將計算機科學與技術(shù)的理論方法應用到電力系統(tǒng)的問題中，在智電網(wǎng)的故障診斷與預測方面，獲得實用新型專利授權(quán)2項、計算機軟件著作權(quán)1項。

圖書目錄

目錄第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進行LTL模型檢測4.3 CTL*模型檢測第5章二叉判定圖5.1 布爾公式的表示方法5.2 Kripke結(jié)構(gòu)的表示方法第6章符號模型檢測6.1 不動點表示6.2 CTL符號模型檢測6.3 符號模型檢測中的公正性6.4 反例和診斷信息6.5 一個ALU的例子6.6 關系積的計算6.7 符號化的LTL模型檢測第7章基于μ-演算的模型檢測7.1 簡介7.2 命題μ-演算7.3 求不動點公式的值7.4 用OBDD表示μ-演算公式7.5 將CTL公式轉(zhuǎn)化為μ-演算7.6 復雜度問題第8章實際中的模型檢測8.1 模型檢測器——SMV8.2 一個實際的例子第9章模型檢測和自動機理論9.1 有限字與無限字上的自動機9.2 用自動機進行模型檢測9.3 檢查Büchi自動機接受的語言是否為空9.4 LTL公式轉(zhuǎn)化為自動機9.5 “on-the-fly”模型檢測9.6 檢測語言包含的符號方法第10章偏序約簡10.1 異步系統(tǒng)中的并發(fā)10.2 獨立性與不可見性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 假設保證方法的證明12.3 CPU控制器的驗證第13章抽象13.1 影響錐化簡13.2 數(shù)值抽象第14章對稱性14.1 群和對稱性14.2 商模型14.3 對稱性和模型檢測14.4 復雜性問題14.5 試驗結(jié)果第15章有限狀態(tài)系統(tǒng)的無限簇15.1 無限簇上的時序邏輯15.2 不變量15.3 再次分析Futurebus+15.4 圖和網(wǎng)絡文法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 時間約束自動機17.2 并行組合17.3 使用時間約束自動機進行建模17.4 時鐘域17.5 時鐘區(qū)17.6 邊界可區(qū)分矩陣17.7 對復雜度的考慮第18章結(jié)論參考文獻