随着新一代人工智能技术和自主技术快速走向战场, 将催生新型作战力量, 颠覆传统战争模式, 未来战争必将是智能化战争。无人机集群作战作为智能作战的重要形式, 正在崭露头角。采用建模仿真方法对无人机集群作战的有关问题开展研究, 可为这一新型作战样式的发展和运用提供理论支撑, 具有重要现实意义。文献[1]提出了一种扩展混成Petri网模型并对无人驾驶车辆系统的躲避障碍场景进行建模。文献[2]提出一种混成Petri网作为信号控制交叉口市区交通网络的模型。文献[3]提出了一种基于AOP的时空Petri网的CPS模型, 并以智能机器人为例, 将该模型成功应用到其故障检测和修复中。文献[4]提出了一种混成时空Petri网的CPS实时事件模型, 并以医疗控制系统为例, 分析了其建模方法的可靠性。

然而, 当前针对无人机的建模多以单一物理实体为研究对象进行建模, 缺少结合异构无人机集群特点, 深度融合离散状态和连续过程、物理和计算过程的建模与实战应用场景建模形式化验证的研究。为此, 面向集群建模技术在集群作战仿真中的迫切需求, 从作战任务需求出发, 研究基于时空混成Petri网的异构无人机集群机动行为模型构建方法, 定义交互事件解决一体化建模问题。最后选取UPPALL工具对所建模型进行验证。

1 无人机集群建模方法

无人机飞行过程中的状态变化量可以表示为^[5]

式中, 依次为3个方位参数、俯仰角、滚转角、偏航角、滚转角速度、俯仰角速度、偏航角速度、速度矢量(又分为三轴速度分量u, v, w)、迎角、侧滑角和质量。

1.1 无人机交互事件建模方法

无人系统集群可以看作一个包括物理空间和信息空间的典型赛博物理系统。在无人机执行任务中, 信息物理系统之间的交互可以看作感知和控制事件之间的交互, 感知事件包括速度、高度、俯仰角、翻滚角等关键属性信息的感知, 控制事件包括各种机动动作, 如平飞加减速、俯冲、跃升和战斗转弯等。

1) 感知事件模型定义

定义传感器感知无人机关键属性这一事件为元感知事件, 该事件是否发生仅由一个关键属性的数值大小决定。定义元感知事件的形式化模型为:

定义1   元感知事件形式化模型

式中：e_s为某一类元感知事件; τ为该类事件名称; x为相关属性名称; c为触发条件; f为函数, f: x→R; x为函数中任一变量。

定义2   感知事件触发规则

式中：OP为属性值数量关系操作符号；D为某一实数；c为感知事件触发规则。如无人机平飞加减速机动动作, Acc〈a, a>0〉用Acc表示机动动作名称, a为关键属性, 当a的值大于0时, 事件平飞加速Acc触发, 无人机随即开始执行平飞加速机动动作。又因为无人机任务执行过程是包含时空属性的, 故将在某一时刻某一空间地点的某感知事件模型表示为Acc〈a, a=30, l₀〉@t₀, l₀和t₀分别代表感知交互事件的时间和空间属性。

无人机大多机动动作的触发是由多个关键属性和多个元感知事件共同控制。在定义1的基础上, X重新定义为组合感知事件相关的属性名称, C为感知事件触发的条件集合。在定义2的基础上, 将组合感知事件模型定义为:

定义3   组合感知事件模型定义

2) 交互事件模型定义

无人机的每个机动行为都是以事件为驱动产生的, 定义交互事件模型为:

定义4  定义交互事件为四元组:

4个参数分别为交互事件中的感知事件、感知事件的接收者、感知事件的响应者或者控制事件的产生者、交互事件中的控制事件, 其中控制事件又可以定义为

式中：Y为包含多个关键属性的集合；N为关键属性具体值的集合。

1.2 异构无人机集群系统行为建模

异构无人机集群系统是既有离散行为也有连续行为的混成系统。对混成系统建模方法有形式化和非形式化两种, 由于非形式化方法无法穷尽地检测系统所有可能的状态, 故这类方法不具有完备性。在形式化建模方法中有混成自动机、混成行为系统、混成通信顺序进程、混成Petri网等。其中, 混成Petri网相比其他方法具有可描述有限状态、可更精细化描述、应用范围广等优势, 故在混成Petri网的基础上加入时空因素建立时空混成Petri网来描述异构无人机集群系统行为。

定义5   时空混成Petri网为一个十元组^[6]：

