嵌入式系統驗證中的覆蓋率分析方法研究

《嵌入式系統驗證中的覆蓋率分析方法研究》是依託清華大學，由周旻擔任項目負責人的青年科學基金項目。

基本介紹

• 中文名：嵌入式系統驗證中的覆蓋率分析方法研究
• 依託單位：清華大學
• 項目負責人：周旻
• 項目類別：青年科學基金項目

項目摘要

動態驗證方法（測試和模擬仿真）是驗證系統功能正確性的主要方法。相比形式化驗證方法，動態驗證方法具有不完備性。為度量驗證過程的完成度，實踐中常使用各類覆蓋模型來描述系統中的關鍵覆蓋點，並且通過覆蓋率來度量其被覆蓋情況。但驗證的最終目的是確保系統無缺陷，覆蓋率和系統缺陷的關係一直是業界關注卻沒有完全解決的問題。已有研究中基於簡化的覆蓋模型和缺陷模型對缺陷覆蓋率進行了分析，但由於模型假設過於簡單，且分析方法沒有考慮到系統的時序性，因此很難用於實際驗證中。本課題擬對動態驗證中的覆蓋率分析展開深入研究，在考慮系統時序行為的前提下，對嵌入式系統進行自動抽象建模，得到帶機率的狀態變遷模型，再針對擴展的覆蓋模型和缺陷模型進行覆蓋率分析。本課題還研究嵌入式系統軟硬體協同驗證時的覆蓋率分析問題，並進行案例研究。課題研究成果可用於定量度量驗證指標以及度量系統可靠性，因此可用於指導驗證過程，並有助於提高驗證效率。

結題摘要

動態驗證方法（測試和模擬仿真）是當前軟硬體系統功能正確性驗證的主要方法。相比形式化驗證方法而言，動態驗證方法具有不完備性。實踐中經常使用各類覆蓋模型來度量驗證過程的完備程度。但驗證的最終目的是為了確保系統無缺陷，覆蓋率大小和系統潛在缺陷數量之間的關聯關係一直是業界關注卻沒有完全解決的問題，現有的缺陷覆蓋率分析方法中對覆蓋模型和缺陷模型的假設過於簡單，且分析方法沒有考慮到系統的時序性，因此很難用於實際驗證中。 本項目對動態驗證中的覆蓋率分析與提升方法展開深入研究，基於機率模型對系統中硬體模組的覆蓋率分析方法以及軟體模組的覆蓋率提升方法進行協同研究，提高系統動態測試中的分析精度與覆蓋度。 具體而言，本項目（1）設計了基於SMT可滿足度的覆蓋率分析支持技術，可用於構造帶機率的抽象遷移系統。（2）實現了基於機率變遷系統的覆蓋率分析，在考慮系統時序行為的前提下，對被驗證系統進行抽象建模，得到帶機率的狀態變遷模型，再針對擴展的覆蓋模型和缺陷模型進行覆蓋率分析，定量度量了系統可靠性與覆蓋率之間的關係。該方法有效解決了其他相關方法不考慮時序性所帶來的問題，可用於指導驗證過程，並有助於提高驗證效率。（3）研究了針對軟體單元測試的覆蓋率提升方法，該方法基於演化算法對單元測試覆蓋率進行自動提升，基於狀態空間邊界提升動態驗證中的缺陷覆蓋率。實驗證明該方法可有效提升缺陷覆蓋率。 本項目研究過程中，實現了3套嵌入式分析工具（分別針對軟體、硬體），在開源和實際系統中進行了套用驗證，發表高水平論文10篇（包括期刊論文5篇，會議論文5篇。有2篇論文分別發表在影響因子大於7、10的IEEE Transaction期刊上，此外還包含ASE等軟體工程頂級會議論文1篇，包含COMPSAC國際學術會議2016年唯一最佳論文，論文中有2篇被分類為CCF A類），申請軟體著作權1項，專利2項，培養碩士研究生2人。達到了項目立項目標。