基於高階規約定向測試的異構系統驗證研究

《基於高階規約定向測試的異構系統驗證研究》是依託華東師範大學，由陳銘松擔任項目負責人的青年科學基金項目。

基本介紹

• 中文名：基於高階規約定向測試的異構系統驗證研究
• 項目類別：青年科學基金項目
• 項目負責人：陳銘松
• 依託單位：華東師範大學

項目摘要

隨著體系結構從單核模式到異構多核模式，處理對象從簡單控制系統到異構信息物理融合系統的漸進演化，嵌入式系設計的複雜性越來越高。大量的時間與資源被消耗在系統功能驗證上，在時間與效率方面功能驗證已經成為了系統設計的主要瓶頸。本項目將基於系統設計高階規約，研究如何提高自頂向下設計流程各個測試驗證環節的效率，有效降低異構系統驗證的複雜性。研究內容主要包括：1、研究異構系統高階規約的形式化建模與模型自動抽取方法，提高對系統基本功能特徵的描述與自動化分析能力；2、研究基於高階規約的自動化測試用例生成的最佳化方法，提高異構系統設計與開發的效率；3、研究如何提高異構系統自頂向下設計過程中各階段驗證結果的重用技術，確保系統從系統高階規約到具體實現逐步精化過程中的一致性與正確性。從而提高系統的整體驗證效率。在縮短嵌入式產品開發周期的同時，保證系統高可靠性。

結題摘要

隨著體系結構從單核模式到異構多核模式，處理對象從簡單控制系統到異構信息物理融合系統的漸進演化，嵌入式系統設計的複雜性越來越高。大量的時間與資源被消耗在系統可信構造上，在時間與效率方面可信構造已經成為了系統設計的主要瓶頸。本項目基於系統設計高階規約，研究如何提高自頂向下嵌入式設計流程中各個環節的效率，有效降低異構系統可信構造的複雜性。本項目主要研究內容與貢獻如下: 1、不確定環境下異構系統高階規約的形式化建模與自動分析方法。基於統計模型檢驗技術，創新地提出了不確定環境下異構嵌入式系統性能的建模與定量評估框架，支持不確定環境下異構嵌入式設計的自動評估、比較與最佳化，該框架已在多個領域如異構多核片上系統、雲計算與智慧型建築方面得以套用。 2、基於高階規約的自動化測試用例生成的最佳化方法。基於有界模型檢驗（Bounded Model Checking），創新地提出了一種高效的基於屬性時空分解與決策序列學習的自動化測試用例生成技術， 能有效降低測試用例的總體時間，加速比可達5-10倍。 3、資源受限情況下異構高階規約的高效綜合方法。基於目前已有的分支界定方法，系統地提出了多種搜尋空間約減方法來快速獲取最優設計；創新地提出了基於結構的狀態空間約減方法，支持除上下界比較之外新的搜尋空間約減；提出了一種有效的兩階段搜尋方法，支持最緊初始搜尋空間的獲取；提出了一種基於狀態空間劃分與上界投機的搜尋方法，支持多搜尋任務間的協同並行搜尋快速獲得最優解。實驗結果顯示，我們提出的方法比現有最好的分支界定方法快10-1000倍。 4、基於高階規約驗證結果重用的多抽象層次一致性檢測方法。創新地提出了一種基於斷言與測試用例重用的頂層設計與底層實現的一致性檢測方法，支持自動化的將頂層規約的斷言與測試用例轉化為底層實現的斷言與測試用例，通過軌跡比較確保系統從系統高階規約到具體實現逐步精化過程中的一致性與正確性。 本項目的研究保證了在不確定環境下系統級設計的性能，大幅度降低了頂層設計到底層實現間的綜合時間，提高了系統的整體測試與驗證的效率，並提供了一套自動檢測頂層設計與底層實現間功能一致的方法。我們的研究能夠在縮短嵌入式產品開發周期的同時，保證系統高可靠性。