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

有效

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

技術領域

本發明涉及一種在控制器局域網協議模型檢驗中進行狀態空間搜索的優化方法，主要利用基于狀態分解的狀態空間搜索算法在緩解狀態空間爆炸問題的情況下實現對控制器局域網協議進行驗證，屬于計算機技術、無線通信、傳感器技術和軟件驗證技術交叉技術應用領域。

背景技術

控制器局域網(CAN，Controller Area Network)是國際標準化的串行通信協議，屬于現場總線的范疇，是一種有效支持分布式控制系統的串行通信網絡。在當前汽車產業中，基于安全性、方便性、舒適性、成本的要求，研究人員開發出了許多類型的電子控制系統。這些系統之間的通信對數據類型、可靠性要求各不相同。由于在電子控制系統中多條總線構成情況增加，通信線束的數量也隨著增加。為了解決現代汽車中龐大的電子控制系統中的通信效率，減少不斷增加的信號線，1986年德國電器商博世公司開發出面向汽車的CAN總線協議。此后，CAN總線協議通過ISO11898及ISO11519進行了標準化，該協議在歐洲已成為汽車網絡的標準協議。由于CAN總線協議高性能、高可靠性以及獨特的設計，該協議越來越受到人們的重視，被廣泛應用于諸多領域。CAN總線協議能夠檢測出所產生的錯誤，當信號傳輸距離達到10km時，該協議仍可提供高達50kbit/s的數據傳輸速率。由于CAN總線協議具有很高的實時性能和應用范圍，從位速率最高可達1Mbps的高速網絡到低成本多線路的50Kbps網絡都可以任意搭配。因此，CAN總線協議己經在汽車業、航空業、工業控制、安全防護等領域中得到了廣泛應用。

隨著CAN總線協議在各個行業和領域的廣泛應用，對它的通信格式標準化也提出了更嚴格的要求。1991年CAN總線技術規范(Version2.0)制定并發布。該技術規范共包括A和B兩個部分，其中2.0A給出了CAN報文標準格式，而2.0B給出了標準的和擴展的兩種格式。美國的汽車工程學會SAE在2000年提出了J1939協議，此后該協議成為了貨車和客車中控制器局域網的通用標準。

模型檢驗是對有窮狀態系統的一種形式化確認方法，主要通過顯式狀態搜索或隱式不動點計算來驗證有窮狀態并發系統的模態/命題性質，該方法實質是利用計算機的快速計算能力，通過窮舉被檢驗系統的狀態空間中的每一個狀態來驗證該系統滿足特定的形式描述。模型檢驗的基本思想是用狀態遷移系統(S)表示系統的行為，用模態/時序邏輯公式(F)描述系統的性質，這樣“系統是否滿足所期望的性質”就轉化為數學問題“狀態遷移系統S是否公式F的一個模型”，用公式表示為S|＝F？。對有窮狀態系統，這個問題是可判定的，即可以用計算機程序在有限時間內自動確定。模型檢驗已被應用于計算機硬件、通信協議、控制系統、安全認證協議等方面的分析與驗證中，取得了令人矚目的成功，并從學術界輻射到了產業界。模型檢驗其基本原理實現為系統建立形式化模型，闡述所要驗證的性質，然后用算法去檢驗該模型是否滿足所述性質。模型檢驗提供一個完整的系統屬性驗證框架，模型檢驗的優點是模型檢驗能達到完全自動化的程度，只需用有窮狀態模型和邏輯公式分別將系統實現和待驗證的系統規范描述出來，之后的判斷過程則完全可以由模型檢驗工具自動完成，不需要人的參與；模型檢驗過程總會以“是”或“否”的結果中止，當以“否”的結果中止時，說明設計或系統不滿足某個給定的性質。此時一個違反性質的行為反例將會被給出，此反例將對理解錯誤的真正原因和修正錯誤提供線索。由于模型檢驗技術有以上優點，利用它對無線傳感器網絡進行同步機制的檢驗，在其設計階段盡可能的找出錯誤。