模型檢測(cè)

定　價(jià)：￥69.00

作　者：	（美）埃德蒙,·,M.,克拉克等
出版社：	電子工業(yè)出版社
叢編項(xiàng)：
標(biāo)　簽：	暫缺

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

ISBN：	9787121352744	出版時(shí)間：	2018-11-01	包裝：
開(kāi)本：	16開(kāi)	頁(yè)數(shù)：	240	字?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ū)共分18章，涵蓋的主要內(nèi)容包括模型檢測(cè)的基本知識(shí)、模態(tài)邏輯、符號(hào)化技術(shù)、SATSolver、限界模型檢測(cè)、自動(dòng)機(jī)上的模型檢測(cè)、抽象解釋、程序分析、實(shí)時(shí)系統(tǒng)驗(yàn)證，同時(shí)介紹NuSMV和UPPAAL兩個(gè)流行的模型檢測(cè)器。

作者簡(jiǎn)介

　　Edmund M.Clarke教授，美國(guó)卡內(nèi)基？梅隆大學(xué)計(jì)算機(jī)科學(xué)系教授，并且是ACM和IEEE會(huì)士。他在軟硬件驗(yàn)證、自動(dòng)定理證明、形式方法等方面享有崇高的國(guó)際聲譽(yù)，2007年獲得ACM圖靈獎(jiǎng)。吳盡昭，廣西大學(xué)副校長(zhǎng)，長(zhǎng)期從事高效能高可信計(jì)算與推理理論與工具的研究和開(kāi)發(fā)，研究領(lǐng)域涉及符號(hào)計(jì)算、自動(dòng)推理、形式化方法及其交叉、融合與應(yīng)用；在國(guó)內(nèi)外學(xué)術(shù)刊物和國(guó)際會(huì)議論文集上發(fā)表研究論文107篇，出版專著3部，獲得軟件著作權(quán)6項(xiàng)，申請(qǐng)專利3項(xiàng)；近年來(lái)承擔(dān)國(guó)家自然科學(xué)基金、863、973子課題等國(guó)家、省部級(jí)科研項(xiàng)目10余項(xiàng)。

圖書(shū)目錄

