New Foundational Structures for Engineering Verified multi-UAVs

2011年3月，日本遭遇了最大的地震和毁灭性的海啸。福岛核电站遭受严重破坏，超过10万人在辐射水平变得不安全后不得不疏散。工作人员无法在现场进行操作，使他们无法确保核电站的安全，并避免了一次重大的辐射泄漏。灾难发生一个月后，为了从上方评估核电站受损的严重程度，派出了一辆装有摄像头的小型飞行器来拍摄受灾地区的照片和视频。获得的视频片段为救援队带来了宝贵的信息，否则这些信息是无法获得的。但飞行器的使用仍然受到这样一个事实的限制，即它们需要传输范围内的远程操作员来控制它们。还需要有操作员控制摄像头并解释数据。为了自主工作，这些系统需要高度智能和理性，以便它们能够变得可靠：它们必须具有高水平的知识，以完成在任何其他信息环境中发生的人工智能复杂任务。这意味着它们应该适应任何意想不到的情况，例如没有反映在先前环境信息中的最近变化，以及由于建筑物受阻或室内探索可能造成的GPS丢失；例如，在这种条件下的可靠运行将使它们能够安全地返回基站。在多无人机环境中，他们还应该能够相互通信，以简化他们的目标，从彼此的信息中学习，以及更新和共享他们的知识。鉴于任何任务在部署地区、任务和要实现的目标等方面都是独一无二的，在可能涉及人的生命的意义上可能是至关重要的，因此必须根据正式规格核实执行情况是否正确。一个著名的实现错误和未能遵守规范的例子是1996年阿丽亚娜5号在起飞后立即自毁，原因是由于实现不适合所有可能的情况而导致数字溢出。1996年，洛克希德·马丁/波音公司的暗黑之星长航时无人机坠毁，五角大楼称这是一起“可直接追溯到飞行器建模和仿真缺陷的事故”。为了实现所需的可靠性，我们需要开发一种形式主义，表示每一架无人机在捕获无人机运动约束的同时可以执行的一系列动作。然后，我们将核实使用这种形式主义建模的每一架无人机的行为是否导致它们要实现的任务的个人或总体目标。这些需要从个人行为扩展到多个无人机之间的合作层面。接下来，我们计划将低级代码链接到高级抽象，并通过高级模型检查技术进行验证。最后，将使用逻辑工具对无人机及其环境之间的信息流的学习进行详尽的推理。

In March 2011, Japan suffered from its biggest earthquake and devastating tsunami. Severe damage were inflicted on its Fukushima nuclear plants and more than 100,000 people had to be evacuated after the radiation levels became unsafe. Workers were not able to operate on site, preventing them from securing safety at the atomic power plant and averting a major radiation leak. One month after the disaster, in order to assess the severity of the damage to the nuclear plant from above, a small aerial vehicle equipped with cameras was sent to take pictures and videos of the affected areas. The video footage obtained brought valuable information to the rescue teams that could not have been acquired otherwise. But the use of aerial vehicles still remains limited by the fact that they require a remote operator at transmission range to control them. It is also necessary to have an operator to control the camera and interpret the data.In order to work autonomously, these systems need to be highly intelligent and rational so that they can become reliable: they must have high levels of knowledge to accomplish their AI-complex missions which occur in any other information environment. This implies that they should adapt to any unexpected situations such as recent changes not reflected in prior information on the environment and possible loss of GPS due to obstructing buildings or indoor exploration; reliable operation under such conditions would, for instance, enable them to return safely to their base station. In a multi-UAV setting, they should additionally be able to communicate with each other to simplify their goals, to learn from each other's information, and to update and share their knowledge. Given that any mission is unique in terms of deployment areas, tasks and goals to be achieved, etc., and can be critical in the sense that human lives may be involved, the implementation must be verified to be correct with respect to a formal specification. A famous example of an implementation error and a failure to comply with the specification is the self-destruction of Ariane 5 in 1996 immediately after take-off, caused by a numeric overflow due to an implementation that was not suitable for all possible situations. In 1996, the Lockheed Martin/Boeing Darkstar long-endurance UAV crashed following what the Pentagon called a "mishap [..] directly traceable to deficiencies in the modelling and simulation of the flight vehicle".To achieve the reliability required, we will need to develop a formalism that represents the sets of actions each Unmanned Aerial Vehicle (UAV) can perform while allowing capture of the kinetic constraints of the UAVs. We will then verify that the behaviours of each UAV modelled using this formalism lead to the individual or overall goal of the mission they are to achieve. These need to be extended from individual behaviours to a cooperative level amongst the multiple UAVs. Next, we plan to link the low-level code to high-level abstraction and verify it via advanced model-checking techniques. Finally, logical tools will be used to exhaustively reason about learning as a result of information flow among UAVs and their environment.