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

　　隨著計(jì)算機(jī)技術(shù)的迅速發(fā)展,人類生活對(duì)計(jì)算機(jī)軟件的依賴程度日益加深,在軟件功能日益強(qiáng)大的同時(shí),其復(fù)雜度和集成度也急劇增高,隨之而來(lái),軟件漏洞所引發(fā)的災(zāi)難也頻頻發(fā)生,尤其在一些關(guān)鍵領(lǐng)域,一個(gè)軟件漏洞就可能造成很嚴(yán)重的后果,因此,軟件的安全性和可靠性急需得到保證。程序驗(yàn)證作為一種驗(yàn)證軟件系統(tǒng)安全性和可靠性的驗(yàn)證技術(shù),致力于確定一個(gè)系統(tǒng)是否正確完成了預(yù)設(shè)的目標(biāo)。目前,程序驗(yàn)證已經(jīng)廣泛應(yīng)用到軟件安全相關(guān)的分析和驗(yàn)證中,并且取得了很大的成功。UMC4MSVL作為一個(gè)代碼級(jí)運(yùn)行時(shí)驗(yàn)證工具,它使用建模仿真驗(yàn)證語(yǔ)言（Modeling Simulation and Verification Language,MSVL）程序M描述系統(tǒng),命題投影時(shí)序邏輯（Propositional Projection Temporal Logic,PPTL）公式P描述性質(zhì),動(dòng)態(tài)執(zhí)行包含系統(tǒng)和性質(zhì)信息的程序來(lái)驗(yàn)證性質(zhì)的有效性。該工具對(duì)程序中不同分支采用深度優(yōu)先搜索的思想進(jìn)行驗(yàn)證,驗(yàn)證完一條分支路徑后,再去遍歷驗(yàn)證其它分支路徑。為了進(jìn)一步提高程序驗(yàn)證的效率,本文基于多核計(jì)算機(jī)提供的硬件基礎(chǔ)上,引入并行化的程序驗(yàn)證思想,實(shí)現(xiàn)UM... 

【文章來(lái)源】：西安電子科技大學(xué)陜西省 211工程院校 教育部直屬院校

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

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

【部分圖文】：

驗(yàn)證操作示例

驗(yàn)證進(jìn)程信息

(a)(b)圖5.3 狼羊菜用例測(cè)試對(duì)比圖 5.3 中圖 5.3(a)是串行的 UMC4MSVL 驗(yàn)證器的驗(yàn)證結(jié)果，圖 5.3(b)是線程池大小設(shè)為 4 下的并行化驗(yàn)證結(jié)果。

【參考文獻(xiàn)】：
期刊論文
[1]二維邏輯PPTLSL的可滿足性檢查[J]. 陸旭,段振華,田聰.  軟件學(xué)報(bào). 2016(03)
[2]一個(gè)命題投影時(shí)序邏輯符號(hào)模型檢測(cè)器[J]. 逄濤,段振華,劉曉芳.  軟件學(xué)報(bào). 2015(08)
[3]構(gòu)造偶階幻方的一個(gè)算法[J]. 段振華.  微電子學(xué)與計(jì)算機(jī). 1990(04)

博士論文
[1]面向?qū)ο驧SVL語(yǔ)言及其在組合Web服務(wù)驗(yàn)證中的應(yīng)用[D]. 王小兵.西安電子科技大學(xué) 2009



本文編號(hào)：3087769