《基於模型檢驗的測試用例生成方法研究》是依託上海大學，由曾紅衛擔任項目負責人的面上項目。
基本介紹
- 中文名：基於模型檢驗的測試用例生成方法研究
- 項目類別：面上項目
- 項目負責人：曾紅衛
- 依託單位：上海大學
中文摘要,結題摘要,
中文摘要
軟體產品複雜度的不斷增加和發布期的縮短給軟體測試帶來了嚴重的挑戰，軟體測試自動化是一種必然趨勢。主要探索用模型檢驗的反例生成能力實現軟體測試自動化的原理和關鍵問題；研究通用測試覆蓋準則在基於模型檢驗的測試中的可套用性以及從測試覆蓋準則自動生成陷阱性質的方法，通過模型檢驗陷阱性質產生的反例構造測試用例；研究不確定性模型帶來的測試用例可控性問題，提出可控性問題解決方法；研究從安全性質產生測試用例的方法；結合組合推理原理和抽象精化框架，研究測試用例生成的抽象精化方法；研究集測試目標縮減、測試用例生成過程監控和測試包縮減於一體的測試最佳化方法；開發基於模型檢驗的測試用例生成工具，建立基於模型檢驗的測試自動化框架。基於模型檢驗的測試支持測試自動化，支持軟體開發與測試的並行化。項目研究在學術上對軟體測試方法、軟體質量保證、軟體過程改進和維護有重大意義，研究成果可以廣泛套用到軟體產品的開發過程。
結題摘要
軟體產品複雜度的不斷增加和發布期的縮短給軟體測試帶來了嚴重的挑戰，軟體測試自動化是一種必然趨勢。主要探索用模型檢驗的反例生成能力實現軟體測試自動化的原理和關鍵技術。 提出了產生數據流覆蓋和狀態圖覆蓋準則（狀態覆蓋、遷移覆蓋和遷移對覆蓋）的時態性質的形式化方法，給出了提取時態性質的方法；基於危險跡概念，提出了安全性質測試的建模方法和基於圖結構覆蓋的安全性質測試準則；結合反例引導的抽象精化框架和組合驗證方法，組合抽象構件產生構件組合的抽象模型，從抽象模型生成抽象測試用例，利用反例引導的抽象精化框架產生具體的測試用例。提出了構件組合的測試生成抽象精化方法；利用測試目標排序、時態邏輯公式重寫等技術，提出了一種基於模型檢驗的測試生成過程的on-the-fly監控最佳化方法，實現測試目標和測試包的動態約簡，降低測試冗餘；基於FSM模型的測試方法及其相關理論，提出測試序列集合冗餘約簡方法、FSM測試的評估量化指標、以及最小測試成本遷移覆蓋準則和準則的充分必要條件，設計了最小測試成本遷移覆蓋的實現算法，對若干基於FSM模型的測試方法進行了實驗評估；在軟體特別是對Web套用和Web服務的形式建模和驗證方面進行了重點研究，除了定性檢驗，還關注定量驗證。使用機率對現有的形式模型如Petri網進行擴展，定義了其代數語義和邏輯語義，開發了非確定機率系統的建模、分析、模擬和驗證技術。 開發了基於模型檢驗器NuSMV的測試生成算法，建立了一個基於模型檢驗的測試生成自動化框架。框架集成了NuSMV、UML建模工具ArgoUML、以及從FSM到NuSMV程式的自動化轉化工具、性質輔助描述工具和反例解析工具等；開發了一個集模型轉換器、測試目標分析器、測試序列生成器、以及測試執行引擎等功能的基於FSM的測試工具原型；提出了基於SOA的模型檢驗工具集成體系結構，無需本地安裝和配置模型檢驗工具，實現了模型檢驗的遠程透明訪問。 基於模型檢驗的測試支持測試自動化，支持軟體開發與測試的並行化。研究成果可以廣泛套用到軟體產品的開發過程。
