模型檢驗(yàn)原理

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