現(xiàn)代計算機技術已經(jīng)時時刻刻伴隨著我們的生活,隨著現(xiàn)代計算機軟件和硬件的設計越來越復雜,對軟件和硬件的測試也變得越來越復雜,不僅需要消耗大量的人力物力成本,而且使用傳統(tǒng)的檢測技術也有一定的局限性,對于生活中真實存在的一些不確定性因素,存在著一定的檢測缺陷,從而導致檢測失敗。1981年,Clarke和Emerson以及Quielle和Sifakis提出了模型檢測的理論,作為一種形式化的自動驗證技術,為我們解決這些檢測問題提供了一個很好的解決方案。對比傳統(tǒng)的檢測技術,模型檢測技術有著一系列的優(yōu)勢,比如可以在系統(tǒng)實現(xiàn)之前對系統(tǒng)進行驗證,提前發(fā)現(xiàn)問題,節(jié)約檢測成本等等,這些檢測一般會使用基于模型檢測理論實現(xiàn)的模型檢測器去進行驗證,傳統(tǒng)的模型檢測器大多是基于一些經(jīng)典的理論而實現(xiàn)的,隨著我們研究的深入,我們發(fā)現(xiàn)現(xiàn)實生活中有著大量的不確定信息,這樣使用傳統(tǒng)理論實現(xiàn)的模型檢測器無法解決這些問題。而多值模型檢測理論的出現(xiàn),利用在格上構建不確定信息,結合多值計算樹邏輯,通過構建的多值可能性Kripke結構模型,有效的解決了這些問題。同時為了實現(xiàn)模型檢測技術的自動化驗證的特性的優(yōu)勢,本文基于多值可能性的多值計... 

【文章來源】：陜西師范大學陜西省 211工程院校 教育部直屬院校

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

【學位級別】：碩士

【部分圖文】：

圖２．１模型檢測流程圖??Ｆｉｇ．?２．１?Ｍｏｄｅｌ?Ｃｈｅｃｋｉｎｇ?Ｆｌｏｗ?Ｃｈａｒｔ??

圖２．２?—個簡單Ｋｒｉｐｋｅ結構??Ｆｉｇ．?２．２?Ａ?Ｓｉｍｐｌｅ?Ｋｒｉｐｋｅ?Ｓｔｒｕｃｔｕｒｅ??．［ｕ］

圖３．１?—個簡單多值Ｋｒｉｐｋｅ結構??

【參考文獻】：
期刊論文
[1]不確定型模糊Kripke結構的計算樹邏輯模型檢測[J]. 范艷煥,李永明,潘海玉.  電子學報. 2018(01)
[2]基于決策過程的廣義可能性計算樹邏輯模型檢測[J]. 馬占有,李永明.  中國科學:信息科學. 2016(11)
[3]隨機模型檢驗研究[J]. 劉陽,李宣東,馬艷,王林章.  計算機學報. 2015(11)
[4]可能LTL模型檢測的兩種方法[J]. 李永明.  陜西師范大學學報(自然科學版). 2014(06)
[5]可能性測度下計算樹邏輯的若干性質[J]. 李亞利,李永明.  陜西師范大學學報(自然科學版). 2013(06)
[6]基于可能性測度的計算樹邏輯CTL*與可能性互模擬[J]. 鄧輝,薛艷,李亞利,李永明.  計算機科學. 2012(10)
[7]概率計算樹邏輯的限界模型檢測[J]. 周從華,劉志鋒,王昌達.  軟件學報. 2012(07)
[8]基于可能性測度的計算樹邏輯[J]. 薛艷,雷紅軒,李永明.  計算機工程與科學. 2011(09)
[9]使用局部建模的微處理器測試程序自動生成方法[J]. 張良,易江芳,佟冬,程旭,王克義.  電子學報. 2011(07)
[10]龍芯2號微處理器浮點除法功能部件的形式驗證[J]. 陳云霽,馬麟,沈海華,胡偉武.  計算機研究與發(fā)展. 2006(10)



本文編號：3093567