UAV Cluster Behavior Modeling Based on Spatial-Temporal Hybrid Petri Net

Abstract

Currently, we are facing an increasing trend in the use of unmanned aerial vehicles (UAV) in various activities, both civilian and military. The application of UAVs in the battlefield has received extensive attention amid a global new military revolution. A UAV cluster is a large and complex real-time feedback system that integrates a communication and sensor network, control system, calculation, and physical process. The heterogeneous UAVs conduct complex behaviors, which requires a comprehensive description and analysis of UAV cluster modeling. The integrated modeling of the heterogeneous UAV cluster is of great significance and value to test and verify the new combat mode. In this paper, we present a novel representation framework based on the Petri nets. We used a spatial-temporal hybrid Petri net to illustrate the discrete state and continuous process of a heterogeneous UAV cluster system, and effectively achieved the fusion of a physical and computational process and interaction event modeling in the cluster system. Finally, the formal verification of UAV cluster attack mission modeling was carried out by UPPAAL, suggesting the proposed modeling method is feasible and effective.

1. Introduction

The increasing application of the new generation of artificial intelligence technology and autonomous technology rapidly in the battlefield will give birth to a new type of combat force and overturn the traditional mode of war [1,2,3,4,5]. The future war will be intelligent war. The application of a UAV cluster in a battlefield is an important part of intelligent warfare. The UAV cluster is a kind of large and complex real-time feedback system that integrates the calculation process, the communication network, the physical process, sensor network, and control system. We need a comprehensive description and analysis on the model of the UAV cluster due to the various forms of complex behavior between heterogeneous UAVs. Using the modeling and simulation method to study the relevant issues of UAV cluster combat can provide theoretical support for the development and application of this new combat style, which has important practical significance [6,7,8]. Cao Ruimin [9] proposed the hybrid stochastic timed Petri net (HSTPN) modeling method for hybrid systems featuring discrete, continuous, conflicting, time-delay, and stochastic characteristics simultaneously. Song Xiangjun [10] used an extended Petri net to model the obstacle avoidance system of the unmanned vehicle, and such models were converted into corresponding Simulink models. The dynamic behaviors and attributes of the obstacle avoidance system was analyzed through the simulation of MATLAB T. In Thacker’s [11] proposal, they labeled a hybrid Petri net model and proposed an automatic extraction technique that could simplify the model handling the state space explosion problem, which can be used for CPS modeling and verification. Hu Haiyang [12] proposed a compression algorithm to convert OGSPN into a generalized stochastic Petri net (GSPN), through which the CPS was abstracted into several types of objects and its logical structure and working process was visually described. Considering the uncertainty of CPS, Hu used a fuzzy mathematics-based method to process the compressed model of GSPN to improve the accuracy of the performance analysis. A variety of CPN (colored Petri net) models were established to represent fleet maintenance activities and maintenance management, taking into consideration the factors that have a significant impact on fleet maintenance including fleet operation, aircraft failure logic, and component failure processes [13]. Peng Shitong [14] built a transition timed Petri net using the heuristic A* algorithm to deal with the scheduling in remanufacturing scheduling. Jianchao Luo [15] developed a Petri net model that can well deal with all AMS characteristics, and proposed a Banker’s algorithm, like deadlock avoidance policy. Zhang Jing [16] used hybrid Petri nets to model and analyze the operating mechanism of adaptive cruise control system and verified the feasibility of the proposed model. Song Zhenhua [17] proposed a CPS model based on AOP spatial-temporal Petri net, which was successfully applied in the fault detection and repair of a robot system. Tan [18] proposed a CPS real-time event model based on spatial-temporal hybrid Petri nets and analyzed the reliability of the method by modeling a medical control system. Wang [19] used spatial-temporal hybrid Petri nets to build and verify a CPS model. Based on formal modeling methods, Guo [20] analyzed and detected the logic flaw of poor synchronization. To avoid this kind of logic flaw, Guo presented a novel optimized modeling solution based on the synchronization theory of Petri nets and further improved the calculation method of the synchronic distance.

