New Foundational Structures for Engineering Verified multi-UAVs

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

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.