空間通信片上網路數字系統形式化驗證與可靠性分析

《空間通信片上網路數字系統形式化驗證與可靠性分析》是依託首都師範大學，由李曉娟擔任項目負責人的面上項目。

基本介紹

• 中文名：空間通信片上網路數字系統形式化驗證與可靠性分析
• 項目類別：面上項目
• 項目負責人：李曉娟
• 依託單位：首都師範大學

項目摘要

空間通信片上網路系統(SpW)是空間設備數據通信的關鍵技術。對這類安全攸關套用的片上網路系統，僅採用傳統的模擬、測試方法無法滿足其正確性和可靠性驗證需求。本項目擬以SpW為用例,研究片上網路鏈路接口設計及通信協定的層次化形式建模、驗證及可靠性分析方法；探索片上網路軟硬體協同驗證, 實現嚴格的功能正確性驗證與量化性能分析的結合。面向數據流，直接基於硬體設計的結構進行形式建模，在保留其時序和功能細節信息的前提下，提高了抽象層次，有效避免以控制流為中心建模導致的狀態空間爆炸問題。抽象連線埠佇列的非確定屬性，建立Markov 模型進行性能分析。建立協定並發、隨機行為的高階邏輯模型, 提取關鍵屬性的邏輯表達函式，量化分析協定的可靠性。據此總結出從較低抽象層RTL 實現到較高抽象層傳輸協定的NOC 形式化建模、驗證方法。

結題摘要

對安全攸關套用的匯流排網路系統，僅採用傳統的模擬、測試方法無法滿足其正確性和可靠性驗證需求。本項目首先以SpW為用例,研究匯流排網路鏈路接口設計及通信協定的層次化形式建模、驗證及可靠性分析方法；並以此為基礎，提出較為通用的嵌入式系統網路接口的正確性和可靠性的層次化驗證和分析方法, 實現嚴格的功能正確性驗證與量化性能分析的結合。研究面向數據流的網路接口微體系結構的形式表達建模方法，建立了圖形化元件的形式表達庫，在保留其時序和功能細節信息的前提下，提高了抽象層次，有效避免以控制流為中心建模導致的狀態空間爆炸問題。基於圖形模型符號化庫，創建了面向片上網路驗證需求的xMAS模型庫，並且在已有元件基礎上，創建了一個可以描述數據流優先權的新xMAS元件，並在定理證明工具ACL2中進行形式表達和屬性的驗證，可實現運用ACL2對SPW及CAN匯流排等通信系統關鍵屬性正確性的自動驗證。基於馬爾科夫決策過程建立模型通信過程的模型，建立時間自動機模型對鏈路設計進行驗證和分析，獲得在不同信道質量情況下匯流排協定的工作性能；提取關鍵屬性的邏輯表達函式，量化分析協定的可靠性。據此總結出從較低抽象層RTL 實現到較高抽象層傳輸協定的嵌入式系統網路接口形式化建模、驗證方法，並將該方法用於機器人分散式控制的匯流排傳輸系統的設計和驗證。本項目研究層次化、模組化的SOC網路通信系統形式建模和自動驗證方法，為通信匯流排系統的設計人員進行驗證下的設計、避免設計階段的bug和系統可靠性保證及性能分析等方面提供了有效參考。