一種用於高可靠通信系統驗證與性能分析的形式化方法
2023-11-07 07:19:07 3
專利名稱：一種用於高可靠通信系統驗證與性能分析的形式化方法
技術領域：
本發明涉及一種用於高可靠通信系統驗證與性能分析的形式化方法，它是嵌入式系統通信的可靠性驗證(Reliability, Maintainability and Supportability,簡稱 RMS)與性能分析的一體化實現方法，特別是基於形式化方法的驗證與系統量化性能分析一體化流程構建方法，屬於形式化驗證工程應用技術領域。
背景技術：
許多關鍵應用的片上系統中通信系統通常具有極高的功能可靠性、嚴格的實時性等要求。關鍵應用的片上系統失效導致生命與財產重大損失的例子枚不勝舉；片上系統傳統的檢驗方法是測試或故障模擬，其主要局限性在於對給定數據集通過了測試，但不能保證在實際運行中對其它輸入不發生錯誤；並且難以發現系統潛在的不合理設計或隱含錯誤。如何保證系統同時滿足給定的功能和非功能需求一直是高可靠片上計算領域中研究的關鍵問題之一。基於形式化的方法對通信系統正確性進行驗證和性能分析將對保證片上通信系統正確性與可靠性具有重要意義。面向片上系統實現數據傳輸或並發、分布式過程的廣泛應用，而這些應用的功能屬性的形式化驗證通常都採用模型檢驗的方法，但是由於模型檢驗方法抽象層次較低，只 能進行定性檢驗，如果抽象不當或協議較複雜，很容易導致狀態過多，甚至狀態爆炸的問題。目前對網絡通信系統的形式化方法只驗證其正確性，要是實現量化分析，則通過建立模擬模型進行。
發明內容
1、目的本發明的目的是提供一種用於高可靠通信系統驗證與性能分析的形式化方法，它是一種基於模型檢驗和定理證明相結合的通信系統形式化驗證與分析的方法。擬基於假設保證的方法，建立環境狀態機，對網絡通信系統的設計進行層次化建模，對關鍵屬性進行形式化驗證，對協議的傳輸過程、屬性的高階邏輯形式化建模方法、設計實現隨機變量統計特徵的高階邏輯形式化，並基於在H0L4所建立的高階邏輯模型和相關定理，實現自動驗證和基於形式模型的量化動態性能分析。2、技術方案為了實現上述目的，本發明一種用於高可靠通信系統驗證與性能分析的形式化方法，該方法具體步驟如下步驟一分析通信系統SOC功能實現結構，並提取關鍵的功能模塊；進行驗證模塊分解、建模。將高階邏輯定理證明和符號模型檢驗相結合，進行組合形式化驗證。步驟二 對模塊之間的接口屬性、I/O 口及物理層功能實現，用模型檢驗的方法進行形式化驗證，基於符號化模型檢驗平臺，分層次地用模型檢驗方法驗證模塊之間的接口屬性、I/o 口及物理層功能實現。步驟三針對複雜功能模塊可能導致狀態過多的問題，進行層次化抽象，基於假設一保證理論，建立環境狀態機模型，進行組合驗證策略。步驟四用定理證明的方法對數據通信協議、並行應用進程進行邏輯、功能實現的驗證。基於高階邏輯對片上系統時態屬性和隨機行為進行形式化表達；步驟五在系統的邏輯分析表達式分析中，提取系統進程統計性質的數學邏輯形式表達函數，實現驗證對象過程的動態量化性能分析。其中，步驟一中所述的「提取關鍵的功能I旲塊；進行驗證I旲塊分解、建I旲；將聞階邏輯定理證明和符號模型檢查相結合，進行組合形式化驗證；」其具體實現過程如下對通信系統中的發送、接收、鏈路管理、差錯控制、流量控制等模塊進行提取，進行驗證模塊的劃分，對照協議設計規範，提取出驗證的目標和子目標。功能較為獨立的模塊抽象為單獨驗證組件，再將低耦合模塊間接口進行抽象建模及狀態描述；建立發送/接收控制器的狀態機模型，形成系統設計的形式化模型，採用模型檢驗的方法進行驗證。對數據傳輸協議及並行的分布式組件等過程在H0L4平臺上，建立高階邏輯模型，採用定理證明的方法進行驗證。其中，步驟三中所述的「進行層次化抽象，基於假設一保證理論，建立環境狀態機模型，進行組合驗證策略；」其具體實現過程如下對於多個模塊級聯耦合成的複雜功能屬性進行驗證時所產生的狀態過多的問題，採用假設保證推理的方法，抽象環境狀態機，對整個系統進行分層次的驗證。假設保證推理過程如下如果兩個子系統S1、S2具有屬性(I) SI滿足性質Pl (2)當S2的環境滿足性質Pl時，S2滿足性質P2。那么子系統SI和S2的組合SI | | S2滿足性質P2。用這種方法進行驗證的優點在於不用對SI和S2的組合建立狀態機進行驗證，只需用S2驗證P1，然後把假設Pl抽象為S2的環境來驗證P2。假設Pl和SI相比，狀態空間少了很多，有利於處理大規模的電路系統。本發明通過以上步驟，給出了一種將模型檢驗和定理證明兩種形式化方法相結合的通信系統形式化驗證與性能分析的方法，同時給出較為通用的通信系統形式化驗證所對應的流程方法。3、優點及功效本發明的主要優點是提供一種SOC的通信系統在不同抽象級別下層次化的形式化 驗證方法，並實現系統並發屬性的性能分析。實現較為通用的SOC的通信系統功能正確性和可靠性分析的自動驗證技術，便於SOC的設計者能在早期發現系統設計階段的漏洞或邏輯錯誤。
圖1基於模型檢驗和定理證明相結合的通信系統形式化驗證與分析的方法實現整體2為本發明的流程框3為典型SOC系統模型檢驗驗證實施流程模板圖4為典型SOC系統的高階邏輯定理證明的流程模板圖5為發送控制模塊狀態轉移圖
具體實施例方式為使本發明的特徵及優點得到更清楚的了解，以下結合附圖，作詳細說明如下圖1描述了本發明實現的整體架構。SOC設計人員對所設計或實現的片上通信系統進行行為、功能正確性驗證時，本發明的一種形式化驗證方法可以實現系統在不同抽象層次的屬性驗證並基於所建立的形式化模型，進行性能分析見圖2，本發明一種用於高可靠通信系統性能檢驗與分析的形式化驗證方法，其具體實施步驟是步驟一分析系統設計，進行驗證分解。如圖2所示，根據系統功能、實現特點，進行驗證任務的分解。(I)詳細分析各關鍵模塊或進程的屬性、功能描述及其實現，提取出驗證的目標和子目標，(2)進行系統功能模塊的劃分及其驗證屬性的抽象，將功能較為獨立的模塊抽象為單獨驗證組件，再將低耦合模塊間接口進行抽象建模及狀態描述，建立抽象狀態機。(3)對數據傳輸協議及並行的分布式組件等過程建立高階邏輯模型，採用定理證明的方法進行驗證，(4)對於功能較為獨立的組件和低耦合模塊間接口，本項目擬採用模型檢驗的方法進行驗證。步驟二 對模塊之間的接口屬性、I/O 口及物理層功能實現，用模型檢驗的方法進行形式化驗證，基於符號模型檢驗平臺，分層次地用模型檢驗方法驗證模塊之間的接口屬性、I/O 口及物理層功能實現。模型檢驗的過程包括建模、性質的描述和自動驗證三個過程，如圖3所示，對驗證對象模塊的系統實現進行抽象和形式化表達，使用5元組的Kripke結構表示系統的有限狀態空間；用計算樹時態邏輯(CTL)描述系統期望的屬性，這個過程需要描述準確、避免二義性。利用符號模型檢驗工具SMV(Symbolic Modeling Verifier)自動窮舉證明期望的屬性是否在狀態空間上成立，如果成立，則說明設計實現滿足期望的屬性。如果不成立，則輸出 反例，可以再根據仿真測試，定位錯誤。這可以是一個驗證一報錯—錯誤信息分析和模型修改一再驗證的循環過程。例如圖5中，發送器在重置狀態下處於等待狀態，(I)如果來自主機系統的Tick_IN (請求發送時間碼)信號為高，並且已經發送了 ESC信號(即ESC_Gone_internal信號為高)，則發送器會到達鎖定時間碼狀態(在此狀態下ProvidejimeCode置為1，傳送給發送寄存器子模塊)，然後無條件的到達發送時間碼狀態.(2)如果Send_FCT (來自控制模塊)為I並且EightMore=I (說明接收器有多於8個的空間來存儲數據)並且 ESC_Gone_internal=0 (如果 ESC_Gone_internal=l,則 ESC+FCT為一個空字符)，那麼發送器會到達鎖定流控制標誌狀態(在此狀態下Provide_FCT置為1，傳送給發送寄存器子模塊)，然後無條件的到達發送常字符狀態。(3)如果SencLNULL (來自控制模塊)=1並且ESC_Gone_internal=l,那麼發送器會到達鎖定流控制標誌狀態(在此狀態下Provide_FCT置為I,傳送給發送寄存器子模塊)。(4)如果Send_All (來自控制模塊)=1並且NoCredit=O,那麼發送器會到達鎖定流控制標誌狀態，(在此狀態下Provide_ESC置為1，傳送給發送寄存器子模塊)。(5)如果Send_EEP=l，那麼發送器會到達鎖定錯誤包結束標誌狀態，(在此狀態下Provide_EEP置為1，傳送給發送寄存器子模塊)。(6)如果Send_E0P=1，那麼發送器會到達鎖定正確包結束標誌狀態，(在此狀態下Provide_E0P置為1，傳送給發送寄存器子模塊)。(7)如果Send_NChar_Flag=l，那麼發送器會到達鎖定常字符狀態，(在此狀態下Provide_NChar置為I,傳送給發送寄存器子模塊)。圖中一些主要輸入變量的含義
權利要求
1.一種用於高可靠通信系統驗證與性能分析的形式化方法，其特徵在於該方法具體步驟如下步驟一分析通信系統SOC功能實現結構，並提取關鍵的功能模塊，進行驗證模塊分解、建模，將高階邏輯定理證明和符號模型檢驗相結合，進行組合形式化驗證；步驟二 對模塊之間的接口屬性、I/o 口及物理層功能實現，用模型檢驗的方法進行形式化驗證，基於符號化模型檢驗平臺，分層次地用模型檢驗方法驗證模塊之間的接口屬性、I/o 口及物理層功能實現；步驟三針對複雜功能模塊可能導致狀態過多的問題，進行層次化抽象，基於假設一保證理論，建立環境狀態機模型，進行組合驗證策略；步驟四用定理證明的方法對數據通信協議、並行應用進程進行邏輯、功能實現的驗證；基於高階邏輯對片上系統時態屬性和隨機行為進行形式化表達；步驟五在系統的邏輯分析表達式分析中，提取系統進程統計性質的數學邏輯形式表達函數，實現驗證對象過程的動態量化性能分析。
2.根據權利要求1所述的一種用於高可靠通信系統驗證與性能分析的形式化方法，其特徵在於步驟一中所述的「提取關鍵的功能模塊，進行驗證模塊分解、建模，將高階邏輯定理證明和符號模型檢查相結合，進行組合形式化驗證；」其具體實現過程如下對通信系統中的發送、接收、鏈路管理、差錯控制、流量控制模塊進行提取，進行驗證模塊的劃分，對照協議設計規範，提取出驗證的目標和子目標；功能較為獨立的模塊抽象為單獨驗證組件，再將低耦合模塊間接口進行抽象建模及狀態描述；建立發送/接收控制器的狀態機模型，形成系統設計的形式化模型，採用模型檢驗的方法進行驗證；對數據傳輸協議及並行的分布式組件過程在H0L4平臺上，建立高階邏輯模型，採用定理證明的方法進行驗證。
3.根據權利要求1所述的一種用於高可靠通信系統驗證與性能分析的形式化方法，其特徵在於步驟三中所述的「進行層次化抽象，基於假設一保證理論，建立環境狀態機模型，進行組合驗證策略；」其具體實現過程如下對於多個模塊級聯耦合成的複雜功能屬性進行驗證時所產生的狀態過多的問題，採用假設保證推理的方法，抽象環境狀態機，對整個系統進行分層次的驗證；假設保證推理過程如下如果兩個子系統S1、S2具有屬性(I) SI滿足性質Pl ; (2)當S2的環境滿足性質Pl時，S2滿足性質P2 ;那么子系統SI和S2的組合SI I I S2滿足性質P2 ;用這種方法進行驗證的優點在於不用對SI和S2的組合建立狀態機進行驗證，只需用S2驗證P1，然後把假設Pl抽象為S2的環境來驗證P2 ;假設Pl和SI相比，狀態空間少了很多，有利於處理大規模的電路系統。
全文摘要
一種用於高可靠通信系統驗證與性能分析的形式化方法，該方法有五大步驟。本發明是一種基於模型檢驗和定理證明相結合的通信系統形式化驗證與分析的方法。擬基於假設保證的方法，建立環境狀態機，對網絡通信系統的設計進行層次化建模，對關鍵屬性進行形式化驗證，對協議的傳輸過程、屬性的高階邏輯形式化建模方法、設計實現隨機變量統計特徵的高階邏輯形式化，並基於在HOL4所建立的高階邏輯模型和相關定理，實現自動驗證和基於形式模型的量化動態性能分析。它在形式化驗證工程應用技術領域裡具有較好的實用價值和廣闊的應用前景。
文檔編號H04L12/24GK103036739SQ20121053363
公開日2013年4月10日 申請日期2012年12月11日 優先權日2012年12月11日
發明者李曉娟, 關永, 施智平, 王瑞, 張 傑, 趙春娜, 華偉, 董玲玲 申請人:首都師範大學