Petri net is a formal graphical model, which can intuitively reveal the essence of the system operation process with a suitable modeling scheme [21,22,23]. Heterogeneous UAV cluster modeling is characterized by deep integration of the discrete process and continuous process, physical process, and computational process. However, most of the current UAV modeling research has only studied a single physical object. There is a lack of studies regarding the characteristics of UAV clusters, and a lack of research work on the formal verification of the practical application of scenario modeling. With the popularization of UAV deployment, the cooperation of multiple UAVs in the cluster has become a prominent problem, which makes it necessary to investigate an integrated modeling method. In order to study the characteristics of the UAV cluster, based on the requirements of intelligent war, this paper studied the model construction method of a heterogeneous UAV cluster, represented by the maneuvering behavior using spatial-temporal Petri nets, and defined the interaction events to solve the integrated modeling problem. The UPPALL tool was used to verify the modeling method. The contributions of this paper are two-fold, as follows.

(1)

A modeling method based on spatial-temporal hybrid Petri nets was proposed. Its high expressiveness allows one to effectively model the complex behavior of the UAV cluster.

(2)

By introducing the labeling mechanism, an external event can be specified to enrich the expressiveness of the model.

2. The Modeling Method of UAV Cluster

The variation in the UAV flight state can be expressed as [24]:

$$u={\left[x_g,y_g,z_g,\theta ,\varphi ,\psi ,p,q,r,V,\alpha ,\beta ,m\right]}^T$$

(1)

where from left to right, the first three attributes are the coordinates, pitch angle, roll angle, yaw angle, roll angular velocity, pitch angular velocity, yaw angular velocity, velocity vector (also divided into three axis velocity components u, v, w), angle of attack, sideslip angle, and mass.

2.1. The Modeling Method of Interaction Event

The UAV cluster can be regarded as a typical cyber physical system including physical space and information space. The interaction of a UAV mission between information and physics can be viewed as the interaction between the perception events and control events. Perception events include the perception of key attributes such as speed, altitude, pitch angle, and roll angle. Control events include maneuvers such as flat flight, acceleration and deceleration, dives, jumps, and combat turns.

2.1.1. Definition of the Perception Event Model

A meta perception event refers to sensors perceiving the key attributes of the UAV. Whether this event occurs is determined only by the numeric value of a key attribute.

Definition 1.

Formal model of a meta perception event:

$$e_s:\tau \langle x,c\rangle$$

(2)

where $e_s$is a class of a meta perception event; $\tau$is the name of the event;$x$is the name of related attributes; $c$is the trigger rule.

Definition 2.

Trigger rules of a meta perception event:

$$\begin{gathered} c:c\&c\left|c^{″}{|}^{″}c\right|!c\left|\left(c\right)\right|a \\ a:f\left(x\right)OPD \\ OP:>\left|<\right|\ge \left|\le \right|==|!= \\ D\in \mathcal{R} \end{gathered}$$

(3)

where $OP$is the operator of the attributes; $D$is a real number; $c$is the trigger rule of a perception event. For example, a UAV performs horizontal acceleration and deceleration maneuvers, $ACC\langle a,a>0\rangle$, where $ACC$is the name of the maneuver, and a is the key attribute. When the value of$a$is greater than $0$, the horizontal acceleration event of $ACC$will be triggered, then the UAV immediately performs a horizontal acceleration maneuver. Since the execution process of the UAV task has temporal and spatial attributes, a perception event model at a certain time and place can be expressed as:

$$ACC\langle a,a=0,l_0\rangle @t_0$$

(4)

where $t_0$and $l_0$represent the temporal and spatial attributes of the perception event, respectively.

The triggering of most maneuvers of an UAV is controlled by multiple key attributes and multiple meta perception events. Based on Definition 1, $x$represents the attribute name related to the combination perception event, and$C$is the set of trigger rules.

The integrated perception event model is defined based on Definition 2.

Definition 3.

Formal model of an integrated perception event:

$$\begin{gathered} e_c:\langle \tau X,C\rangle \\ C:C\&C\left|C^{″}{|}^{″}C\right|!C\left|\left(C\right)\right|a \\ a:g_v\left|X\right|OP|D \\ OP:>\left|<\right|\le \left|\ge \right|==|!= \\ D\in \mathcal{R} \end{gathered}$$

