《无人机蜂群共识协议的建模、验证与仿真》200页论文

无人驾驶飞行器（UAV），尤其是电动多旋翼飞行器，在娱乐、运输、物流和军事领域越来越受欢迎。在撰写本报告时，这些飞行器的主要缺点之一是，由于电池技术的限制，其续航能力有限。克服这种局限性的一个常用方法是使用多个飞行器合作实现某个目标。无人驾驶飞行器的这种应用被称为蜂群，多个飞行器可以协调行动，以一定的队形飞行，进入某个具有挑战性的区域，或飞得更远。与任何多组件系统一样，蜂群的复杂性意味着存在多个故障点。高度复杂的实时协调飞行机制所带来的任何不确定性风险都是安全关键行业所无法接受的。关键故障的后果可能是重大的生命损失、财产损失或环境危害。要扩大无人机群的使用范围，确保无人机群的正确行为是必须解决的首要挑战。模型检查是验证系统正确性的最可靠技术之一，它可以通过系统检查所有可能的状态来验证系统的行为。系统验证基于高级模型表示法，可以抽象出实现细节。由于需要投入大量时间和资源，这种软件开发方法并不常用。本文介绍的工作提出了一个框架，用于对具有共同目标的代理分布式系统进行建模、验证并提供正确性证据。具体来说，该框架展示了一个部分自动化的过程，将 UPPAAL 模型检查器中建模的系统在机器人操作系统（ROS）环境中实现。目标系统是一个由无人机组成的蜂群，在通过共识协议实现领导者-追随者分层结构的同时，飞向指定的目标位置。本文提供了将 UPPAAL 结构映射到 ROS 结构的算法表示。最后，还在 Gazebo 3-D 机器人模拟器中模拟了无人机任务的 ROS 实现。