(19)中华 人民共和国 国家知识产权局 (12)发明 专利申请 (10)申请公布号 (43)申请公布日 (21)申请 号 202111572432.6 (22)申请日 2021.12.21 (71)申请人 北航 （四川） 西部国际创新港科技有 限公司 地址 610000 四川省成 都市天府新区科 学 城湖畔路北段1 199号 (72)发明人 周强　刘广才　 (74)专利代理 机构 成都方圆聿联专利代理事务 所(普通合伙) 51241 代理人 邓永红 (51)Int.Cl. G06F 30/27(2020.01) G06F 30/15(2020.01) G06N 5/04(2006.01) (54)发明名称 基于UPPAAL的无人机系统安全性形式化建 模验证方法 (57)摘要 本发明提供基于UPPAAL的无人机系统安全 性形式化建模验证方法， 包含两步骤， 分别是算 法推理验证和仿真建模验证； 算法推理验证， 通 过数学方法对待验证的无人机系统的性质进行 逻辑推演， 初步判断其是否存在安全性问题， 为 仿真建模验证提供理论依据； 仿真建模验证， 在 算法推理验证的基础上， 利用UPPAAL工 具对待验 证的系统进行建模与仿真， 进一步模拟系统运行 中的状态， 并最终得出待验证的无人机系统安全 性要求是否被满足的结论， 同时， 若无人机系统 的安全性要求不被满足， 输出造成安全性不被满 足的具体 状态， 供研究人员做针对性调整。 权利要求书2页 说明书9页 附图8页 CN 114297917 A 2022.04.08 CN 114297917 A 1.基于UPPAAL的无人机系统安全性形式化建模验证方法， 其特征在于， 包含两步骤， 分 别是算法推理验证和仿真 建模验证； 算法推理验证， 通过数学方法对待验证的无人机系统的性质进行逻辑推演， 初步判断 其是否存在安全性问题， 为仿真 建模验证提供理论依据； 仿真建模验证， 在算法推理验证的基础上， 利用UPPAAL工具对待验证的系 统进行建模 与仿真， 进一步模拟系统运行中的状态， 并最终得出待验证的无人机系统安全性要求是否 被满足的结论， 同时， 若 无人机系统的安全性要求不被满足， 输出造成安全性不被满足的具 体状态， 供研究人员做针对性调整。 2.根据权利要求1所述的基于UPPAAL的无人机系统安全性形式化建模验证方法， 其特 征在于， 所述的算法推理验证， 基于LRTL的无 人机安全性形式化验证算法。 3.根据权利要求2所述的基于UPPAAL的无人机系统安全性形式化建模验证方法， 其特 征在于， 所述的算法推理验证， 具体包括以下子步骤： 步骤(1)： 提取出具体系统的系统行为规范SP和安全要求SA， 将其写作时间约束不等式 的形式； 系统行为规范SP包含了任务场景本身的要求， 安全要求SA代表与无人机安全相关的要 求； 在将S P及SA提炼出来后， 将其改写为命题形式； 步骤(2)： 根据S P和SA， 建立命题 步骤(3)： 将F转 化为合取范式FCNF； 步骤(4)： 分别提取出合取范式中的正子句Fpos及负子句Fneg， 构造子句 集合PF＝Fpos∪ Fneg； 步骤(5)： 利用归结原理对PF进行归结， 以证明S P→SA成立。 4.根据权利要求1所述的基于UPPAAL的无人机系统安全性形式化建模验证方法， 其特 征在于， 所述的算法推理验证， 利用实时系统验证工具UPPAAL对该场景进行建模， 并利用 UPPAAL的验证器验证 “通过系统行为规范SP命题的成立， 是否可以确 定安全要求SA命题的 成立”； 若SP命题的成立一定可以推理出SA命题的成立， 则证 明该系统中的无人机只需要严格 遵循系统的行为规范， 即可确保自身的安全， 证明了系统自身的安全性以及 任务的合理性； 否则， 证明无 人机即使严格遵循了系统行为 规范， 却仍然无法 保证自身的安全。 5.根据权利要求1所述的基于UPPAAL的无人机系统安全性形式化建模验证方法， 其特 征在于， 所述的算法推理验证包括以下子步骤： 步骤(1)： 根据任务场景， 确定系统的系统行为 规范SP及安全要求SA； 步骤(2)： 根据飞行器性能， 设置系统指标； 步骤(3)： 利用UP PAAL建立系统中无 人机在节点间的位置转移模型； 在建模时， 首先依照任务要求， 对无人机所在的空域进行规划， 在空域中的关键位置处 设置节点， 这些节点将作为无 人机在整个任务执 行流程中的观测点； 其次， 需要依据建立的节点， 设置无 人机的转移规则； 步骤(4)： 利用UP PAAL建立系统中各个节点自身的状态转换模型； 步骤(5)： 对系统进行验证， 检验S P是否必然满足SA；权　利　要　求　书 1/2 页 2 CN 114297917 A 2通过命题验证功能对安全要求进行验证， 将SA以规定的语法格式写入UPPAAL的验证器 中， 通过建立的模型验证SA命题是否成立； 若验证结果为成立， 则证明系统设计符合安全性 要求； 若验证结果为不成立， 则证明系统设计有一定缺陷， 将导致系统中的无人机安全性无 法保证， 需要调整任务或对系统进行修改。权　利　要　求　书 2/2 页 3 CN 114297917 A 3