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

有效

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

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

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

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

步驟3、針對無人機工作環境的干擾，在所述狀態與變遷特性中定義干擾因素，并重新生成時間自動機模型的關聯矩陣，驗證時間自動機模型的有界性，即無人機飛控程序執行的時效性能在有限時間內進行確認；

步驟4、基于概率統計對通信時間消耗進行分析，驗證無人機飛控程序運行過程能在預定的時間內完成。

2.根據權利要求1所述基于時間自動機的無人機飛控程序建模與驗證方法，其特征在于，所述步驟1定義狀態與變遷特性，具體為：

M=(L,Π,S,T,C,G,E)

其中，L表示無人機飛控程序的主控進程、消息傳輸、無線信道三個模型層級，Π是表示主控進程的時間約束與消息類型的集合；S表示時間自動機模型中的狀態集合；T表示變遷集合，包括模型層級L間的變遷，以及消息傳輸和狀態轉換的變遷；C表示S和Π的對應關系；G表示狀態轉換函數；E表示消息傳輸、超時處理引起狀態轉換的表達式函數。

3.根據權利要求1所述基于時間自動機的無人機飛控程序建模與驗證方法，其特征在于，所述步驟2建立無人機飛控程序的時間自動機模型，包括：

確定無人機的狀態集合S、變遷集合T包含元素：

S={s₀…s_s|j∈0,1,2…}

T={t₀…t_i|i∈0,1,2…}

其中，s_j表示無人機的各種狀態；t_i表示無人機狀態間的變遷；

將無人機飛控程序建模為時間自動機模型，用關聯矩陣R表示：

其中，r_ij表示無人機的變遷t_i和狀態s_j之間的關系。

4.根據權利要求2所述基于時間自動機的無人機飛控程序建模與驗證方法，其特征在于，所述步驟3在所述狀態與變遷特性中定義干擾因素，包括：

在消息傳輸模型、無線信道模型中增加狀態SOT，用來定義控制事件因外部干擾的超時；

在表達式函數E中增加干擾因素的表示。

5.根據權利要求2所述基于時間自動機的無人機飛控程序建模與驗證方法，其特征在于，所述步驟4基于概率統計對通信時間消耗進行分析，包括：

在變遷模型中引入隨機因素，丟包率通過變遷的執行條件模擬，延時通過狀態轉換函數G的執行時間模擬。