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

有效

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

1.一種ROS底層通訊機制的形式化建模與驗證方法，其特征在于，包括以下步驟：

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

步驟A1：從ROS開源代碼中提取所要建模與描述的主節點、節點、發布器、訂閱器、主題管理器和鏈接六個重要模塊以及它們的功能與規則；

所述功能包括節點注冊、建立鏈接、發布消息、訂閱消息、執行回調；

步驟A2：根據主節點、節點、發布器、訂閱器、主題管理器和鏈接六個模塊的功能與規則描述提取出六個模塊之間的同步關系，并用消息函數與通道進行表示；

步驟A3：根據消息函數與通道表示的模塊之間的同步關系，對每個模塊進行形式化建模，并將各模塊的建模結果進行組合，結合形成完整的形式化模型；

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

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

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

2.如權利要求1所述的ROS底層通訊機制的形式化建模與驗證方法，其特征在于，所述步驟二從“發布/訂閱”通訊機制中提取關鍵性質，用時態邏輯語言描述性質包括以下步驟：

步驟B1：從“發布/訂閱”通訊機制的描述中提取ROS應用所必備的關鍵性質；

步驟B2：根據提取出的關鍵性質，使用時態邏輯語言，進行對關鍵性質的形式化表述；

所述關鍵性質包括：無死鎖性、可達性、活性與正確性。

3.如權利要求2所述的ROS底層通訊機制的形式化建模與驗證方法，其特征在于，所述步驟三使用形式化驗證工具，通過所建立的形式化模型結合具體的ROS發布訂閱應用實例，對提取的關鍵性質進行形式化驗證，并對驗證結果進行分析包括以下步驟：

步驟C1：根據所述步驟A3形成的形式化模型，在形式化驗證工具中建立符合形式化驗證工具規則的ROS通訊機制中的形式化模型；

步驟C2：根據所述步驟B2所得到的待驗證關鍵性質的時態邏輯語言表述，在形式化驗證工具中轉化為符合形式化驗證工具規則的表述形式；

步驟C3：在模型聲明中，創建一個ROS應用實例情景，在形式化驗證工具中描述應用實例中的訂閱關系；

步驟C4：根據步驟C1中的形式化模型和步驟C3中的ROS應用實例，對步驟C2中的時態邏輯語言表述的關鍵性質進行模擬和驗證，并對結果進行分析。

4.如權利要求3所述的ROS底層通訊機制的形式化建模與驗證方法，其特征在于，所述步驟四修改ROS源代碼或ROS機器人應用程序直至滿足所有關鍵性質包括以下步驟：

步驟D1：如果步驟C4的分析結果與模擬存在不滿足一條或多條關鍵性質的反例，則找出不滿足所述關鍵性質的路徑狀態，并執行步驟D2；否則得到正確的ROS代碼或ROS發布訂閱應用程序；

步驟D2：根據路徑狀態得到源代碼或ROS應用程序中對應的執行代碼，進行完善和修改；

步驟D3：重復步驟C4，如果模擬驗證結果不滿足所有關鍵性質，則重新執行步驟D1，否則說明已經得到正確的ROS代碼或ROS發布訂閱應用程序。