[發明專利]一種基于時間自動機的無人機飛控程序建模與驗證方法

有效

• 申請號: 202011351643.2
• 申請日: 2020-11-26
• 公開（公告）號: CN112486141B
• 公開（公告）日: 2022-09-02
• 發明（設計）人: 劉佳;錢昌宇;卞方舟
• 申請（專利權）人: 南京信息工程大學
• 主分類號: G05B23/02
• 分類號: G05B23/02
• 代理公司: 南京經緯專利商標代理有限公司 32200
• 代理人: 徐瑩

本發明公開了一種基于時間自動機的無人機飛控程序建模與驗證方法，包括：將無人機飛控程序的命令交互過程分為主控進程、消息傳輸、無線信道，定義時間自動機模型中的狀態與變遷特性；建立無人機飛控程序的時間自動機模型，使用形式化驗證工具進行狀態空間搜索，驗證無人機飛控程序運行過程的時序正確；針對無人機工作環境的干擾，在狀態與變遷特性中定義干擾因素，并重新生成時間自動機模型的關聯矩陣，驗證模型的有界性，即無人機飛控程序執行的時效性能在有限時間內進行確認；基于概率統計對通信時間消耗進行分析，驗證無人機飛控程序運行過程能在預定的時間內完成。本發明可提高無人機在復雜環境下的魯棒性。

技術領域

本發明涉及一種基于時間自動機的無人機飛控程序建模與驗證方法，屬于無人機自動控制的技術領域。

背景技術

近年來，無人機在環境監測、氣象探測、基礎設施運維等應用場景下得到廣泛應用。無人機隨著應用環境的日趨復雜，以及任務的日益多樣，對無人機的遠程遙控，以及多無人機基于無線通信的編隊協同，已經成為重要發展趨勢。但是，氣動參數不確定性、執行機構故障等因素會嚴重降低無人機的控制精度，由于無線通信的開放性，還存在電磁環境干擾等影響因素。

為了提升無人機對未知干擾和執行機構故障的魯棒性、狀態誤差限制以及跟蹤誤差收斂性能，需要優化無人機控制算法。例如，北京航空航天大學提出了一種無人機固定時間路徑跟蹤容錯制導控制方法，利用反步法及固定時間收斂的視線制導算法確保無人機路徑跟蹤誤差在固定時間內收斂，通過非線性固定時間觀測器對不確定性進行估計補償，消除執行機構故障及外部環境干擾等因素對跟蹤性能的影響(北京航空航天大學學報，2020.7)，等等。

但是，未知干擾值通過很難進行精確測量，特別是當通信延遲較大時，可能無法保證正常信息交互和控制算法的正確執行，因此研究存在通信時延條件下的無人機控制具有十分重要的現實意義。例如西北工業大學提出了具有時延和干擾約束的多無人機滑模一致性編隊控制方法，在考慮時延的基礎上設計合適的一致性算法，利用滑模控制(SMC)方法解決編隊系統中的軌跡跟蹤和控制問題，并保證系統對于外部擾動的魯棒性(西北工業大學學報，2020.4)。

總之，無人機飛控程序的設計與測試是個復雜的技術問題，因為既涉及自動控制算法，又涉及與通信有關的性能，要保證遙控命令的正確性，需要保證信息交互的時效性，在規定的時間內完成通信過程。對控制程序的測試目前一般基于典型的黑盒測試，存在測試用例不能完全覆蓋的問題。業界采用形式化驗證避免上述測試覆蓋率問題。其基本思想是通過遍歷系統模型的狀態空間，來檢驗系統模型是否滿足給定的性質。例如云南大學提出了一種機器人分數階PID控制器穩定性的形式化驗證方法，申請號為201610485045.1，針對機器人分數階PID控制器，建立分數階PID控制器和分數階閉環控制系統的高階邏輯形式化模型，利用該形式化模型和定理，驗證分數階PID控制系統的穩定性。但是，該專利未考慮控制過程中的無線通信，不能完全適用于無人機在無線信道上存在電磁干擾的場景，對于氣動參數不確定性、執行機構間歇性故障等因素考慮不足。

發明內容

針對無人機的非線性特性和所受的干擾，需要考慮隨機干擾、通信延遲等問題，本發明提供一種基于時間自動機的無人機飛控程序建模與驗證方法，基于時間自動機，建立無人機飛控程序的形式化模型，驗證控制算法的正確性；同時，引入隨機性因素，通過多次仿真，對時效性進行統計，在存在通信時延、外部干擾等情況下提高無人機飛控的魯棒性。

本發明具體采用以下技術方案解決上述技術問題：

一種基于時間自動機的無人機飛控程序建模與驗證方法，包括以下步驟：

步驟1、將無人機飛控程序的命令交互過程分為主控進程、消息傳輸、無線信道，基于時間自動機形式化建模方法，定義時間自動機模型中的狀態與變遷特性；

步驟2、基于定義的狀態與變遷特性，建立無人機飛控程序的時間自動機模型，使用形式化驗證工具進行狀態空間搜索，驗證無人機飛控程序運行過程的時序正確；