基于關(guān)系數(shù)據(jù)理論的函數(shù)型程序似然不變量動(dòng)態(tài)檢測(cè)方法.pdf

1、隨著計(jì)算機(jī)技術(shù)的發(fā)展,軟件在各個(gè)行業(yè)得到廣泛的應(yīng)用,人們對(duì)軟件的質(zhì)量和安全也得到更為廣泛的關(guān)注。對(duì)如何提高軟件質(zhì)量的問(wèn)題人們已經(jīng)從軟件開發(fā)方法、軟件開發(fā)過(guò)程管理、軟件開發(fā)工具等多個(gè)方面加以研究,取得了一定的成績(jī)。基于合約的軟件開發(fā)是其中十分重要且得到廣泛應(yīng)用的一種技術(shù)。軟件合約是指軟件中必須遵守的規(guī)則。開發(fā)者和執(zhí)行者通過(guò)遵守這些合約來(lái)保證軟件的質(zhì)量。從不同的層面合約可分為語(yǔ)法合約、數(shù)據(jù)合約、行為合約和服務(wù)合約。程序不變量是數(shù)據(jù)合約的一種

2、形式。程序不變量對(duì)于程序演進(jìn)與重構(gòu)、程序測(cè)試與排錯(cuò)、輔助定理證明、構(gòu)件升級(jí)替換都有重要作用。由于大多數(shù)軟件開發(fā)時(shí)都沒有書寫形式化文檔,程序不變量在程序中很少被清楚地表示出來(lái)。如何從程序中發(fā)現(xiàn)這些隱含的沒有被程序員寫出來(lái)的程序不變量成為實(shí)現(xiàn)高層次行為合約、提高程序質(zhì)量的關(guān)鍵。
　　本文重點(diǎn)研究如何使用動(dòng)態(tài)檢測(cè)技術(shù)發(fā)現(xiàn)程序中函數(shù)型似然不變量。論文首先介紹了不變量動(dòng)態(tài)檢測(cè)技術(shù)及其主要的兩個(gè)實(shí)現(xiàn)工具:Daikon和DIDUCE,并分析了它

3、們?cè)诰幣涔ぞ吆筒蛔兞繖z測(cè)方法上存在的不足。然后運(yùn)用面向?qū)ο蟮能浖_發(fā)方法,設(shè)計(jì)并實(shí)現(xiàn)了一個(gè)新的基于關(guān)系數(shù)據(jù)庫(kù)的編配工具。新的編配工具具有易用、靈活等特點(diǎn)。結(jié)合關(guān)系數(shù)據(jù)理論,針對(duì)函數(shù)型不變量提出了一個(gè)啟發(fā)式不變量檢測(cè)方法。該方法通過(guò)函數(shù)推導(dǎo)技術(shù)首先確定待檢變量中是否存在函數(shù)依賴關(guān)系,然后再進(jìn)行函數(shù)解析式推導(dǎo),解決了傳統(tǒng)似然不變量檢測(cè)方法中存在的盲目性問(wèn)題。并對(duì)新方法和傳統(tǒng)方法進(jìn)行了對(duì)比實(shí)驗(yàn)分析,實(shí)驗(yàn)結(jié)果表明新方法的可靠性與檢測(cè)效率明顯優(yōu)于