[發明專利]一種機器人關節通信系統模型的驗證方法及系統

有效

• 申請號: 201711427979.0
• 申請日: 2017-12-26
• 公開（公告）號: CN108199940B
• 公開（公告）日: 2021-07-20
• 發明（設計）人: 李曉娟;關永;孟瑤;王瑞;施智平;張倩穎;談金東;邵振洲;張杰;王國輝;劉永梅;吳敏華
• 申請（專利權）人: 首都師范大學
• 主分類號: H04L12/40
• 分類號: H04L12/40;H04L12/26;H04L12/24
• 代理公司: 北京安博達知識產權代理有限公司 11271
• 代理人: 徐國文

本發明涉及一種機器人關節通信系統模型的驗證方法及系統，所述方法包括：采用形式化方法對基于CAN現場總線型控制系統進行建模分析，其中需要對系統進行模型抽象，再進行形式建模與驗證，判斷時間自動機是否滿足正確性和實時性，若不滿足正確性則對系統方案重新規劃，若不滿足實時性，則通過部署動態優先級策略提升實時性，本發明提供的技術方案，采用形式化描述的方式建立時間自動機模型并在UPPAAL工具中驗證時間自動機的正確性與實時性，若不滿足實時性約束條件則部署動態優先級策略。

技術領域

本發明涉及機器人通信領域，具體涉及一種機器人關節通信系統模型的驗證方法及系統。

背景技術

機器人應用領域越來越廣泛，已經不僅僅局限于工業，由于市場的需求，大量服務型機器人開始應用于醫療和家庭。由于機器人通信系統的復雜性、高并發性和對實時性的高要求性，保證機器人精確和實時的完成預期動作非常重要，特別是在機器人分布式節點間的信息傳輸中，通信時延必須滿足規定響應時間的需求，否則將影響系統的穩定性或導致系統出錯、奔潰。

CAN總線協議規范中用信息靜態優先級策略進行通信，可以基本保證實時性，但是隨著CAN總線上節點的增多和對實時性要求的提高，靜態優先級策略不能滿足節點間傳輸的時延需求。

目前對CAN總線協議的驗證主要集中在電動汽車的控制系統中，在這些對CAN協議的驗證方法中主要采用的是傳統的測試、模擬和仿真的方法，然而這三種方法都有一定的局限性，不能覆蓋所有的執行路徑，所以會導致驗證結果不完善。傳統的測試方法是在設計的最后階段借助實體機搭建測試平臺進行參數設定和測試，這種方法需要在最后階段才能進行，并且測試過程中參數的設定有限，導致測試結果不精確。傳統的模擬和仿真方法主要是利用計算機軟件進行環境模擬個動作仿真，進而進行通信分析，但是這種方法依賴硬件，提供的參數設置也有限，同樣會導致驗證結果不完善。

發明內容

本發明提供一種機器人關節通信系統模型的驗證方法及系統，其目的是為了在設計初期保證系統設計的完善性，避免設計階段的漏洞，嚴謹且系統的驗證并分析CAN總線在機器人通信中的正確性和實時性，提高基于CAN總線的機器人關節系統通信的正確與實時性。

本發明的目的是采用下述技術方案實現的：

一種機器人關節通信系統的建模與驗證的方法，其改進之處在于，包括：

判斷機器人關節通信系統中的通信節點的時間自動機模型是否滿足正確性約束；

若不滿足正確性約束，則重新構建機器人關節通信系統中通信節點的時間自動機模型；

若滿足正確性約束，則判斷通信節點的時間自動機模型是否滿足實時性約束；

若滿足實時性約束，則結束操作；

若不滿足實時性約束，則將該通信節點的數據幀傳輸原優先級修正為最高優先級,所述該通信節點的數據幀傳輸完畢后，將該通信節點的數據幀傳輸的優先級恢復為該通信節點的數據幀傳輸的所述原優先級；

所述通信節點利用CAN總線傳輸數據幀。

優選的，所述重新構建機器人關節通信系統中通信節點的時間自動機模型，包括：

根據機器人節點通信系統中通信節點的運行狀態，利用UPPAAL工具構建機器人節點通信系統中通信節點的時間自動機模型。

優選的，所述判斷機器人關節系統的中通信節點的時間自動機模型是否滿足正確性約束，包括：

當利用UPPAAL工具檢測所述通信節點的時間自動機模型滿足所有約束指標時，則所述時間自動機模型滿足正確性約束；否則，不滿足正確性約束；