隨著軟硬件系統(tǒng)的日益復(fù)雜,保證系統(tǒng)的安全性至關(guān)重要。模型檢測是自動驗(yàn)證系統(tǒng)正確性的有效技術(shù),目前已經(jīng)廣泛應(yīng)用于計算機(jī)軟硬件系統(tǒng),通信協(xié)議,安全協(xié)議等方面的分析與驗(yàn)證中。針對包含非確定性信息、不完備信息的并發(fā)系統(tǒng)的形式化驗(yàn)證問題,本文研究了兩種定量模型檢測算法。（1）基于可能性理論,模糊邏輯等理論,研究了基于廣義可能性決策過程的μ-演算模型檢測算法。首先引入廣義可能性決策過程作為系統(tǒng)模型,接著對經(jīng)典的命題μ-演算進(jìn)行改進(jìn)和擴(kuò)展,給出廣義可能性μ-演算的概念,用于描述非確定系統(tǒng)的屬性特征。然后提出廣義可能性μ-演算模型檢測算法,并將模型檢測問題簡化為模糊矩陣運(yùn)算,最后通過具體的實(shí)例進(jìn)行了分析與驗(yàn)證。與經(jīng)典的μ-演算相比,廣義可能性μ-演算具有更強(qiáng)的表達(dá)力,能夠刻畫不確定系統(tǒng)的屬性特征,模型檢測算法能夠給出系統(tǒng)滿足屬性的可能性程度,研究成果擴(kuò)大了廣義可能性測度在模型檢測中的應(yīng)用范圍。（2）在格理論,多值邏輯的基礎(chǔ)上,研究了基于多值Kripke結(jié)構(gòu)的多值μ-演算模型檢測算法,將多值Kripke結(jié)構(gòu)作為系統(tǒng)模型,對經(jīng)典μ-演算語言進(jìn)行擴(kuò)展,用于描述多值系統(tǒng)的屬性,提出了多值μ-演算模型檢測算法,... 

【文章來源】：北方民族大學(xué)寧夏回族自治區(qū)

【文章頁數(shù)】：60 頁

【學(xué)位級別】：碩士

【部分圖文】：

多值模型檢測器Chek的圖形界面

【參考文獻(xiàn)】：
期刊論文
[1]具有多值決策過程的廣義可能性計算樹邏輯模型檢測[J]. 袁申,魏杰林,李永明.  計算機(jī)工程與科學(xué). 2019(01)
[2]形式化方法概貌[J]. 王戟,詹乃軍,馮新宇,劉志明.  軟件學(xué)報. 2019(01)
[3]可能性測度下的CTL符號化模型檢測[J]. 雷麗暉,郭越,張延波.  計算機(jī)工程與科學(xué). 2018(11)
[4]具有DP的廣義可能性模糊時態(tài)CTL模型檢測[J]. 魏杰林,袁申,李永明,梁常建.  計算機(jī)科學(xué)與探索. 2019(10)
[5]不確定型模糊Kripke結(jié)構(gòu)的計算樹邏輯模型檢測[J]. 范艷煥,李永明,潘海玉.  電子學(xué)報. 2018(01)
[6]具有模糊時態(tài)的廣義可能性線性時序邏輯的模型檢測[J]. 梁常建,李永明.  電子學(xué)報. 2017(12)
[7]廣義可能性計算樹邏輯的模型檢測問題[J]. 梁常建,李永明.  電子學(xué)報. 2017(11)
[8]基于決策過程的廣義可能性計算樹邏輯模型檢測[J]. 馬占有,李永明.  中國科學(xué):信息科學(xué). 2016(11)
[9]廣義可能性決策過程的計算樹邏輯模型檢測[J]. 馬占有,李永明.  計算機(jī)工程與科學(xué). 2015(11)
[10]隨機(jī)模型檢驗(yàn)研究[J]. 劉陽,李宣東,馬艷,王林章.  計算機(jī)學(xué)報. 2015(11)

博士論文
[1]基于決策過程的廣義可能性時態(tài)邏輯模型檢測[D]. 馬占有.陜西師范大學(xué) 2017
[2]狀態(tài)轉(zhuǎn)換系統(tǒng)的格值量化驗(yàn)證方法研究[D]. 潘海玉.華東師范大學(xué) 2012

碩士論文
[1]可能性測度下并發(fā)系統(tǒng)的符號化模型檢測研究與實(shí)現(xiàn)[D]. 張延波.陜西師范大學(xué) 2018
[2]基于μ演算的認(rèn)知難題符號化模型檢測[D]. 楊志剛.華僑大學(xué) 2017
[3]基于可能性測度的計算樹邏輯和Kripke結(jié)構(gòu)決策過程[D]. 薛艷.陜西師范大學(xué) 2012



本文編號：3270958