模型檢測

定　價：￥69.00

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

購買這本書可以去

ISBN：	9787121352744	出版時間：	2018-11-01	包裝：
開本：	16開	頁數(shù)：	240	字?jǐn)?shù)：

內(nèi)容簡介

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

作者簡介

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

圖書目錄

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