Improving the reliability of unmanned aircraft used in disaster situations: new grant awarded

Members of the Computer Science Department have been awarded funding by EPSRC (Engineering and Physical Sciences Research Council) for the `New Foundational Structures for Engineering Verified Multi-Unmanned Aerial Vehicles` project.

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, the project team will be working 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,  the project will look 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. The unique feature of our proposal is its cross-disciplinarity nature. It targets the whole cycle of the verification process: from platform details to code-level implementations to  high level  rules and scenarios.

This was a proposal submitted to the EPSRC's recent call on Autonomous Systems and will start in March 2012.    The project is worth about £650K

The primary investigator (PI) on the project will be Daniel Kroening, with co-PIs Mehrnoosh Sadrzadeh and Sonia Waharte (Universities of Oxford and Bedfordshire), along with Stephen Cameron. Michael Tautschnig  working as a research assistant. Our partners on the project include IBM, George Washington University (USA), and professors Prakash Panangaden (McGill University, USA) and Michael Wooldridge (University of Liverpool, UK.)