(5)

2.1.2. Definition of the Interaction Event Model

Each maneuver of UAVs is driven by events.

Definition 4.

Formal model of an interaction event:

$$E_i=\left(e_s,Capture,Reactor,e_c\right)$$

(6)

where $e_s$is the perception event in the interaction event; $Capture$is the receiver of the perception event; $Reactor$is the responder of the perception event or the producer of the control event; and$e_c$is the control event in the interaction event. The control event can be defined as:

$$e_c:=\tau \langle Y,N\rangle$$

(7)

$Y$is a set containing multiple key attributes, and $N$is the set of values of the key attribute.

2.2. The Modeling Method of Heterogeneous UAV Cluster System Behavior

A heterogeneous UAV cluster system is a hybrid system with discrete behavior and continuous behavior. There are two kinds of modeling methods for hybrid system. The non-formal method is incomplete because it cannot detect all possible states of the system exhaustively. Formal modeling methods include hybrid automata, hybrid behavior systems, hybrid communication sequence processes, and hybrid Petri nets. Compared with other methods, the hybrid Petri net has the advantages of finite state description, description simplification, and widening application range. Therefore, spatial-temporal factors are introduced into the spatial-temporal hybrid Petri net as a new model to describe the behavior of a heterogeneous UAV cluster system.

Definition 5.

Formal model of heterogeneous UAV cluster system behavior:

$$STHPN=\langle P,T,F,W,M_0,H,E,V,I,A\rangle$$

(8)

where$P$is the finite set of places represented by circular nodes; $T$is the finite set of transitions represented by square nodes; $F$is the set of flow relations represented by directed arcs;$W$is the weight function; $M_{\mathrm{0}}$is the initial identification vector; $H$is a hybrid function; $E$is the set of conditions; $V$is the excitation velocity of continuous transition; $I$represents the time function; $A$is the spatial position.

Definition 6.

There is a one-to-one correspondence between events and discrete transitions. The excitation of discrete transitions indicates the occurrence of corresponding events.

There are both discrete state nodes and continuous state nodes in a spatial-temporal hybrid Petri net, and their interactions are represented by directed arcs. The excitation of transitions indicates the occurrence of corresponding events.

3. UAV Cluster Modeling and Formal Verification

We took the heterogeneous UAV cluster collaborative combat scenario as the object for modeling and used the UPPAAL tool based on time automata to verify the availability, reliability, and real-time capability of the built model to evaluate the feasibility of the modeling method.

3.1. Modeling Instance

We used a heterogeneous UAV cluster combat scenario to verify the modeling method. Suppose that the red side is a heterogeneous UAV cluster system consisting of two reconnaissance UAVS, three attack UAVs and a control center, and the blue side consists of two UAVs. The red side conducts reconnaissance and attack missions against the blue side. The scenario of the attack mission is complex. There will be many situations in the actual attack mission such as weather, equipment, and surrounding environment. This paper assumes that all external factors are ideal, and the whole process of the attack mission can be regarded as a sequence of events.

We will show a modeling instance for an attack mission of a heterogeneous UAV cluster. The attack mission has the following primitive behaviors:

• Search target

The UAV cluster searches the blue side through the event of reconnaissance carried out by reconnaissance UAVs.

• Assign tasks

The control center assigns specific tasks to each UAV.

• Approach target

With the assistance of reconnaissance UAVs, attack UAVs approach the target.

• Target acquired

With the assistance of reconnaissance UAVs, the targets are acquired by attack UAVs.

• Mission complete

UAV cluster complete attack mission.

The heterogeneous UAV cluster system includes reconnaissance UAVs, attack UAVs, and reconnaissance/attack UAVs as well as sensors. The formal expression is shown in Formulas (9) and (10):

$$U=\left(U_{id},U_P\left(D,K,M,R\right),U_b\left(S,A\right),U_{st}\left(Z,T\right)\right)$$

(9)

$$S_n=\left(S_{id},S_P\left(u,v,w,p,q,r,a\right),S_b\left(C_1,C_2\right),S_{st}\left(Z,T\right)\right)$$

(10)