式中：P为有限库所集合, 包含离散行为P_d和随时间连续变化的P_c, 用圆形节点表示; T为有限变迁集合, 包含离散行为的T_d和随时间连续变化的T_c, 用方形节点表示; F为流关系集合, 用有向弧曲表示; W为HPN上的权函数; M₀为库所集合上初始标识向量; H为既包含离散又包含连续的混合函数; E为离散变迁激发结束的条件集合; V为连续变迁的激发速度; I表示时间函数, [t₁, t₂]表示变迁上的时间区间函数, 即事件完成的时间要求; A表示空间位置信息, 可以用区域坐标信息或者经纬度表示, A_i=(x_i, y_i)。

定义6   事件和离散变迁是一一对应关系, 离散变迁的触发表明相应事件的发生;

时空混成Petri网中既有离散状态节点, 也有连续状态节点, 通过有向弧来表示它们之间的相互作用, 变迁的激发表明有对应事件的发生。

2 无人机集群建模及其形式化验证

针对异构无人机集群协同作战, 采用基于时间自动机的UPPAAL工具, 对建立的模型进行属性验证, 证明所建模型的可靠性、可达性、有效性和实时性的, 以评价建模方法的可行性。

2.1 实例建模

假设由2架侦察无人机、3架攻击无人机和负责决策的无人机决策控制中心组成异构无人机集群系统, 对敌方13架无人机进行侦察攻击, 整个作战系统如图 1所示。

异构无人机集群系统中物理实体有侦察类无人机实体、打击类无人机实体和察打一体化无人机实体。将物理实体类分为无人机实体类和传感器实体类, 形式化表示如(1)~(2)式所示

(1)

(2)

式中：D表示动力学属性；K表示运动学属性；S表示侦察行为；A表示攻击行为；Z表示实体坐标信息；T表示时间点或区间；C₁表示传感数据变化；C₂表示传感数据未变化。

每个类下的物理实体具体定义为:

加速度传感器:

陀螺仪传感器

侦察无人机实体

攻击无人机实体

察打一体无人机实体

式中：STHP表示时空混成Petri网；p_f, p_h表示直线飞行和定常盘旋机动属性；p_d, p_p表示俯冲增速和急上升转弯机动属性；Z表示侦察无人机侦察区域、攻击无人机攻击区域、决策中心所在区域、侦察无人机监视区域, 定义为库所S₁~S₆。

在描述整个异构无人机集群作战任务过程时用库所表示时空混成Petri网中各个物理实体, 用变迁表示物理实体之间信息和控制决策指令的传输。

将无人机集群执行任务的整个过程看作是事件顺序执行的过程, 可将整个过程描述为图 2所示的Petri网。其中, 无人机决策控制中心库所负责发送控制任务。指令发送和信息反馈用变迁T₁~T₁₀表示。整个过程每个库所都有时空属性, 信息获取和指令发送对应时间点t_i, 每个库所中令牌变化时间段对应「t₁, t₂」。

图 2中各个变迁含义如表 1所示。异构无人机集群系统的事件表如表 2所示。

对异构无人机集群打击任务建模先用Petri网对整体协同打击过程进行建模, 然后用时空混成Petri网对单架打击无人机机动行为进行建模。

所有打击无人机到达指定位置后开始打击任务, 3架打击无人机协同打击过程可用Petri网描述如图 3所示。

在图 3中, P₀为打击无人机到达指定打击区域, P_ij表示打击无人机各自状态, 1≤i≤3, i∈N, 1≤j≤3, j∈N。j=1时, 无人机开始协同打击, j=2时, 当前序号无人机将自身打击完成情况发送到控制中心, P₄为控制中心接收所有打击信息。P₆为协同打击任务完成; T_ij表示打击无人机状态变化。j=1, 协同打击任务下发事件, j=2, 开始打击任务准备完成事件, j=3, 当前无人机成功发送打击任务完成情况到控制中心。T₄为控制中心获取到的信息为没有完成全部打击任务, T₅为13个打击目标均已打击完成。

当用Petri网对3架打击无人机协同打击任务整体建模以后, 具体单个无人机状态用时空混成Petri网表示, 所建模型如图 4所示。

完成打击任务先经过平飞加速到达指定打击空间位置点; 再执行俯冲到达第一个目标正上方; 然后平飞减速靠近目标; 再进行战斗转弯; 最后快速跃升完成打击任务。离散库所表示机动动作的转移, 连续库所表示打击无人机运行过程中关键属性数值的变化, 连续变迁表示关键属性变化规律。

