Towards Certification of Autonomous Unmanned Aircraft Using Formal Model Checking and Simulation
Towards Certification of Autonomous Unmanned Aircraft Using Formal Model Checking and Simulation
复制标题
使用正式模型检查和仿真进行自主无人机认证
DOI：
10.2514/6.2012-2573
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
Michael Fisher
中科院分区：
文献类型：
--
作者：
M. Webster;N. Cameron;M. Jump;Michael Fisher
在未来几年，无人驾驶飞行器在民用领域的使用预计会增加，特别是用于所谓的枯燥、肮脏和危险的任务。为确保安全运行，无人驾驶飞行器无疑需要某种形式的自主性：通信故障可能会使完全由人操控的无人驾驶飞行器对其他空域使用者造成危险。为了用于民用领域，无人驾驶飞行器必须在一个被称为认证的过程中获得政府监管部门的批准。本文提出了一种基于形式化方法（特别是形式化模型检验）和飞行模拟为自主无人驾驶飞行器的认证收集证据的方法。特别是，对基于理性主体的自主系统进行了研究。可以使用根据自主系统可能接收的不同传感器输入所指定的飞行器物理环境的隐式模型对无人驾驶飞行器的理性主体进行模型检验。然而，当试图针对诸如英国民航局《空中航行条例》等监管文件中出现的物理量对主体进行模型检验时，这会带来困难。本文展示了如何在模型检验器中使用环境的显式物理模型来解决这一问题，以及如何通过与飞行模拟进行比较来验证这个显式物理模型本身。最后，对相关工作和未来工作进行了概述。
Unmanned aircraft are expected to increase in use in civil applications over the coming years, particularly for the so-called dull, dirty and dangerous missions. Unmanned aircraft will undoubtedly require some form of autonomy in order to ensure safe operations: communications failure could render a completely human-piloted unmanned aircraft dangerous to other airspace users. In order to be used for civil applications, unmanned aircraft must gain government regulatory approval in a process known as certification. This paper presents an approach to gathering evidence for certification of autonomous unmanned aircraft based on formal methods (in particular formal model checking) and flight simulation. In particular, rational agent-based autonomous systems are examined. Rational agents for unmanned aircraft can be model checked using implicit models of the aircraft’s physical environment specified in terms of the different sensor inputs the autonomous system may receive. However this presents difficulties when trying to model check the agents relative to physical quantities such as those found in regulatory documents like the CAA Air Navigation Order. It is shown how this can be remedied using an explicit physical model of the environment within the model checker, and how this explicit physical model can itself be verified through comparison with flight simulations. To conclude, an overview of related and future work is given.