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

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

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

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

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