依賴分析在程序驗(yàn)證和遺留系統(tǒng)改造中的應(yīng)用.pdf

1、在眾多保障軟件可靠性和安全性的途徑中，采用形式化方法對(duì)系統(tǒng)進(jìn)行形式化驗(yàn)證和分析是被很多計(jì)算機(jī)科學(xué)家所認(rèn)同的。形式化驗(yàn)證主要包括兩類方法：一是以邏輯推理為基礎(chǔ)的定理證明，另一是以窮盡搜索為基礎(chǔ)的模型檢測。二者相比，前者自動(dòng)化程度弱于后者，但因其表達(dá)力較強(qiáng)，加之自動(dòng)定理證明技術(shù)的日益進(jìn)步，它依然有著較好的應(yīng)用前景，值得人們對(duì)其進(jìn)行深入探討。目前大多數(shù)的程序驗(yàn)證過程是順序地按每一條驗(yàn)證規(guī)則進(jìn)行驗(yàn)證。由于驗(yàn)證過程中的并發(fā)構(gòu)造特性沒有被充分挖掘出

2、來，這種順序驗(yàn)證方法嚴(yán)重地制約了驗(yàn)證工作的效率，尤其在驗(yàn)證大型程序時(shí)愈發(fā)明顯。所以，從提高驗(yàn)證過程的并發(fā)度的角度來研究提高程序驗(yàn)證的效率一件很有意義的事。
　　 軟件行業(yè)是一個(gè)快速發(fā)展的行業(yè)，大量的新舊技術(shù)的交替造成了大規(guī)模的遺留系統(tǒng)。針對(duì)遺留系統(tǒng)的處理有兩種方法，要么設(shè)計(jì)新的系統(tǒng)去替換，要么對(duì)其進(jìn)行再工程。由于遺留系統(tǒng)存在技術(shù)陳舊、系統(tǒng)結(jié)構(gòu)混亂、文檔缺失和維護(hù)成本高等問題，越來越多的企業(yè)和組織采用新技術(shù)將遺留系統(tǒng)再工程到新的軟

3、件或硬件平臺(tái)，以提高系統(tǒng)的可靠性、可重用性、可維護(hù)性和運(yùn)行性能。任何先進(jìn)系統(tǒng)最終都成為遺留系統(tǒng)，所以良好的系統(tǒng)結(jié)構(gòu)設(shè)計(jì)方案和系統(tǒng)可擴(kuò)展性在再工程中將顯得越來越重要。早期系統(tǒng)大多數(shù)采用面向過程方法編程，而面向過程編程的特點(diǎn)是注重功能的實(shí)現(xiàn)，業(yè)務(wù)過程和系統(tǒng)的操作方法聯(lián)系的比較緊，不利于系統(tǒng)的維護(hù)和升級(jí)。所以把注重功能實(shí)現(xiàn)的面向過程系統(tǒng)轉(zhuǎn)換成注重結(jié)構(gòu)設(shè)計(jì)的面向?qū)ο笙到y(tǒng)，以期利用面向?qū)ο蟮奶卣鱽硖岣呦到y(tǒng)的可擴(kuò)展性的研究變得有意義了。
　　

4、 任何事物之間都是有聯(lián)系的，利用事物間的依賴關(guān)系開展有關(guān)理論與應(yīng)用研究既有普遍的現(xiàn)實(shí)意義，也有潛在的學(xué)術(shù)價(jià)值。為此本文把依賴分析應(yīng)用到了并行化程序驗(yàn)證策略和遺留系統(tǒng)改造中，主要完成了以下幾項(xiàng)工作：
　　 1.提出了一種提取While程序控制結(jié)構(gòu)的算法，用實(shí)驗(yàn)證明該算法的正確性，并對(duì)該算法做了簡要的分析。
　　 2.在獲取程序控制結(jié)構(gòu)依賴關(guān)系的基礎(chǔ)上，提出一種基于依賴分析的并行化驗(yàn)證策略，進(jìn)一步提高程序的驗(yàn)證效率，并用實(shí)