Büchi自動(dòng)機(jī)模型檢測及其安全性分析應(yīng)用研究

第1章 緒論
1．1 研究背景
1．2 國內(nèi)外研究現(xiàn)狀
1．2．1 模型檢測相關(guān)研究
1．2．2 安全苛求系統(tǒng)的安全性研究現(xiàn)狀
1．2．3 模型檢測與安全性分析研究現(xiàn)狀
1．3 研究內(nèi)容
1．4 本書的結(jié)構(gòu)安排
第2章 基于Büchi自動(dòng)機(jī)的模型檢測理論與方法
2．1 Büchi自動(dòng)機(jī)基本原理
2．1．1 標(biāo)準(zhǔn)Büchi自動(dòng)機(jī)
2．1．2 廣義Büchi自動(dòng)機(jī)
2．2 模型檢測基本原理
2．2．1 系統(tǒng)建模
2．2．2 屬性描述
2．2．3 模型驗(yàn)證
2．3 基于LTL的模型檢測
2．4 基于Büchi自動(dòng)機(jī)的模型檢測方法
2．5 本章小結(jié)
第3章 基于啟發(fā)式NDFS的模型檢測算法
3．1 NDFS模型檢測算法研究現(xiàn)狀
3．2 基本概念及相關(guān)技術(shù)
3．2．1 TGBA簡介
3．2．2 相關(guān)技術(shù)
3．3 HNDFS算法描述
3．4 HNDFS算法正確性證明
3．5 HNDFS算法復(fù)雜度分析
3．6 實(shí)驗(yàn)與分析
3．7 本章小結(jié)
第4章 基于啟發(fā)式SCCs的廣義Büchi自動(dòng)機(jī)判空檢測算法
4．1 引言
4．2 HSCCsEC算法描述
4．4 HSCCsEC算法實(shí)例
4．5 HSCCsEC算法正確性證明
4．6 HSCCsEC算法復(fù)雜性分析
4．7 實(shí)驗(yàn)對比與分析
4．8 小結(jié)
第5章 基于啟發(fā)式On-the-fly的擴(kuò)展TGBA模型檢測算法
5．1 擴(kuò)展的TGBA模型
5．2 MCA_ETGBA算法描述
5．3 算法實(shí)例
5．4 正確性證明及復(fù)雜度分析
5．5 實(shí)驗(yàn)
5．6 小結(jié)
第6章 基于場景分析的系統(tǒng)形式化模型生成方法
6．1 OCL與FSP簡介
6．2 系統(tǒng)需求場景分析及形式化模型生成流程
6．3 系統(tǒng)需求場景的OCL分析子算法
6．4 系統(tǒng)形式化模型生成子算法
6．5 小結(jié)
第7章 基于LTS模型檢測的系統(tǒng)安全性驗(yàn)證方法
7．1 系統(tǒng)安全性驗(yàn)證相關(guān)原理
7．2 基于模型檢測的系統(tǒng)安全性驗(yàn)證方法
7．2．1 安全需求規(guī)格的形式化描述
7．2．2 基于LTS模型檢測的安全性驗(yàn)證方法
7．3 實(shí)例研究
7．4 本章小結(jié)
第8章 基于故障注入的系統(tǒng)安全性分析
8．1 引言
8．2 基于故障注入的模型檢測流程
8．3 基于故障注入的模型檢測算法描述
8．4 多故障注入的算法實(shí)例
8．5 形式化安全需求規(guī)格的獲取
8．6 本章小結(jié)
第9章 鐵路車站聯(lián)鎖系統(tǒng)的安全性分析研究
9．1 安全性分析流程
9．2 鐵路車站聯(lián)鎖系統(tǒng)中進(jìn)路建立的形式化建模
9．2．1 鐵路車站聯(lián)鎖系統(tǒng)進(jìn)路建立場景
9．2．2 鐵路車站聯(lián)鎖系統(tǒng)的進(jìn)路建立需求場景分析
9．2．3 鐵路車站聯(lián)鎖系統(tǒng)進(jìn)路建立的形式化模型生成
9．3 鐵路車站聯(lián)鎖系統(tǒng)中進(jìn)路建立的安全性驗(yàn)證
9．4 系統(tǒng)的形式化安全需求
9．5 小結(jié)
第10章 結(jié)束語
參考文獻(xiàn)