where $D$ is the dynamic attributes; $K$ is the kinematic attributes; $S$ is the reconnaissance behavior; $A$ is the attack behavior; Z is the coordinate of UAV; $T$ is a point or an interval; $C_1$ indicates the change of sensor data; $C_2$ indicates that the sensor data remain unchanged.

• Acceleration sensor

$$\left(S_{ai},S,S_{ap}\left(v,u,w,a\right),S_{ab}\left(C_1,C_2\right),S_{ast}\left(Z,T\right),STHP\right)$$

(11)

• Gyroscope sensor

$$\left(S_{gi},S,S_{gp}\left(p,q,r\right),S_{gb}\left(C_1,C_2\right),S_{gst}\left(Z,T\right),STHP\right)$$

(12)

• Reconnaissance UAV

$$\left(U_{si},U,U_P\left(p_f,p_h\right),U_b\left(S\right),U_{st}\left(Z,T\right)\right)$$

(13)

• Attack UAV

$$\left(U_{ki},U,U_P\left(p_d,p_P\right),U_b\left(A\right),U_{st}\left(Z,T\right)\right)$$

(14)

where $STHP$ represents the spatial-temporal hybrid Petri net; $p_f$ and $p_h$ represent linear flight and steady hover; $p_d$ and $p_P$ are the accelerated dive and sharp rise turn; $Z$ represents the area of reconnaissance/attack or the area where the decision center is located.

Modeling high level behaviors for a UAV cluster executing complex attack mission in dynamic, partially observable, and environments requires a powerful modeling method. The attack mission of a heterogeneous UAV cluster can be described as a Petri net, as shown in Figure 1. The process of the attack mission begins with a reconnaissance event. When the targets are detected, the control center will carry out task assignment. Then, with the assistance of reconnaissance UAVs, the attack UAVs approach the targets. When the targets are acquired by the attack UAVs, an attack action will be carried out. Finally, the process of the attack mission is ended whether the targets are destroyed or not.

