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

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

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

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

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