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

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

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

【學位級別】：博士

【部分圖文】：

運行時驗證框架

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

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

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



本文編號：3620796