[發明專利]基于狀態空間搜索的控制器局域網協議驗證方法

有效

• 申請號: 201410116466.8
• 申請日: 2014-03-26
• 公開（公告）號: CN103888460B
• 公開（公告）日: 2017-09-12
• 發明（設計）人: 朱彥沛;陳志;高陽陽;高顯強;岳文靜
• 申請（專利權）人: 南京郵電大學
• 主分類號: H04L29/06
• 分類號: H04L29/06
• 代理公司: 南京經緯專利商標代理有限公司32200
• 代理人: 葉連生

1.一種基于狀態空間搜索的控制器局域網協議驗證方法，其特征在于該方法包括以下步驟：

1).系統建模

11)分析控制器局域網協議，列出協議所有常量和變量；

12)列出節點所有可能狀態，所述狀態是節點能夠穩定維持的抽象化表述，包含一個或多個參數變量；

13)列出每一可能狀態的參數變量，所述參數變量是指狀態包含的信息大小，信息內容，狀態生成時間，消息歷史，狀態環境變量；

14)列出節點各個狀態之間轉移條件，標注轉移過程中參量變化；

15)根據轉移條件，在各個狀態節點之間建立有向邊，建立狀態自動機模型；

16)用時序邏輯公式語言描述待驗證的模型的所有性質；

2).模型預處理

對狀態自動機模型中的狀態進行遍歷，如果一個狀態上沒有時鐘解釋，并且其前驅遷移或者后繼遷移都為空，則刪除此狀態，并對與此狀態有關的遷移進行合并；

3).模型性質檢驗

31)建立棧st，初始化為空，該棧用于存儲訪問狀態空間的訪問路徑；

311)根據控制器局域網協議內容構建功能函數h(s)，該函數用于分解狀態s并返回其關鍵部分S_rel，其中參數s為一個表示狀態的結構體，該結構體用于記錄一個狀態的各個屬性和遷移條件，h(s)通過分析當前驗證的時序邏輯，將與待驗證性質相關的狀態的屬性和遷移條件取出并生成新的狀態，稱為關鍵部分S_rel，并返回；

312)建立棧CE-stack，初始化為空，該棧用于保存已訪問狀態s的關鍵部分的路徑；

313)建立棧reached，初始化為空，該棧用于保存已訪問過的狀態的關鍵部分，相同的關鍵部分不重復存儲；

32)根據模型驗證性質初始化狀態S_I為系統的最初狀態；

33)將最初的狀態節點放進棧st，并將S_I標記為已訪問；

34)利用功能函數h(s)分解并得到當前訪問狀態的關鍵部分S_rel，將S_rel壓進棧CE-stack；

35)判斷st是否為空，若st為空，則滿足驗證性質，結束驗證；若st不為空，則取出棧頂元素s，根據狀態轉移條件，利用局部偏序簡化算法生成s的臨時頑固集t，當頑固集t不為空則轉向步驟36)，當頑固集t為空則轉向步驟37)；所述局部偏序簡化算法是指在模型檢測并發執行的不同進程動作的不同次序中，將局部狀態的次序固定，減少重復驗證本質上相同的路徑，所述頑固集是指當前狀態必須執行的轉移條件的集合；

36)判斷頑固集t是否為空，若為空則轉向步驟35)，否則，任意取t中的一個轉移條件，并將其從t中刪除，根據此轉移條件得到狀態s’，利用h(s’)得到s’的關鍵部分S_rel，將S_rel壓入棧CE-stack中；

361)判斷S_rel是否在reached中，若不在則將其壓入reached中；

362)判斷在s’上可使用的狀態轉移個數T是否大于1，如果大于1，則將s’放進棧st中，否則可知在以后的搜索過程中不會在s’上進行回溯，不需要放進st中；

363)判斷當前待驗證性質f是否符合當前狀態s’；

3631)如果不滿足，那么狀態空間搜索停止，立即返回當前出錯的狀態s’和CE-stack，其中CE-stack存儲的是當前從初始狀態S_I到不滿足條件的狀態s’的一條路徑，并轉步驟37)；

3632)如果滿足，那么轉步驟36)；

37)根據狀態搜索結果進行分析，將根據以上過程進行模型檢驗的最終結果展示出來，如果滿足驗證性質則告知用戶滿足的性質，反之則返回不滿足的性質，并提供不滿足性質的反例，將不滿足性質的完整路徑顯示出來以供用戶調試糾錯。