基于動態(tài)符號執(zhí)行的MSVL程序模型檢測理論與方法.pdf

1、軟件已經(jīng)成為國防建設(shè)與國計民生的重要組成部分，如何提高軟件的正確性、可靠性和安全性是計算機軟件領(lǐng)域面臨的重要挑戰(zhàn)。Clarke等人提出的模型檢測方法被認為是迄今為止應(yīng)對這一挑戰(zhàn)的最具潛力的方法之一。模型檢測方法已經(jīng)成功用于對計算機軟件系統(tǒng)的驗證中，但仍存在一些不足：（1）軟件模型難以提??；（2）性質(zhì)描述語言的表達能力不足，部分程序性質(zhì)無法描述；（3）模型和性質(zhì)不在同一體系；（4）狀態(tài)空間爆炸問題。
　　為了解決模型檢測中存在的問題

2、，本文對現(xiàn)有的模型檢測方法和動態(tài)符號執(zhí)行方法進行研究，將動態(tài)符號執(zhí)行技術(shù)應(yīng)用于模型檢測領(lǐng)域，給出了一種新的模型檢測方法。本文的主要貢獻包含以下三點。
　　1.研究了建模、仿真和驗證語言（Modeling,Simulation and Verification Language, MSVL）與命題投影時序邏輯（Propositional Projection Temporal Logic, PPTL）的語法結(jié)構(gòu)、基本語義和范式理論，

3、提出了基于動態(tài)符號執(zhí)行的MSVL程序模型檢測理論和方法，從四個方面來應(yīng)對模型檢測中存在四個問題。（1）通過 MSVL程序的動態(tài)符號執(zhí)行獲取程序的符號執(zhí)行樹作為模型，利用程序執(zhí)行的方式避免了程序模型提取的困難。（2）利用PPTL描述待驗證的系統(tǒng)性質(zhì)，由于PPTL的表達能力等價于完全正則語言，克服了性質(zhì)描述語言表達能力不足的問題。（3）MSVL和PPTL同屬投影時序邏輯（Projection Temporal Logic, PTL）系統(tǒng)，模

4、型和性質(zhì)在同一體系，不需要進行額外轉(zhuǎn)換，驗證效率高。（4）MSVL程序動態(tài)符號執(zhí)行得到的符號執(zhí)行樹是一個抽象模型，該模型的一條路徑代表了滿足路徑約束的所有輸入對應(yīng)的執(zhí)行路徑。這種對模型的抽象方式能夠顯著地壓縮程序模型的狀態(tài)數(shù)，有效地緩解了狀態(tài)空間爆炸問題。
　　2.基于現(xiàn)有的MSVL解釋器，設(shè)計了基于動態(tài)符號執(zhí)行的MSVL程序模型檢測工具的基本框架，給出了該模型檢測工具的三個主要模塊的設(shè)計與實現(xiàn)方案，最后利用C++編程實現(xiàn)了該模型