The formal model of the attack mission of a heterogeneous UAV cluster can be expressed as Formula (14). $P=\left\{p_1,p_2,\cdots ,p_8\right\}$, places $p_i$ represent the execution phases of the attack mission. $T=\left\{t_r,t_{r\_t},t_{r\_f},\cdots ,t_s,t_f\right\}$, transitions $t$ represent events (i.e., $t_r$ is the reconnaissance event; $t_e$ is the mission complete event. Here, we introduced a labeling mechanism for transitions in the Petri net to specify external events. All transitions may be labeled with conditions that must be verified in order to be fired when enabled. A condition $e$ on the transition $t$ is denoted with $t.e$. If no condition is specified for a transition, we will assume that it is True. $F=\left\{\left(p_1,t_r\right),\cdots ,\left(p_7,t_f\right),\left(t_r,p_2\right),\cdots ,\left(t_f,p_8\right)\right\}$. $W=\left\{{\omega }_i\right\}$, $\omega \left(f_i,f_j\right)=1$, for each $\left(f_i,f_j\right)\in F$. $M_0$ is the initial marking representing a description of the initial state of the attack mission. $M_0=\left\{1,0,0,0,0,0,0,0\right\}$. $H$ is a hybrid function (i.e., the maneuvers of UAV). E is the set of conditions (i.e., $t_{r\_t}.e=True$). V is the firing velocity of continuous transition; I represents the time function; A is the spatial position. The explanation of places and transitions is shown in

Table 1. The explanation of transitions.

Transition	Explanation
$P_1$	Initial state of attack mission
$P_2$	Phase of reconnaissance of attack mission
$P_3$	Phase of task assignment
$P_4$	Phase of approaching target (attack UAVs)
$P_5$	Phase of assistance of approaching target (reconnaissance UAVs)
$P_6$	Phase of acquiring targets
$P_7$	Phase of attacking targets
$P_8$	Attack mission complete
$T_r$	Event of reconnaissance
$T_{r\_t}$	Event of targets detected
$T_{r\_f}$	Event of targets are not detected
$T_{as}$	Event of task assignment
$T_{ap}$	Event of keep effective firing range (attack UAVs)
$T_{aap}$	Event of keep effective firing range (reconnaissance UAVs)
$T_{l\_t}$	Event of targets acquired
$T_{l\_f}$	Event of losing targets
$T_s$	Event of targets are destroyed
$T_f$	Event of failure of the attack mission

.

The state of the attack mission during the execution of the Petri net is given by its marking. Transitions between two states are modeled by transitions in the Petri net (i.e., by evolution of its markings). During the execution of the Petri net of the attack mission, we assumed that UAVs were provided with a set of functions that can evaluate its internal state. These functions were used to evaluate the conditions labelling the transitions of the Petri net and thus determine when and how it is possible to perform such transitions.

Given two markings $M_i$, $M_{i+1}$, a transition from $M_i$ to $M_{i+1}$ is enabled if $\exists t\in T$, so that

(i)

$\forall p\in P$, $s.t.\left(p,t\right)\in F$, then $M_i\left(p\right)>0$;

(ii)

$M_{i+1}\left(p\right)=M_i\left(p\right)-1$ for each $p\in P,s.t.\left(p,t\right)\in F$;

(iii)

$M_{i+1}\left(p^{\prime }\right)=1$ for each $p^{\prime }\in P,s.t.\left(t,p^{\prime }\right)\in F$.

An enabled transition from $M_i$ to $M_{i+1}$ is denoted by $M_i\to M_{i+1}$.

Given two markings $M_i$, $M_{i+1}$, and a situation at time $\tau$, firing a transition from $M_i$ to $M_{i+1}$ in situation $\tau$, if $\exists t\in T$, a transition from $M_i$ to $M_{i+1}$ is enabled and the event condition $e$ labelling the transition t ($t.e)$ is verified in situation $\tau$.

There exists a finite sequence of markings $\left\{M_0,\cdots ,M_n\right\}$ such that $M_0$ is the initial markings, and $M_n$ is the goal marking, which shows that the Petri net of the attack mission is executable.

We used Petri net to simulate the process of the coordinated combat of the heterogeneous UAV cluster. The attack UAVs will execute the attack mission when all the attack UAVs reach the specified position. The collaborative attack/reconnaissance process of the UAVs was mapped in Petri net, as shown in Figure 2.

Figure 2a shows the model of the coordinated attack process; $P_0$ represents that the attack UAVs arrive at the specified area; $P_{ij}$ represents the state of each UAV, $1\le i\le 3,i\in \mathsf{{\rm N}},1\le j\le 3,j\in \mathsf{{\rm N}}$; $i$ is used to identify different attack UAVs. When j = 1, the UAVs will carry out coordinated attack. When j = 2, each of the UAVs will notify the control center of the completion of its own task. $P_4$ shows that the control center receives the message about the completion of the coordinated attack task. $P_6$ represents the end of the coordinated attack mission. $T_{ij}$ represents the state changes of the attack UAVs, $j=1$ represents a coordinated attack task that is assigned, $j=2$ represents a coordinated attack task that is carried out, j = 3 represents that the attack UAVs sends the information of completion of the attack mission to the control center. $T_4$ represents that the control center has received the message that the attack mission has not been completed, indicating that some targets are left undestroyed. $T_5$ shows that all two targets were destroyed. The initial marking $M_0=\left\{3,0,0,0,0,0,0,0,0\right\}$.

Figure 2b shows the model of the coordinated reconnaissance process, $P_0$ shows that the reconnaissance UAVs arrive at the specified area; $P_{ij}$ represents the state of each UAV, $1\le i\le 2,i\in \mathsf{{\rm N}}$; $i$ is used to identify different reconnaissance UAVs; $j$ is used to represent the different states of reconnaissance task, $1\le j\le 7,j\in N$. When $j=1$, reconnaissance UAVs carry out the reconnaissance task, $j\in \left\{2,3,4,5\right\}$ represents the exchange of information between two reconnaissance UAVs, $j=6$ determines whether the current reconnaissance information is fully obtained, $j=7$ shows that the reconnaissance task is complete. The initial marking is $M_0=\left\{2,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0\right\}$.

We used spatial-temporal hybrid Petri nets to simulate the behavior of the individual UAV, as shown in Figure 3.

The UAV completes an attack mission through the following procedures.

• Reaches the specified position through horizontal acceleration maneuver;
• Performs a dive maneuver to reach directly above the first target;
• Performs a horizontal deceleration maneuver to approach the target;
• Performs a chandelle maneuver;
• Performs a zooming maneuver and finishes the attack mission.

The places and transitions in the spatial-temporal hybrid Petri net include discrete and continuous attributes. Place $P_i$ represents the state of different maneuvers of the attack UAVs. Transition $T_i$ shows when the maneuver changes. $M_0=\left\{\left(1,u_0,\right),\left(0,u_1\right),\cdots ,\left(0,u_6\right)\right\}$, 1 represents the token in $P_1$; $u_i$ represents the continuous attributes of UAV shown in Formula (1).

$P_1$ represents the level accelerating, where the speed of the UAV rises from 200 m/s to 300 m/s, and key attributes such as velocity and tangential overload are changed. The velocity $v_1$ of the UAV at time $t_1$ in $T_8$ represents the differential equation for the change in velocity, as defined in Equation (16).

$$dV=\frac{F_x\cos \alpha \cos \beta +F_y\sin \beta +F_z\sin \alpha \sin \beta }{m}$$

(15)

$T_1$ indicates that the horizontal acceleration maneuver has been completed. $P_2$ represents the dive maneuver. The differential equation for the change in the angle of attack is as defined in Equation (17).

$$d\alpha =\frac{F_z\cos \alpha -F_x\sin \alpha }{mV\cos \beta }+q-\tan \beta \left(p\cos \alpha +r\sin \alpha \right)$$

(16)

$T_2$ indicates that the dive maneuver has been completed. $P_3$ represents the horizontal deceleration maneuver, which is like the horizontal acceleration maneuver. $T_3$ indicates that the horizontal deceleration maneuver has been completed. $P_4$ represents the chandelle maneuver. The differential equation for the change in height is as defined in Equation (18).

$$dH=\cos \theta \left(v\sin \phi +v\cos \phi \right)-u\sin \theta$$

(17)

The differential equation for the change in the roll angle is as defined in Equation (19).

$$d\varphi =\left(q\cos \phi -r\sin \phi \right)$$

(18)

$T_4$ represents that the chandelle maneuver has been completed. $P_5$ represents a jump maneuver. $T_5$ represents that the jump maneuver has been completed. $P_6$ represents that the current attack job has been completed. $T_7$ represents the return to $P_4$ as several targets are left unattacked. $T_6$ represents that the individual UAV have completed all of its attacks. $P_7$ represents the end of the attack mission.

The key attributes in the $u$of interaction events include velocity $v$, height $h$, air flow angle of attack $\alpha$, and roll angle $\phi$. Different attribute values represent different events. The modeling of perception events, control events, and interaction events is as follows:

• Model of perception events

$$\begin{gathered} \{e_{speeding}\left(v,v\ge 200\right),e_{subing}\left(\alpha ,\alpha \ge 0\right), \\ {e}_{turning}\left(\left\{h,\varphi \right\},\left(h\ge 2000\right)\&\left(\varphi \ge 30\right)\right)\} \end{gathered}$$

(19)

• Model of control events

$$\left\{e_{speed}\left(v,v\ge 300\right),e_{speed}\left(\alpha ,\alpha =60\right),e_{turn}\left(\left\{h,\varphi \right\},\left(h\ge 3000\right)\&\left(\varphi \ge 60\right)\right)\right\}$$

(20)

• Model of interaction events

$$\begin{gathered} \{\langle e_{speeding},S_v,e_{ctrlsystem},e_{speed}\rangle ,\langle e_{subing},S_{\alpha },e_{ctrlsystem},e_{sub}\rangle , \\ \langle e_{turning},S_h,e_{ctrlsystem},e_{turn}\rangle ,\langle e_{turning},S_{\varphi },e_{ctrlsystem},e_{turn}\rangle \} \end{gathered}$$

(21)

3.2. Formal Verification of the Modeling

In addition to six discrete maneuver action modules including Acc_Action, Sub_Action, Turn_Action, Jump_Action, Attack_Action, Finished_Action, which respectively represent horizontal acceleration maneuver, dive maneuver, chandelle maneuver, jump maneuver, attack maneuver and mission accomplished, there are four continuous attribute modules including Velocity, Height, Roll, Pitch. These modules communicate with each other through synchronous channels. These ten modules are mapped into timed automata templates, where each process in the module corresponds to a location of the template, and each maneuver action corresponds to a synchronous channel of the template. The timed automata is shown in Figure 4.

As shown in Figure 4, circles represent various states of the system, where directed segments with arrows represent transitions of different states in the system, red circles represent the current state, dark blue data are the update of the current state, green data are the conditions for state transition, and light blue data represent the synchronous channel of transmission of the current state.

4. Discussion

We used the UPPAAL tool [25,26] for automatic analysis. The flowchart of instances of the attack mission is shown in Figure 5.

Based on the timed automata template, the key attributes in the process of the heterogeneous UAV cluster attack mission were verified with the help of an UPPAAL tool.

$E<>\left(enemy==2\right)$ illustrates that there is at least one path in the process of completing the attack mission, and two blue targets are destroyed in the end, which verifies the reachability of the model.

$A<>\left(Sub.Sub\_Completeimplyroll\_state==0\right)$ illustrates that the chandelle maneuver followed the dive maneuver, which verified the real-time of the model.

$E\left[\right]\left(h\ge 0\right)$ illustrates that the height attribute in the procedure will never be a negative value.

$A\left[\right]\left(Attack.Attack\_Completeimplyblue==2\right)$ illustrates that all two blue targets are destroyed if the attack mission is complete.

$E<>\left(Acc.Acc\_Complete\right)$ illustrates the existence of a complete state of horizontal acceleration maneuver.

The attributes verified above can represent a certain class of attributes of the events. The verification results are shown in Figure 6. The results show that the model could well represent the process, and all attributes were verified. The model meets the requirements of reliability, accessibility, effectiveness, and real-time performance.

The occurrence of any failure will inhibit the normal mission performance in the physical simulation. This fact leads to the need to consider the security analysis to determine which system has failed and what is the UAV mission phase. Whenever there is a failure in the flight controllers or in the communication, or a combination of failures of these systems, the normal execution of the UAV mission will be interrupted. Such cases were not considered in this article. For future research, this interruption may be represented by a dashed arc (inhibiting arc) in the Petri net. In this situation, the UAV will perform security analysis to identify the flight phase in which the failure occurred.

5. Conclusions

The experience in using a spatial-temporal hybrid Petri net for modeling the attack mission of a UAV cluster has been very effective, providing many advantages over other methods as well as some difficulties that we have dealt with.

This paper focused on representing the heterogeneous UAV cluster combat mission through spatial-temporal hybrid Petri net modeling. First, the modeling and verification of the heterogeneous UAV cluster combat mission was performed, then the dynamic and kinematic equation of the change in key attributes of the heterogeneous UAV cluster were represented, and the formal modeling of the perceptive events, control events, and their interaction event was achieved, extending the single object modeling to various objects modeling for UAVs. This modeling method can effectively represent the fusion of the physical and computational process and information exchange and coordination between each UAV node in the UAV cluster system. Throughout verification, the UPPAAL tool provides an effective framework and environment to demonstrate the reliability, accessibility, effectiveness, and real-time of the aforementioned modeling method.

The main advantage of the spatial-temporal hybrid Petri net is the clear definition of the modeling language and of its semantics in terms of Petri nets. Using such a modeling method guarantees the possibility of using standard tools to evaluate the properties of the model such as liveness and reachability of the goal states. High expressiveness of the spatial-temporal hybrid Petri net allows for effectively capturing and dealing with most of the situations encountered in the research of a UAV cluster.

Although we proposed a modeling method to describe the scenario of the attack mission of a UAV cluster, in order to have a clear specification of the behavior of the UAV cluster, it may still be very difficult to design a model when more and more factors are considered and the dependency across each other becomes more complex. There is no automatic tool to support the conversion between the behavior model proposed in this paper and the simulation verification model, and further research is needed to simplify the connection process between the formal characterization model and the simulation model.