本发明涉及一种基于时间自动机的无人机飞控程序建模与验证方法，属于无人机自动控制的技术领域。
背景技术：
近年来，无人机在环境监测、气象探测、基础设施运维等应用场景下得到广泛应用。无人机随着应用环境的日趋复杂，以及任务的日益多样，对无人机的远程遥控，以及多无人机基于无线通信的编队协同，已经成为重要发展趋势。但是，气动参数不确定性、执行机构故障等因素会严重降低无人机的控制精度，由于无线通信的开放性，还存在电磁环境干扰等影响因素。
为了提升无人机对未知干扰和执行机构故障的鲁棒性、状态误差限制以及跟踪误差收敛性能，需要优化无人机控制算法。例如，北京航空航天大学提出了一种无人机固定时间路径跟踪容错制导控制方法，利用反步法及固定时间收敛的视线制导算法确保无人机路径跟踪误差在固定时间内收敛，通过非线性固定时间观测器对不确定性进行估计补偿，消除执行机构故障及外部环境干扰等因素对跟踪性能的影响(北京航空航天大学学报，2020.7)，等等。
但是，未知干扰值通过很难进行精确测量，特别是当通信延迟较大时，可能无法保证正常信息交互和控制算法的正确执行，因此研究存在通信时延条件下的无人机控制具有十分重要的现实意义。例如西北工业大学提出了具有时延和干扰约束的多无人机滑模一致性编队控制方法，在考虑时延的基础上设计合适的一致性算法，利用滑模控制(smc)方法解决编队系统中的轨迹跟踪和控制问题，并保证系统对于外部扰动的鲁棒性(西北工业大学学报，2020.4)。
总之，无人机飞控程序的设计与测试是个复杂的技术问题，因为既涉及自动控制算法，又涉及与通信有关的性能，要保证遥控命令的正确性，需要保证信息交互的时效性，在规定的时间内完成通信过程。对控制程序的测试目前一般基于典型的黑盒测试，存在测试用例不能完全覆盖的问题。业界采用形式化验证避免上述测试覆盖率问题。其基本思想是通过遍历系统模型的状态空间，来检验系统模型是否满足给定的性质。例如云南大学提出了一种机器人分数阶pid控制器稳定性的形式化验证方法，申请号为201610485045.1，针对机器人分数阶pid控制器，建立分数阶pid控制器和分数阶闭环控制系统的高阶逻辑形式化模型，利用该形式化模型和定理，验证分数阶pid控制系统的稳定性。但是，该专利未考虑控制过程中的无线通信，不能完全适用于无人机在无线信道上存在电磁干扰的场景，对于气动参数不确定性、执行机构间歇性故障等因素考虑不足。
技术实现要素：
针对无人机的非线性特性和所受的干扰，需要考虑随机干扰、通信延迟等问题，本发明提供一种基于时间自动机的无人机飞控程序建模与验证方法，基于时间自动机，建立无人机飞控程序的形式化模型，验证控制算法的正确性；同时，引入随机性因素，通过多次仿真，对时效性进行统计，在存在通信时延、外部干扰等情况下提高无人机飞控的鲁棒性。
本发明具体采用以下技术方案解决上述技术问题：
一种基于时间自动机的无人机飞控程序建模与验证方法，包括以下步骤：
步骤1、将无人机飞控程序的命令交互过程分为主控进程、消息传输、无线信道，基于时间自动机形式化建模方法，定义时间自动机模型中的状态与变迁特性；
步骤2、基于定义的状态与变迁特性，建立无人机飞控程序的时间自动机模型，使用形式化验证工具进行状态空间搜索，验证无人机飞控程序运行过程的时序正确；
步骤3、针对无人机工作环境的干扰，在所述状态与变迁特性中定义干扰因素，并重新生成时间自动机模型的关联矩阵，验证时间自动机模型的有界性，即无人机飞控程序执行的时效性能在有限时间内进行确认；
步骤4、基于概率统计对通信时间消耗进行分析，验证无人机飞控程序运行过程能在预定的时间内完成。
进一步地，作为本发明的一种优选技术方案，所述步骤1定义状态与变迁特性，具体为：
m＝(l，π，s，t，c，g，e)
其中，l表示无人机飞控程序的主控进程、消息传输、无线信道三个模型层级，π是表示主控进程的时间约束与消息类型的集合；s表示时间自动机模型中的状态集合；t表示变迁集合，包括模型层级l间的变迁，以及消息传输和状态转换的变迁；c表示s和π的对应关系；g表示包括状态转换的条件函数；e表示消息传输、超时处理引起状态转换的表达式函数。
进一步地，作为本发明的一种优选技术方案，所述步骤2建立无人机飞控程序的时间自动机模型，包括：
确定无人机的状态集合s、变迁集合t包含元素：
s＝{s0…sj|j∈0，1，2…}
t＝{t0…ti|i∈0，1，2…}
其中，sj表示无人机的各种状态；ti表示无人机状态间的变迁；
将无人机飞控程序建模为时间自动机模型，用关联矩阵r表示：
其中，rij表示无人机的变迁ti和状态sj之间的关系。
进一步地，作为本发明的一种优选技术方案，所述步骤3在所述状态与变迁特性中定义干扰因素，包括：
在消息传输模型、无线信道模型中增加状态sot，用来定义控制事件因外部干扰的超时；在表达式函数e中增加干扰因素的表示。
进一步地，作为本发明的一种优选技术方案，所述步骤4基于概率统计对通信时间消耗进行分析，包括：在变迁模型中引入随机因素，丢包率通过变迁的执行条件模拟，延时通过状态转换函数g的执行时间模拟。
本发明采用上述技术方案，能产生如下技术效果：
本发明的方法，基于形式化方法，建立时间自动机模型，通过状态空间搜索验证无人机飞控程序的可操作性，并分析时间自动机模型的有界性，缓解状态空间爆炸问题；针对无线遥控中的外界干扰，引入外部电磁环境干扰、气动参数不确定性、执行机构故障等随机性因素，通过多次仿真，对无人机飞控程序的时效性进行统计分析，提高无人机在复杂环境下的鲁棒性。本发明适用范围广泛，可应用于多功能无人机飞控、无人机编队、基于无人机的气象探测、设备巡视等。
附图说明
图1为本发明基于时间自动机的无人机飞控程序建模与验证方法的流程示意图。
图2为本发明提供的无人机飞控程序的时间自动机模型示意图。
具体实施方式
以下将结合具体实施例对本发明提供的技术方案进行详细说明，应理解下述具体实施方式仅用于说明本发明而不用于限制本发明的范围。
实施例1，以某一种现有的无人机飞控系统为例，该系统可适用于四旋翼无人机等广泛应用的无人机，在飞行时通过搭载的惯性导航系统、摄像头、激光雷达等，判断自身的飞行姿态，实现避障等功能，并能接受外部指令完成具体的任务。本发明提供一种基于时间自动机的无人机飞控程序建模与验证方法，对飞控程序的建模和验证过程如图1所示，具体包括如下步骤：
步骤1、将无人机飞控程序的命令交互过程分为主控进程、消息传输、无线信道，本发明基于时间自动机形式化建模方法，定义时间自动机模型中相关的状态与变迁特性，具体为：
m＝(l，π，s，t，c，g，e)
其中，l表示无人机飞控程序的主控进程、消息传输、无线信道三个模型层级，π是表示主控进程的时间约束与消息类型的集合；s表示时间自动机模型中的状态集合；t表示变迁集合，包括模型层级l间的变迁，以及消息传输和状态转换的变迁；c表示s和π的对应关系；g表示包括状态转换的条件函数；e表示消息传输、超时处理引起状态转换的表达式函数。
步骤2、基于定义的状态与变迁特性，建立无人机飞控程序的时间自动机模型，使用形式化验证工具进行状态空间搜索，验证无人机飞控程序运行过程的时序是否正确；
根据步骤1中的定义，将无人机飞控程序建模为时间自动机模型。部分与无线通信相关的模型如图2所示，将无人机当前状态、受控状态、失控、通信过程等状态，定义为状态集合s：
s＝{s0…sj|j∈0，1，2…}
类似的，如图2中所示，将无人机的建立通信链路、任务循环执行、中断控制、发送数据等变迁，定义为变迁集合t：
t＝{t0…ti|i∈0，1，2…}
其中，s0...sj表示无人机的各种状态；t0...ti表示无人机状态间的变迁；
上述的状态s0...sj在图2中用uavc、uavp、err、comm等标记；上述的变迁t0...ti在图2中用commconf、taskproc、interruptcon、senddata等标记。
将无人机飞控程序建模为包含j 1个状态和i 1个变迁的时间自动机模型，可以用关联矩阵r表示：
其中，rij表示变迁ti和状态sj之间的关系；
基于关联矩阵r，验证时间自动机模型的有界性，在此基础上使用形式化验证工具进行状态空间搜索，可采用通用的spin工具，以promela语言描述上述模型，验证控制过程的时序是否正确。
步骤3、针对无人机工作环境的干扰，在步骤1所述的状态与变迁特性中定义干扰因素，在消息传输模型、无线信道模型中增加状态sot，用来定义控制事件因外部干扰的超时，在表达式函数e中增加电磁、气流等干扰因素的表示，干扰因素为设定的经验值。并重新生成时间自动机模型的关联矩阵，采用和步骤2中相同的方式验证时间自动机模型的有界性，即无人机飞控程序执行的时效性能在有限时间内进行确认。
步骤4、基于概率统计对通信时间消耗进行分析，验证无人机飞控程序运行过程能在预定的时间内完成。
基于概率统计对通信时间消耗进行分析，即在变迁模型中引入电磁干扰、气流等随机因素，如图2中的interruptcon变迁，在执行条件中引入随机函数rand，模拟延时，使每次模拟的延时存在随机差异，即丢包率通过变迁的执行条件模拟，延时通过状态转换函数g的执行时间模拟，通过执行时间模拟延时。在此基础上，多次执行步骤3中的验证过程，即重复进行状态空间搜索，从而仿真无人机飞控程序的执行时间，验证控制过程和无线遥控操作可以按照时序，在预定的时间内完成执行。
综上，本发明方法，针对无线遥控中的外界干扰，引入外部电磁环境干扰、气动参数不确定性、执行机构故障等随机性因素，通过多次仿真，对无人机飞控程序的时效性进行统计分析，提高无人机在复杂环境下的鲁棒性。本发明适用范围广泛，可应用于多功能无人机飞控、无人机编队、基于无人机的气象探测、设备巡视等。
本发明方案所公开的技术手段不仅限于上述实施方式所公开的技术手段，还包括由以上技术特征任意组合所组成的技术方案。应当指出，对于本技术领域的普通技术人员来说，在不脱离本发明原理的前提下，还可以做出若干改进和润饰，这些改进和润饰也视为本发明的保护范围。
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＝{s0…sj|j∈0,1,2…}
t＝{t0…ti|i∈0,1,2…}
其中，sj表示无人机的各种状态；ti表示无人机状态间的变迁；
将无人机飞控程序建模为时间自动机模型，用关联矩阵r表示：
其中，rij表示无人机的变迁ti和状态sj之间的关系。
4.根据权利要求2所述基于时间自动机的无人机飞控程序建模与验证方法，其特征在于，所述步骤3在所述状态与变迁特性中定义干扰因素，包括：
在消息传输模型、无线信道模型中增加状态sot，用来定义控制事件因外部干扰的超时；
在表达式函数e中增加干扰因素的表示。
5.根据权利要求2所述基于时间自动机的无人机飞控程序建模与验证方法，其特征在于，所述步骤4基于概率统计对通信时间消耗进行分析，包括：
在变迁模型中引入随机因素，丢包率通过变迁的执行条件模拟，延时通过状态转换函数g的执行时间模拟。
技术总结