發(fā)布時(shí)間：2021-03-21 21:27

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

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

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

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

【部分圖文】：

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

圖２．２?—個(gè)簡(jiǎn)單Ｋｒｉｐｋｅ結(jié)構(gòu)??Ｆｉｇ．?２．２?Ａ?Ｓｉｍｐｌｅ?Ｋｒｉｐｋｅ?Ｓｔｒｕｃｔｕｒｅ??．［ｕ］

圖３．１?—個(gè)簡(jiǎn)單多值Ｋｒｉｐｋｅ結(jié)構(gòu)??

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



本文編號(hào)：3093567