為了提高大規(guī)模軟件系統(tǒng)的可靠性和安全性,程序的形式化驗(yàn)證受到廣泛關(guān)注。傳統(tǒng)模型檢測(cè)方法需要從源代碼中提取模型,然而,隨著程序規(guī)模增大以及結(jié)構(gòu)的復(fù)雜化,從程序中提取模型變得異常困難,任何一個(gè)錯(cuò)誤都可能造成模型和源程序的不一致。近年來,源代碼級(jí)別的形式化驗(yàn)證已成為一個(gè)重要的研究課題。其研究主要分為以下三個(gè)方向:第一,可達(dá)性分析方法,該方法在待驗(yàn)證程序中插樁錯(cuò)誤標(biāo)簽,然后通過分析錯(cuò)誤標(biāo)簽的可達(dá)性來驗(yàn)證程序是否滿足指定性質(zhì),然而該方法僅能進(jìn)行安全性驗(yàn)證,而無法驗(yàn)證諸如活性的其他時(shí)序性質(zhì)。第二,靜態(tài)軟件模型檢測(cè)方法,該方法不執(zhí)行程序,靜態(tài)檢測(cè)程序所有路徑,從而使得較小規(guī)模程序都可能產(chǎn)生很大的狀態(tài)空間,因此很難驗(yàn)證大規(guī)模程序,且驗(yàn)證效率不高。而且由于沒有程序的執(zhí)行信息,導(dǎo)致精確性不夠,可能產(chǎn)生誤報(bào)。第三,運(yùn)行時(shí)驗(yàn)證方法,在執(zhí)行程序時(shí)提取事件信息,構(gòu)造監(jiān)控器來檢測(cè)當(dāng)前的執(zhí)行路徑是否滿足指定性質(zhì),由于每次只驗(yàn)證一條路徑,避免了狀態(tài)空間爆炸問題。盡管在代碼級(jí)別程序驗(yàn)證方面已有一些研究工作,然而現(xiàn)有技術(shù)并不成熟,現(xiàn)有驗(yàn)證工具仍無法處理大規(guī)模應(yīng)用程序。本文圍繞代碼級(jí)別的形式化驗(yàn)證方法進(jìn)行研究,主要工作如下:... 

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

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

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

【部分圖文】：

運(yùn)行時(shí)驗(yàn)證框架

這里的<==即為MSVL語句中的賦值操作，編寫程序時(shí)，由于編譯器無法識(shí)別特殊字符 ，我們用<==替代 。如圖3.2所示，圖左邊是LNFG，右邊是由它生成的MSVL程序。因?yàn)橹挥幸粋�(gè)fin標(biāo)記 1出現(xiàn)在節(jié)點(diǎn)2中，所以我們將它存儲(chǔ)在集合 2= { 1}中。最初，初始節(jié)點(diǎn)集合被轉(zhuǎn)為程序CuNode <== 1 or CuNode <== 2。對(duì)于節(jié)點(diǎn)1，從1到3的邊轉(zhuǎn)換成if( ) then{CuNode := 3}else{false}，從1到4的邊轉(zhuǎn)換成if(true)then{CuNode :=4}else {false}，等價(jià)為CuNode := 4。于是有 1=“if( )then{CuNode := 3}else{false}38

′ 在執(zhí)行該程序時(shí)，可以獲取到一個(gè)如圖3.5(a)所示的無窮的無環(huán)路徑 = 0, 1, 2, 3, 4, 5, ... 。 然而，我們可以從中抽象出一個(gè)有環(huán)的簡化計(jì)算 ( ) = 0, 1, 2,47

【參考文獻(xiàn)】：
期刊論文
[1]形式化方法概貌[J]. 王戟,詹乃軍,馮新宇,劉志明.  軟件學(xué)報(bào). 2019(01)
[2]Model checking concurrent systems with MSVL[J]. Nan ZHANG,Zhenhua DUAN,Cong TIAN.  Science China（Information Sciences）. 2016(11)
[3]運(yùn)行時(shí)驗(yàn)證技術(shù)的研究進(jìn)展[J]. 張碩,賀飛.  計(jì)算機(jī)科學(xué). 2014(S2)



本文編號(hào)：3620796