在軟件可信性質(zhì)保證的諸多方法中,面向軟件源代碼的分析與驗(yàn)證具有重要意義。形式化方法在軟件可信性質(zhì)保證中有不可替代的作用,但是距離大規(guī)模廣泛應(yīng)用還有不小的差距。符號(hào)執(zhí)行是一種重要的形式化方法,在測(cè)試數(shù)據(jù)生成和靜態(tài)分析中有廣泛應(yīng)用。但是,符號(hào)執(zhí)行面臨一些問題。其中,內(nèi)存模型是影響符號(hào)執(zhí)行的精確性和可擴(kuò)展性的主要問題之一。 論文綜述了面向符號(hào)執(zhí)行的內(nèi)存模型問題的研究現(xiàn)狀,分析了符號(hào)執(zhí)行中符號(hào)狀態(tài)跟蹤面臨的主要問題和現(xiàn)有的內(nèi)存抽象的不足,提出了基于抽象符號(hào)表的內(nèi)存模型。抽象符號(hào)表的基本思想是,通過為可尋址對(duì)象生成抽象地址統(tǒng)一處理各種數(shù)據(jù)類型和建模內(nèi)存操作。研究了使用抽象符號(hào)表建立內(nèi)存模型的方法,給出了抽象地址生成方法以及符號(hào)執(zhí)行算法�；诔橄蠓�(hào)表的內(nèi)存模型能夠很好地解決面向符號(hào)執(zhí)行的內(nèi)存模型面臨的主要問題,包括指針和別名問題、類型不安全的內(nèi)存訪問和大小不確定的數(shù)據(jù)。最后,通過實(shí)驗(yàn)評(píng)估了基于抽象符號(hào)表的內(nèi)存模型,設(shè)計(jì)的一個(gè)符號(hào)執(zhí)行工具能夠精確地跟蹤符號(hào)狀態(tài),并且通過與其他內(nèi)存模型的比較,說明了這個(gè)內(nèi)存模型具有一定的可擴(kuò)展性。 精確而且可擴(kuò)展的內(nèi)存模型是提高符號(hào)執(zhí)行技術(shù)的實(shí)用性的關(guān)鍵,能夠有效地...

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

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

【部分圖文】：

則SymbolicState=<M,I號(hào)值的映射；，即程序計(jì)數(shù)器，指向下一個(gè)件。成面向硬件機(jī)器的目標(biāo)代碼，編語言定義精確的符號(hào)語義。編程，它定義各種數(shù)據(jù)類型的符號(hào)表狀態(tài)下，程序控制的流動(dòng)。如同bolicState=<M,IP,PC>更新置如下：PC的初始值設(shè)為....

存消耗也十分巨大。因此，精確的表示每字節(jié)數(shù)組內(nèi)存模型對(duì)即使很小的代碼段也代碼沒有動(dòng)態(tài)內(nèi)存分配并且是類型安全的代碼，但是不能精確分析系統(tǒng)軟件。monolithicmemorymodel）[26]在系統(tǒng)軟件的7]的內(nèi)存模型本質(zhì)上就是單片內(nèi)存模型。單分為不相交的區(qū)域（region）....

國防科學(xué)技術(shù)大學(xué)研究生院碩士學(xué)位論文存訪問只發(fā)生在少數(shù)數(shù)據(jù)上[26]。所以這種保守做法不但浪費(fèi)大量存儲(chǔ)空間，增加了數(shù)據(jù)讀寫代價(jià)。然而，ASTable對(duì)類型不安全的內(nèi)存訪問的支持是需求的，其可擴(kuò)展性比字節(jié)數(shù)組方法和單片內(nèi)存模型都好。用下面圖4.3中的一個(gè)的例子演示三者之間的區(qū)別....

ainteger1node1S5120678910p&char15node2S105圖4.7ASTable方法在圖4.3代碼片段的L2處的內(nèi)存布通過為每個(gè)大小不確定數(shù)據(jù)生成單獨(dú)的全局ASTable，允許這縮或擴(kuò)展，而不必在這些數(shù)據(jù)生成時(shí)對(duì)其大小....

本文編號(hào)：3966787