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

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

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

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

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

【部分圖文】：

驗證操作示例

驗證進程信息

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

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

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



本文編號：3087769