[發明專利]一種針對分布式機器人集群的層次化時序屬性監控方法

在審

• 申請號: 202011183839.5
• 申請日: 2020-10-29
• 公開（公告）號: CN112148565A
• 公開（公告）日: 2020-12-29
• 發明（設計）人: 董威;胡馳;史浩;尹良澤;陳立前;文艷軍
• 申請（專利權）人: 中國人民解放軍國防科技大學
• 主分類號: G06F11/30
• 分類號: G06F11/30
• 代理公司: 湖南兆弘專利事務所(普通合伙) 43008
• 代理人: 劉暢舟

本發明公開了一種針對分布式機器人集群的層次化時序屬性監控方法，包括：在分布式機器人集群中部署分布式節點監控器，獲得機器人操作系統在資源層、通信層、單個機器人層在高層屬性規約層面涉及的事件和命題的數據；對數據進行組幀和封裝，并形成數據接口，將數據接口和分布式節點監控器進行動態綁定，然后傳輸數據流到服務器；服務器生成中心監控器并按照MTL3?RMoM時序邏輯解算算法生成監控器并得到判決結果；在中心監控器實時顯示判決結果并實時反饋違反信息給分布式節點監控器。本發明能夠在線監控拓撲關系動態變化的機器人集群屬性是否違背，同時能夠覆蓋集群屬性，單機器人屬性，硬件資源和通信層屬性的三層屬性運行時監控。

技術領域

本發明涉及計算機領域，尤其涉及一種針對分布式機器人集群的層次化時序屬性監控方法。

背景技術

近年來，隨著新的計算技術、網絡技術和控制技術的不斷涌現，以機器人系統為典型的信息物理融合系統CPS(Cyber-physical Systems)已經成為一個快速發展的新趨勢。從系統工程的角度，機器人集群本身就是一個較為復雜的軟硬件協同系統，其復雜性體現在機器人集群CPS所特有的混成(物理設備和信息系統深度整合)特性、時間空間特性、系統模型和海量數據復雜性以及分布式協同特性等等。而且，這類系統還往往面臨著各節點動態變化、環境多變等外部要素，很難完全確保這類CPS系統在整個執行過程中完全滿足需求規約。如何保證需求和實現一致性已經成為機器人以及機器人集群進行產業布局和應用推廣的一道擺在面前的瓶頸性難題。

想要系統性地驗證和保障機器人集群CPS系統安全，基于形式化方法的在線監控是一項必要且有效的手段，能夠有效調高“系統的可信度”，也是目前學者們研究的熱點。在眾多的軟硬件系統監控方法中，運行時驗證(Runtime Verification簡稱RV)是近年來興起的輕量級的軟件可靠性保障技術，它基于目標系統的運行軌跡來判定給定的性質規約是否滿足。由于系統運行軌跡的唯一性，它有效的克服了當系統足夠復雜后帶來的模型檢驗技術的狀態空間爆炸和測試技術全路徑難以覆蓋的問題。另外與傳統的軟件可靠性保障技術不同的是，RV技術主要應用在系統部署后，對運行環境和上下文不確定導致的系統缺陷能很好的監控。這些特點都使得RV技術很適合應用在機器人集群CPS系統上。

然而，由于機器人系統的復雜性和RV技術中形式化理論的學習門檻較高。當前，RV技術在機器人集群系統上的研究還處于初級階段，相關的工具應用也較少。因此，本發明主要在典型的機器人操作系統ROS(Robot Operating System)上開展RV應用，通過對基于ROS系統的機器人集群的運行時監控，保障機器人導航、避障等自主行為以及集群協同控制在運行時狀態下始終滿足安全規約。

并且，針對ROS機器人系統及其集群系統，提出適合的運行時驗證理論和相應的工具。

綜上，針對ROS系統下的機器人集群的RV技術應用需要基于機器人系統的全局及局部約束，著重研究如何運用RV技術來層次化地實時監控整個系統，以及發現性質違反后的強制方法，從而豐富這類CPS系統的可信性保障手段。這樣的技術實現具有很大的挑戰：一是面向復雜的機器人集群系統，如何構建層次化監控CPS系統的監控框架，并保證該方法的時空一致性；二是如何增強監控規約語言和形式化描述方法，從而將RV監控器應用于混成特性的CPS系統。