基于障碍函数与 SMT 求解的八旋翼飞行包线形式化验证
计算机科学中的逻辑
2021-07-02 v1 系统与控制
系统与控制
摘要
本文提出一种对八旋翼平台飞控器安全性进行形式化验证的方法。我们的方法涉及寻找八旋翼状态空间中被视为安全且可证明相对于动力学不变的区域。具体而言，利用指数障碍函数构造期望指令状态附近候选不变区域。这些区域不变性的证明由 dReal SMT 求解器自动发现，其确保八旋翼在一定的误差范围内准确跟踪指令。考虑了旋翼推力卡滞于固定值的旋翼故障，并通过伪逆控制分配器加以处理。控制分配器的安全性在 dReal 中通过检查分配器所需推力从未超过旋翼能力得以验证。我们将该方法应用于一个具体八旋翼实例，并在正常条件及各种旋翼故障组合下验证了控制器的期望指令跟踪特性。
引用
@article{arxiv.2107.00612,
title = {Formal verification of octorotor flight envelope using barrier functions and SMT solving},
author = {Byron Heersink and Pape Sylla and Michael A. Warren},
journal= {arXiv preprint arXiv:2107.00612},
year = {2021}
}