注冊(cè) | 登錄讀書好,好讀書,讀好書!
讀書網(wǎng)-DuShu.com
當(dāng)前位置: 首頁(yè)出版圖書科學(xué)技術(shù)工業(yè)技術(shù)金屬學(xué)、金屬工藝模型檢測(cè)

模型檢測(cè)

模型檢測(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)買這本書可以去


ISBN: 9787121272950 出版時(shí)間: 2016-02-01 包裝: 平塑
開本: 頁(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ì)。本書涵蓋的內(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)。

圖書目錄

目 錄第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ì)算樹邏輯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ú)立性與不可見性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)

本目錄推薦

掃描二維碼
Copyright ? 讀書網(wǎng) m.ranfinancial.com 2005-2020, All Rights Reserved.
鄂ICP備15019699號(hào) 鄂公網(wǎng)安備 42010302001612號(hào)