[發明專利]一種ROS底層通訊機制的形式化建模與驗證方法

有效

• 申請號: 202110365733.5
• 申請日: 2021-04-06
• 公開（公告）號: CN113127344B
• 公開（公告）日: 2023-06-09
• 發明（設計）人: 郭建;王子健;孫正旺
• 申請（專利權）人: 華東師范大學
• 主分類號: G06F11/36
• 分類號: G06F11/36
• 代理公司: 上海德禾翰通律師事務所 31319
• 代理人: 夏思秋

本發明公開了一種ROS底層通訊機制的形式化建模與驗證方法，首先根據ROS的開源代碼，提取出來ROS底層通訊機制的模塊、功能和規則；建立其關于底層主題通信機制的形式化模型；根據“發布/訂閱”通訊機制，提取出關鍵性質，用時態邏輯語言來描述性質；設計ROS應用實例，使用形式化驗證工具，通過結合應用實例和所建立的形式化模型，對時態邏輯語言描述的關鍵性質進行驗證；根據驗證結果和過程，對ROS的“發布/訂閱”通訊機制進行分析。本發明應用到包含了三個互相訂閱的節點的ROS具體實現，通過形式化驗證，來提高ROS及ROS應用實現的無死鎖性、可達性、活性與正確性。

技術領域

本發明屬于機器人操作系統(ROS)技術領域，具體涉及一種ROS底層通訊機制的形式化建模與驗證方法。

背景技術

機器人技術極大的豐富便利了我們的生活，隨著軟硬件技術的發展，家居、環保、工業生產、醫療保健以及軍事活動等領域都越來越依賴機器人技術，另一方面，隨著機器人技術在各行各業的蓬勃發展，和人類之間的交互越來越頻繁，一旦機器人出現錯誤，極有可能會導致災難性的后果。這就要求機器人系統對于各個節點間通信的安全性與可靠性有著極高的要求。近些年來，機器人操作系統(ROS)受到了工業界與學術界的廣泛高度關注，成為機器人應用程序開發的流行框架。

機器人操作系統(ROS)是一種開源的操作系統中間件，用來在統一的編程過程中開發機器人軟件。ROS為分布式計算集群提供了一個結構化的通信層。在ROS的支持下，不同的機器人功能模塊可以單獨設計，作為ROS的節點進行運行。多個ROS節點可以實現基于TCP/IP的點對點通信，這些節點可以分布式地運行在通過網絡連接的多臺計算機上，同時ROS通信也是語言獨立的，主節點負責存儲所有節點的主題和服務信息，這是兩種通信機制，主題通信是基于發布訂閱機制，是異步的通信機制。服務通信為同步通信設計，但是他的底層同樣是主題通信的簡化版本。

ROS本身的可靠性直接影響了所有基于ROS的機器人應用的安全性，因此，驗證ROS通信層的正確性有著重要意義。為了保證基于ROS的機器人應用的信息交流，ROS的通信層主要使用的是基于“發布/訂閱”機制的主題通信。為了保證ROS的可靠性正確性，ROS相關的開發就需要保證一些重要的性質。一般的ROS性質描述是個人提取并進行描述的，個人提取并進行描述的性質不可避免會存在二義性，這樣在實現和測試過程中都會給相關工作帶來誤導。

發明內容

為了解決現有技術存在的不足，本發明的目的是提出了一種針對ROS底層通訊機制的形式化建模與驗證方法及其應用。

本發明對ROS的主題通信所使用的“發布/訂閱”機制進行形式化建模，提出了一個詳細的ROS特征模型，并對“發布/訂閱”通訊機制中的與ROS相關的關鍵性質進行了形式化表述，根據模型對ROS的主題通信機制的這些關鍵特性進行了驗證。本發明方法建立了ROS的主題通信的形式化模型，并通過模型檢測方法驗證機器人應用是否滿足性質規范，保證該性質規范在任何時候都是成立的。將形式化建模的方法引入ROS中，可以提高其安全性和正確性，本發明所述方法包括以下步驟：

步驟一：根據開源的ROS實現源碼，提取出ROS包含的各個功能模塊，以及各模塊的功能和規則描述，然后建立其關于底層主題(topic)通信機制的形式化模型；

步驟二：從一般語言描述的“發布/訂閱”通訊機制中提取需要驗證的關鍵性質，并用時態邏輯語言來描述性質；所述關鍵性質包括：無死鎖性、可達性、活性與正確性；

步驟三：使用形式化驗證工具UPPAAL，通過所建立的形式化模型，結合具體的ROS應用實例，對提取的關鍵性質進行形式化驗證，并對驗證結果進行分析。

步驟四：根據步驟三的分析結果，如果所建立的形式化模型不滿足所有關鍵性質，則修改ROS源代碼或對ROS應用程序進行改進，直至滿足所有關鍵性質；如果滿足所有關鍵性質，則無需進行改進，獲得正確的ROS代碼或ROS發布訂閱應用程序。