基于集成測試技術(shù)的SOFL形式化規(guī)格說明驗證.pdf

1、形式化方法目前在工業(yè)界還沒有得到廣泛應(yīng)用，主要是因為各種形式化方法沒有很好地整合到工業(yè)界的軟件開發(fā)過程中去，并且目前還沒有比較成熟的形式化工具可以對軟件開發(fā)提供令人滿意的支持。在這個背景下，SOFL作為一種更貼近工業(yè)界軟件開發(fā)需要的形式化工程方法被提出來。它結(jié)合了傳統(tǒng)的形式化方法以及結(jié)構(gòu)化方法和面向?qū)ο蠓椒?。SOFL集成了數(shù)據(jù)流圖、Petri網(wǎng)絡(luò)以及VDM形式化規(guī)格說明語言，形成了一套全新的形式化方法。 形式驗證是形式化方法的一

2、個重要組成部分。形式驗證主要分為定理證明、模型檢測和形式化測試三種方法。SOFL的形式驗證主要采用測試的方法，分為單元測試和集成測試。本文主要討論SOFL理論中的集成測試?yán)碚?。包括以下幾個主要方面： ①針對數(shù)據(jù)流圖內(nèi)各元素之間的一致性測試，研究如何統(tǒng)一Proof Obligation的生成策略。我們在文章中給出了一種通過分類和簡化CDFD圖形結(jié)構(gòu)的方式來構(gòu)筑統(tǒng)一的Proof Obligation生成策略。 ②探索如何有效

3、地完成數(shù)據(jù)流圖之間的一致性測試。CDFD的圖形結(jié)構(gòu)和圖形元素非常復(fù)雜，我們很難找到一個統(tǒng)一的算法來生成CDFD間一致性測試的Proof Obligation。本文提出了通過一種實現(xiàn)形式驗證的方法：通過輸入CDFD的輸入數(shù)據(jù)計算CDFD輸出數(shù)據(jù)，根據(jù)對輸出數(shù)據(jù)的分析進(jìn)行驗證。 ③結(jié)合SOFL的測試策略，研究如何引導(dǎo)用戶進(jìn)行對形式化規(guī)格說明的集成測試。針對這一問題，本文提出了分層引導(dǎo)測試的測試模式。使用分層引導(dǎo)測試，用戶可以在工具的

4、配合下充分遍歷SOFL形式化規(guī)格說明測試的所有測試標(biāo)準(zhǔn)，從而提高SOFL形式驗證的檢錯效率。 作為整個SOFL形式化方法支撐工具的一部分，本文還簡要介紹了當(dāng)前SOFL集成測試工具的開發(fā)情況。目前，工具的開發(fā)還處在原型階段，還有大量的理論問題急待解決。為繼續(xù)當(dāng)前的理論研究和工具開發(fā)，還需要解決以下幾個主要內(nèi)容： （1）進(jìn)一步深化數(shù)據(jù)流圖一致性測試的相關(guān)研究，并最終完善快速、便捷的Proof Obligation的生成算法。