Avis：面向无人机的在位模型检测
软件工程
2021-06-30 v1
摘要
无人机（UAVs）中的控制固件利用传感器建模并管理从起飞、降落至航点间飞行的飞行动作。然而，传感器可能在飞行期间任意时刻失效。若控制固件错误处理传感器故障，无人机可能坠毁、飞离或遭遇其他不安全状况。在位模型检测通过系统性地使传感器失效，寻找可能导致不安全状况的传感器故障。但传感器故障的类型及其在飞行中的时机影响其表现，从而产生巨大搜索空间。我们提出 Avis，一种在位模型检测器，可快速揭示导致不安全状况的无人机传感器故障。广泛使用的控制固件已支持运行模式。Avis 在控制固件于模式间转换时注入传感器故障——这是一个关键的被执行点，此处未被妥善处理的软件异常可触发不安全状况。我们实现了 Avis 并将其应用于 ArduPilot 与 PX4。Avis 发现不安全状况的速度比领先的先进方法 Bayesian Fault Injection 快 2.4 倍。在 ArduPilot 与 PX4 当前代码库中，Avis 发现了 10 个先前未知的导致不安全状况的软件缺陷。此外，我们重新插入了 5 个曾引起严重不安全状况的已知缺陷，Avis 正确报告了全部。
引用
@article{arxiv.2106.14959,
title = {Avis: In-Situ Model Checking for Unmanned Aerial Vehicles},
author = {Max Taylor and Haicheng Chen and Feng Qin and Christopher Stewart},
journal= {arXiv preprint arXiv:2106.14959},
year = {2021}
}