模型檢驗原理

●章 系統(tǒng)驗證
1.1 模型檢驗
1.2 模型檢驗的特征
1.2.1 模型檢驗的步驟
1.2.2 模型檢驗的優(yōu)點與缺點
1.3 文獻說明
第2章 并發(fā)系統(tǒng)的建模
2.1 遷移系統(tǒng)
2.1.1 執(zhí)行
2.1.2 硬件和軟件系統(tǒng)的建模
2.2 并行與通信
2.2.1 并發(fā)與交錯
2.2.2 用共享變量通信
2.2.3 握手
2.2.4 通道系統(tǒng)
2.2.5 nanoPromela
2.2.6 同步并行性
2.3 狀態(tài)空間爆炸問題
2.4 總結
2.5 文獻說明
2.6 習題
第3章 線性時間性質(zhì)
3.1 死鎖
3.2 線性時間行為
3.2.1 路徑與狀態(tài)圖
3.2.2 跡
3.2.3 線性時間性質(zhì)
3.2.4 跡等價與線性時間性質(zhì)
3.3 安全性質(zhì)與不變式
3.3.1 不變式
3.3.2 安傘件質(zhì)
3.3.3 跡等價與安全性質(zhì)
3.4 活性性質(zhì)
3.4.1 活性性質(zhì)概念
3.4.2 安全性質(zhì)與活性性質(zhì)
3.5 公平性
3.5.1 公平性約束
3.5.2 公平性策略
3.5.3 公平性與安全性
3.6 總結
3.7 文獻說明
3.8 習題
第4章 正則性質(zhì)
4.1 有限單詞上的自動機
4.2 正則安全性質(zhì)的模型檢驗
4.2.1 正則安全性質(zhì)
4.2.2 驗證正則安全性質(zhì)
4.3 無限單詞上的自動機
4.3.1 ω正則語言與性質(zhì)
4.3.2 未定Buchi自動機
4.3.3 確定Buchi自動機
4.3.4 廣義未定Buchi自動機
4.4 模型檢驗ω正則性質(zhì)
4.4.1 持久性質(zhì)與乘積
4.4.2 嵌套深度優(yōu)先搜索
4.5 總結
4.6 文獻說明
4.7 習題
第5章 線性時序邏輯
5.1 線性時序邏輯述要
5.1.1 語法
5.1.2 語義
5.1.3 準述性質(zhì)
5.1.4 LTL公式的等價性
5.1.5 弱直到、釋放和正范式
5.1.6 LTL中的公平性
5.2 基于自動機的LTL模型檢驗
5.2.1 LTL模型檢驗問題的復雜度
5.2.2 LTL可滿足性和有效性檢驗
5.3 總結
5.4 文獻說明
5.5 習題
第6章 計算樹邏輯
6.1 引言
6.2 計算樹邏輯
6.2.1 語法
6.2.2 語義
6.2.3 CTL公式的等價性
6.2.4 CTL范式
6.3 LTL與CTL的表達力對比
CTL模型檢驗
.1 基本算法
.2 直到和存在總是運算符
.3 時間復雜度和空間復雜度
6.5 CTL的公平性
6.6 反例和證據(jù)
6.6.1 CTL中的反例
6.6.2 公平CTL中的反例和證據(jù)
6.7 符號CTL模型檢驗
6.7.1 開關函數(shù)
6.7.2 用開關函數(shù)編碼遷移系統(tǒng)
6.7.3 有序二決策圖
6.7.4 實現(xiàn)基于ROBDD的算法
6.8 CTL
6.8.1 邏輯、表達力和等價
6.8.2 CTL模型檢驗
6.9 總結
6.10 文獻說明
6.11 習題
第7章 等價和抽象
7.1 互模擬
7.1.1 互模擬商
7.1.2 基于動作的互模擬
7.2 互模擬和CTL等價
7.3 求互模擬商的算法
7.3.1 確定初始劃分
7.3.2 細化劃分
7.3.3 個劃分細化算法
7.3.4 效率改進
7.3.5 遷移系統(tǒng)的等價檢驗
7.4 模擬關系
7.4.1 模擬等價
7.4.2 互模擬、模擬與跡等價
7.5 模擬等價和CTL等價
7.6 求模擬商的算法
7.7 踏步線性時間關系
7.7.1 踏步跡等價
7.7.2 踏步跡等價和LTLO等價
7.8 踏步互模擬
7.8.1 發(fā)散敏感的踏步互模擬
7.8.2 賦范互模擬
7.8.3 踏步互模擬和CTLO等價
7.8.4 踏步互模擬求商
7.9 總結
7.10 文獻說明
7.11 習題
第8章 偏序約簡
8.1 動作的無關性
8.2 線性時間的充足集方法
8.2.1 充足集的條件
8.2.2 動態(tài)偏序約簡
8.2.3 計算充足集
8.2.4 靜態(tài)偏序約簡
8.3 分支時間的充足集方法
8.4 總結
8.5 文獻說明
8.6 習題
第9章 時控自動機
9.1 時控自動機述要
9.1.1 語義
9.1.2 時間發(fā)散、時間鎖定和芝諾性
9.2 時控計算樹邏輯
9.3 TCTL模型檢驗
9.3.1 消去時間參數(shù)
9.3.2 區(qū)域遷移系統(tǒng)
9.3.3 TCTL模型檢驗算法
9.4 總結
9.5 文獻說明
9.6 習題
0章 概率系統(tǒng)
10.1 馬爾可夫鏈
10.1.1 可達性概率
10.1.2 定性性質(zhì)
10.2 概率計算樹邏輯
10.2.1 PCTL模型檢驗
10.2.2 PCTL的定性片段
10.3 線性時間性質(zhì)
10.4 PCTL和概率互模擬
10.4.1 PCTL
10.4.2 概率互模擬
10.5 帶成本的馬爾可夫鏈
10.5.1 成本有界可達性
10.5.2 長遠性質(zhì)
10.6 馬爾可夫決策過程
10.6.1 可達性概率
10.6.2 PCTL模型檢驗
10.6.3 極限性質(zhì)
10. 線性時間性質(zhì)和PCTL
10.6.5 公平性
10.7 總結
10.8 文獻說明
10.9 習題
附錄A 預備知識
A.1 常用符號與記號
A.2 形式語言
A.3 命題邏輯 ……