書籍信息
作譯者：吳盡昭 等
出版時間：2018-11千 字 數：346版次：01-01頁 數：240
開本：16開裝幀：I S B N ：9787121352744
換版：
紙質書定價：￥69.0
內容簡介
模型檢測是一種用於自動驗證有限狀態並發系統的技術，與基於模擬、測試和演繹推理的傳統技術相比，具有許多方面的優勢。本書共分18章，涵蓋的主要內容包括模型檢測的基本知識、模態邏輯、符號化技術、SATSolver、限界模型檢測、自動機上的模型檢測、抽象解釋、程式分析、實時系統驗證，同時介紹NuSMV和UPPAAL兩個流行的模型檢測器。
圖書目錄
第1章 緒論 1
1.1 形式化方法的需求 1
1.2 硬體與軟體驗證 1
1.3 模型檢測的流程 3
1.4 時序邏輯與模型檢測 3
1.5 符號算法 4
1.6 偏序約簡 6
1.7 緩解狀態爆炸問題的其他方法 7
第2章 系統建模 8
2.1 並發系統建模 8
2.2 並發系統 11
2.3 程式翻譯的實例 16
第3章 時序邏輯 18
3.1 計算樹邏輯CTL* 18
3.2 CTL和LTL邏輯 20
3.3 公正性 22
第4章 模型檢測 24
4.1 CTL模型檢測 24
4.2 基於tableau結構的LTL模型檢測 29
4.3 CTL*模型檢測 33
第5章 二叉判定圖 36
5.1 布爾公式的表示方法 36
5.2 Kripke結構的表示方法 40
第6章 符號模型檢測 42
6.1 不動點表示 42
6.2 CTL符號模型檢測 45
6.3 符號模型檢測中的公正性 48
6.4 反例和診斷信息 50
6.5 一個ALU的例子 52
6.6 關係積的計算 54
6.7 符號化的LTL模型檢測 61
第7章 基於? 演算的模型檢測 68
7.1 簡介 68
7.2 命題? 演算 68
7.3 求不動點公式的值 71
7.4 用OBDD表示? 演算公式 74
7.5 將CTL公式轉化為? 演算 75
7.6 複雜度問題 76
第8章 實踐中的模型檢測 77
8.1 SMV模型檢測器 77
8.2 一個實際的例子 80
第9章 模型檢測和自動機理論 85
9.1 有限字與無限字上的自動機 85
9.2 使用自動機進行模型檢測 86
9.3 檢查Büchi自動機接受的語言是否為空 90
9.4 LTL公式轉化為自動機 93
9.5 採用“On-the-Fly”技術的模型檢測 97
9.6 檢測語言包含的符號方法 98
第10章 偏序約簡 100
10.1 異步系統中的並發 101
10.2 獨立性與不可見性 102
10.3 LTL?X的偏序約簡 104
10.4 一個例子 107
10.5 計算充足集(ample)集合 109
10.6 算法的正確性 114
10.7 SPIN系統中的偏序約簡 117
第11章 結構間的等價性和擬序 122
11.1 等價和擬序算法 128
11.2 構建tableau結構 129
第12章 組合推理 133
12.1 多個結構的組合 134
12.2 判斷假設保證證明方法的正確性 136
12.3 CPU控制器的驗證 136
