模型檢測(cè)

定　價(jià)：￥69.00

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

購(gòu)買這本書(shū)可以去

ISBN：	9787121272950	出版時(shí)間：	2016-02-01	包裝：	平塑
開(kāi)本：		頁(yè)數(shù)：	236	字?jǐn)?shù)：

內(nèi)容簡(jiǎn)介

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

作者簡(jiǎn)介

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

圖書(shū)目錄

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