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

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

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

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

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