Formally Verified Switching Logic for Recoverability of Aircraft Controller

Formally Verified Switching Logic for Recoverability of Aircraft Controller
复制标题

飞机控制器可恢复性的正式验证切换逻辑

DOI:
10.1007/978-3-030-81685-8_27
复制
发表时间:
2021
期刊:
International Conference on Computer Aided Verification
影响因子:
--
通讯作者:
Prabhakar, Pavithra
Prabhakar, Pavithra
中科院分区:
--
文献类型:
--
作者:
Lal, Ratan;McKinnis, Aaron;Hauptman, Dustin;Keshmiri, Shawn;Prabhakar, Pavithra

文献摘要

参考文献

相似文献

在本文中,我们研究了一个安全的混合控制器的设计,一个经典的线性二次型调节器(LQR)控制器和一个更智能的人工神经网络(ANN)控制器之间切换的飞机。我们的目标是在控制器之间安全地切换,使得飞机总是在固定的时间内恢复,同时允许ANN控制器的最大操作时间。对于LQR控制器的操作,存在先验的安全区,在该安全区中,飞机永远不会失速、过度加速或超过最大结构载荷,因此,通过在退出该安全区之前切换到LQR控制器,可以保证安全。然而,这种已知的安全区是保守的,因此,限制了人工神经网络控制器的操作时间。我们应用可达性分析来扩展已知的安全区,使得LQR控制器总是能够在固定的持续时间内将飞机从扩展区(“可恢复区”)驾驶回安全区。“可恢复区”延长了ANN控制器的操作时间。我们使用对应于可恢复区的混合控制器进行模拟,并观察到该设计确实是安全的。
In this paper, we investigate the design of a safe hybrid controller for an aircraft that switches between a classical linear quadratic regulator (LQR) controller and a more intelligent artificial neural network (ANN) controller. Our objective is to switch safely between the controllers, such that the aircraft is always recoverable within a fixed amount of time while allowing the maximum time of operation for the ANN controller. There is aprioriknown safety zone for the LQR controller operation in which the aircraft never stalls, over accelerates, or exceeds maximum structural loading, and hence, by switching to the LQR controller just before exiting this zone, one can guarantee safety. However, thisprioriknown safety zone is conservative, and therefore, limits the time of operation for the ANN controller. We apply reachability analysis to expand the known safety zone, such that the LQR controller will always be able to drive the aircraft back to the safe zone from the expanded zone (“recoverable zone") within a fixed duration. The “recoverable zone" extends the time of operation of the ANN controller. We perform simulations using the hybrid controller corresponding to the recoverable zone and observe that the design is indeed safe.
HARE:用于验证非线性混合自动机的混合抽象细化引擎
DOI: --
发表时间: 2017
期刊: International Conference on Tools and Algorithms for Construction and Analysis of Systems
影响因子: --
作者:
Nima Roohi;P. Prabhakar;Mahesh Viswanathan
通讯作者: Mahesh Viswanathan