论文标题
无人驾驶汽车控制系统功能的验证框架
Verification Framework for Control System Functionality of Unmanned Aerial Vehicles
论文作者
论文摘要
使用定理证明，为无人机提供了控制系统验证框架。该框架的目的是制定一个程序，以证明飞机数学设计的控制系统满足了稳健性的要求，以确保在不同的环境条件下进行安全性能。以前已经手动执行的广泛的数学派生已在计算机上检查其正确性。为了说明这些程序，利用高阶逻辑交互式定理 - 示威者和自动化定理 - 符号 - 正式验证无人机动力学空间内稳定性域上通用多转机无人机的非线性态度控制系统。该程序的进一步好处是，可以在飞机上实施一些由此产生的方法，以检测其控制器何时由于恶劣的天气条件或执行器/传感器的功能而违反飞行器包络限制。这样的检测程序可用于建议远程飞行员或机上智能代理，以决定计划的飞行路径的某些更改或进行紧急降落。
A control system verification framework is presented for unmanned aerial vehicles using theorem proving. The framework's aim is to set out a procedure for proving that the mathematically designed control system of the aircraft satisfies robustness requirements to ensure safe performance under varying environmental conditions. Extensive mathematical derivations, which have formerly been carried out manually, are checked for their correctness on a computer. To illustrate the proceedures, a higher-order logic interactive theorem-prover and an automated theorem-prover are utilized to formally verify a nonlinear attitude control system of a generic multi-rotor UAV over a stability domain within the dynamical state space of the drone. Further benefits of the proceedures are that some of the resulting methods can be implemented onboard the aircraft to detect when its controller breaches its flight envelop limits due to severe weather conditions or actuator/sensor malfunction. Such a detection procedure can be used to advise the remote pilot or an onboard intelligent agent to decide on some alterations of the planned flight path or to perform emergency landing.