目錄
第1章緒論\t1
1．1 形式化方法的需求\t1
1．2 硬件與軟件驗(yàn)證\t1
1．3 模型檢測(cè)的流程\t3
1．4 時(shí)序邏輯與模型檢測(cè)\t3
1．5 符號(hào)算法\t4
1．6 偏序約簡(jiǎn)\t6
1．7 緩解狀態(tài)爆炸問(wèn)題的其他方法\t7
第2章系統(tǒng)建模\t8
2．1 并發(fā)系統(tǒng)建模\t8
2．2 并發(fā)系統(tǒng)\t11
2．3 程序翻譯的實(shí)例\t16
第3章時(shí)序邏輯\t18
3．1 計(jì)算樹(shù)邏輯CTL*\t18
3．2 CTL和LTL邏輯\t20
3．3 公正性\t22
第4章模型檢測(cè)\t24
4．1 CTL模型檢測(cè)\t24
4．2 基于tableau結(jié)構(gòu)的LTL模型檢測(cè)\t29
4．3 CTL*模型檢測(cè)\t33
第5章二叉判定圖\t36
5．1 布爾公式的表示方法\t36
5．2 Kripke結(jié)構(gòu)的表示方法\t40
第6章符號(hào)模型檢測(cè)\t42
6．1 不動(dòng)點(diǎn)表示\t42
6．2 CTL符號(hào)模型檢測(cè)\t45
6．3 符號(hào)模型檢測(cè)中的公正性\t48
6．4 反例和診斷信息\t50
6．5 一個(gè)ALU的例子\t52
6．6 關(guān)系積的計(jì)算\t54
6．7 符號(hào)化的LTL模型檢測(cè)\t61
第7章基于? 演算的模型檢測(cè)\t68
7．1 簡(jiǎn)介\t68
7．2 命題? 演算\t68
7．3 求不動(dòng)點(diǎn)公式的值\t71
7．4 用OBDD表示? 演算公式\t74
7．5 將CTL公式轉(zhuǎn)化為? 演算\t75
7．6 復(fù)雜度問(wèn)題\t76
第8章實(shí)踐中的模型檢測(cè)\t77
8．1 SMV模型檢測(cè)器\t77
8．2 一個(gè)實(shí)際的例子\t80
第9章模型檢測(cè)和自動(dòng)機(jī)理論\t85
9．1 有限字與無(wú)限字上的自動(dòng)機(jī)\t85
9．2 使用自動(dòng)機(jī)進(jìn)行模型檢測(cè)\t86
9．3 檢查Büchi自動(dòng)機(jī)接受的語(yǔ)言是否為空\(chéng)t90
9．4 LTL公式轉(zhuǎn)化為自動(dòng)機(jī)\t93
9．5 采用“On-the-Fly”技術(shù)的模型檢測(cè)\t97
9．6 檢測(cè)語(yǔ)言包含的符號(hào)方法\t98
第10章偏序約簡(jiǎn)\t100
10．1 異步系統(tǒng)中的并發(fā)\t101
10．2 獨(dú)立性與不可見(jiàn)性\t102
10．3 LTL?X的偏序約簡(jiǎn)\t104
10．4 一個(gè)例子\t107
10．5 計(jì)算充足集(ample)集合\t109
10．6 算法的正確性\t114
10．7 SPIN系統(tǒng)中的偏序約簡(jiǎn)\t117
第11章結(jié)構(gòu)間的等價(jià)性和擬序\t122
11．1 等價(jià)和擬序算法\t128
11．2 構(gòu)建tableau結(jié)構(gòu)\t129
第12章組合推理\t133
12．1 多個(gè)結(jié)構(gòu)的組合\t134
12．2 判斷假設(shè)保證證明方法的正確性\t136
12．3 CPU控制器的驗(yàn)證\t136
第13章抽象\t139
13．1 影響錐化簡(jiǎn)\t139
13．2 數(shù)值抽象\t141
第14章對(duì)稱性\t154
14．1 群和對(duì)稱性\t154
14．2 商模型\t156
14．3 對(duì)稱性和模型檢測(cè)\t159
14．4 復(fù)雜度問(wèn)題\t160
14．5 實(shí)驗(yàn)結(jié)果\t164
第15章有限狀態(tài)系統(tǒng)的無(wú)限簇\t166
15．1 無(wú)限簇上的時(shí)序邏輯\t166
15．2 不變量\t167
15．3 再次分析Futurebus+\t169
15．4 圖和網(wǎng)絡(luò)文法\t171
15．5 令牌環(huán)簇的不確定性結(jié)果\t179
第16章離散實(shí)時(shí)系統(tǒng)和定量時(shí)序分析\t183
16．1 實(shí)時(shí)系統(tǒng)和單調(diào)變化率調(diào)度\t183
16．2 實(shí)時(shí)系統(tǒng)的模型檢測(cè)\t184
16．3 RTCTL模型檢測(cè)\t185
16．4 量化時(shí)序的分析：最小或最大延遲\t185
16．5 飛行控制器\t187
第17章連續(xù)實(shí)時(shí)系統(tǒng)\t192
17．1 時(shí)間約束自動(dòng)機(jī)\t192
17．2 并行組合\t194
17．3 使用時(shí)間約束自動(dòng)機(jī)進(jìn)行建模\t195
17．4 時(shí)鐘域\t198
17．5 時(shí)鐘區(qū)\t203
17．6 邊界可區(qū)分矩陣\t208
17．7 復(fù)雜度問(wèn)題\t211
第18章結(jié)論\t213
參考文獻(xiàn)\t215