On Modelling, Simulating and Verifying a Decentralized Mission Control Algorithm for a Fleet of Collaborative UAVs

It can be relatively easy to correctly design a centralized mission control algorithm for a fleet of UAVs to achieve optimal mission efficiency. However, the fault intolerance of an algorithm can put the fleet at risk for missions in a noisy communication environment. This paper presents a Decentralized Mission Control (DMC) algorithm for coordinating a fleet of UAVs to accomplish a specific mission. The symbolic model of the UAV fleet configuration and the software processes are applied to the Berkley UAV systems described in [1], and [10], , which facilitate peer-to-peer communication and environmental awareness. The design goal of DMC algorithm is that the UAVs work either cooperatively to achieve the highest efficiency under normal communication modes or adaptively to guarantee the safety of the UAVs under various fault modes. The communication protocol of DMC algorithm mostly relies on message broadcasting in order to minimize the dependency on a ground station. The task assignment schema of the DCM algorithm depends on the modes of the environment variables. It is derived from the Hungary Algorithm [11], which attains the optimal assignment for equal numbers of tasks and agents. A formal method is used to verify the safety and progress properties such as tolerance to faults and freedom from deadlocks. The real-time interactions of the system are modeled as a nexus of UPPAAL automata and are verified against expected properties specified as a list of temporal CTL queries. A C# program is used to simulate and measure the mission efficiency.