P₁为平飞加速, V从200 m/s加速到300 m/s, 在此过程中涉及速度、切向过载等关键属性变化, 连续库所P₉表示t₁时刻打击无人机的速度v₁, T₈表示速度变化的微分方程，即

P₁₀表示t₁到t_i时刻速度具体变化值ΔV。T₁表示平飞加速机动动作完成。P₂为俯冲机动动作。T₉表示迎角变化的微分方程，即

T₂为俯冲机动动作完成。P₃表示平飞减速机动动作, 与平飞加速机动动作类似。P₅表示战斗转弯机动动作。T₁₀表示高度变化的微分方程dH=cosθ(vsinϕ+vcosϕ)-usinθ。T₁₁表示滚转角变化的微分方程dϕ=qcosϕ-rsinϕ。T₄表示战斗转弯机动动作完成。P₆表示跃升机动动作与俯冲机动动作类似。T₅表示跃升机动动作完成。P₇表示本次打击任务完成。T₆表示还有待打击目标需再次到达目标执行打击任务。T₇表示本架无人机已完成所有打击任务。P₈表示打无人机打击任务结束。

在异构无人机集群打击实例中, 交互事件关键属性包括速度v、高度h、气流角迎角α、滚转角ϕ, X={v, h, α, ϕ}, 不同属性值代表不同事件, 对感知事件、控制事件和交互事件建模如下所示:

感知事件模型:

控制事件模型:

交互事件模型:

2.2 实例模型的形式化验证

Acc_Action、Sub_Action、Turn_Action、Jump_Action、Attack_Action、Finished_Action 6个离散机动动作模块和Velocity、High、Roll、Pitch 4个连续属性变化模块, 分别表示水平加速机动动作、俯冲机动动作、战斗转弯机动动作、跃升机动动作、打击机动动作和完成任务行为。模块之间通过同步信道进行交互。将表示离散连续的10个模块组件分别映射成时间自动机模板, 将模块中执行的每个过程映射为时间自动机模板中的位置, 将机动动作转换事件映射为时间自动将中的同步通道, 得到如图 5所示模型。

时间自动机模型中, 圆圈代表系统各种状态, 带箭头有向线段代表系统中状态之间的转换, 红色圆圈表示当前正在执行的状态, 深蓝色数据表示当前状态的更新操作, 绿色数据表示当前状态的转移条件, 浅蓝色数据表示当前状态的同步信道传输。

2.3 实例验证分析

运用UPPAAL工具^[7-8]，进行自动分析, 得到实例执行打击任务过程的流程图, 如图 6所示。

基于时间自动机模型, 借助UPPAAL工具对无人机打击过程中的各种属性进行验证:

E<>(enemy==13): 验证了完成任务过程中, 至少存在一条路径, 最终将13个敌方目标都消灭掉, 可验证模型的可达性;

A<>(Sub.Sub_Complete imply roll_state==0): 验证了如果俯冲机动动作完成则认为紧接着进入了下一个机动动作——战斗转弯, 可验证模型的实时性;

E[](h≥0): 验证了过程中的高度属性不会有负值;

A[](Attack.Attack_Complete imply enemy==13): 验证了如果打击任务完成, 则敌方13个目标全部被消灭, 可验证模型的有效性;

E<>(Acc.Acc_Complete): 验证了存在水平加速这个机动动作完成这个状态。

以上验证的属性均可代表某一类属性。验证结果如图 7所示。

结果表明所建模型能很好地对该实例过程进行描述, 性质均验证通过。该模型满足可靠性、可达性、有效性和实时性的要求。

3 结论

针对异构无人机集群作战仿真中物理实体数字模型描述这一关键技术, 围绕异构无人机集群作战任务过程的建模和验证, 通过对无人机实体和无人机集群关键属性值变化的运动学和动力学方程描述, 以及无人机实体的感知事件、控制事件和两者之间的交互事件的形式化建模, 将无人机的建模由单一物理实体增加到多个物理实体; 选用时空混成Petri网描述军用实战-异构无人机集群打击过程。该方法有效描述无人机集群系统中物理过程和计算过程的融合过程, 刻画出各节点之间信息的交换和协同。论文采用UPPAAL工具进行验证和分析, 为无人机集群作战系统提供验证框架和环境, 证明所建模型满足可靠性、可达性、有效性和实时性要求。