RIVERAS: Robust Integrated Verification of Autonomous Systems

Any system used for a safety-critical task, like a pollution-monitoring unmanned aerial vehicle, a robot inspecting a nuclear plant or a human assistive nursebot in a hospital or at home, must have enough evidence to demonstrate its safety before we can use it. Gathering such evidence involves verification, the process of demonstrating that the implementation of a system meets the requirements laid down in its specification. Much work has been done to develop tools and methods for verification of microelectronic designs and software.

When we try to verify an autonomous, intelligent system (AIS), with existing methods, two problems arise:

First, traditional verification techniques rely on a specification that fully defines the functional behaviour of the system to be verified. But, we want to use an intelligent system - one that can adapt to circumstances, deciding what to do without being told exactly how - precisely so we can avoid having to specify a response for every possible scenario. There are usually far too many possible scenarios for this to be practical. Instead, we need flexible specifications expressed in terms of acceptable and required behaviour with associated precise limits for critical properties complemented by more vague indications of desired actions.

Second, the control software to achieve dynamic adaptation is very complex, using iterative optimization algorithms to combine discrete and continuous decision-making. Although there has been much research on how to design these algorithms, their verification is still an open research question.

The RIVERAS project aims to tackle both of these problems.

First, we will develop a way of verifying a system with a flexible specification. This will require a formal way to write a specification, using a modelling language that can capture these flexible requirements. Then, fuzzy concepts will be used to analyse how well we meet the specification. Fuzzy concepts are graded and properties or statements involving them are true (or false) to some degree. This means that specifications may only be partialy satisfied which introduces new challenges when verifying them.

Second, we will also develop ways of verifying control software that uses optimization, which is a general approach for making decisions. Given a cost model and a set of constraints that define permitted limits, an optimizer finds the best set of decisions to maximize or minimize the cost while staying within permitted limits. Most planning problems for intelligent systems can be expressed in the form of optimization and research on control theory proves properties that help us understand how well it should work. We will use the properties established with control theory as a specification to demonstrate that the optimizer software does what it should. Moreover, we will integrate these properties into the software. This allows us to detect, contain and correct failures should they occur.

Finally, we will integrate all these developments into an innovative "Design for Verification" (DFV) method. Engineers who use our DFV methods when specifying and designing an intelligent system, and when producing its optimization-based control software, will immediately be able to use our verification methods to determine if they have done it right. This will be far easier and a lot more efficient than designing it first, without thinking about verification, and then figuring out how to verify afterwards.

To help refine our methods and to evaluate them afterwards, RIVERAS will try them out on real robots. For example, we will design an intelligent exploration system for a Mars rover, implement it on a robot on Earth, and produce all the verification evidence to demonstrate it works as intended.

The economic impact of this work comes from the UKs ability to exploit its results as it becomes a world leader in intelligent systems. The potential for this impact is highlighted by the industrial support for the Call for Proposals. The capacity to verify the behaviour of real-time decision making systems is a prerequisite for their use in many safety-critical applications. This certainly includes the four scenarios described in the Call for Proposals, in which the need for greater autonomy and flexibility must be balanced with strict requirements for safe operation. Indeed the importance of verification is recognized by EPSRC who have identified it as an area for growth in their recent Shaping Capability Policy. The verification capability developed by RIVERAS will boost the prospect for intelligent systems in safety critical market sectors. It also enables the mass production of the next generation of intelligent consumer gadgets and toys, unlocking huge market potential.

The social impact of this research comes from enabling the deployment of more autonomous intelligent systems in a wider range of missions and environments. This will reduce risk to humans operating in hazardous environments while extending capabilities in those environments in which it is impractical or too costly to deploy manned or human operated systems. It will also enable new opportunities such as human assistive robots, public safety applications, and the enormous potential of space exploration. We will engage with the industrial partners throughout the project and especially with regards to the case studies. In particular, knowledge exchange will take the form of input from partners regarding the selection of relevant test problems, and output to partners of research results. A contribution in kind has been requested for time and expertise from the industrial partners as well as travel funds for the necessary visits. We are also requesting access to simulation and experimental facilities where appropriate. Indeed, this goal of integrating our techniques with an industrial partner's platform, such as a robotic rover, provides avenues for direct industrial exploitation of the work. Overall the team has a strong track record in industrial engagement. In particular, Dr Eder's close collaboration with the local and international microelectronics design industry is evidenced in numerous collaborative projects.

A further societal impact is improved public perception of autonomous systems, which are often portrayed negatively in the public arena using terms like "Killer Drone". In reality, however, human-robot interaction offers great promise, such as assisted independent living, more economic services and improved public safety, e.g. when used by fire and rescue services. Close interaction with these robots will necessitate a degree of compatibility with us to ensure safety and dependability, requiring negative perceptions to be challenged. This challenge strays beyond engineering and includes ethical, legal and societal questions. Should intelligent systems imitate human behaviour? Who is liable when the system makes a mistake? Our proposal can contribute to this important debate. We aim to embed the same rigorous safety verification culture in autonomous systems as is found in aviation, whose safety is held in high regard by the public. This impact will be facilitated by Bristol's STAARS (Safe and Trustworthy Autonomous Assistive Robots) initiative, bringing together researchers from law, psychology and robotics with members of the RIVERAS team.

The fields of autonomous systems and robotics need a new generation of researchers who possess specialist knowledge and expertise combined with an understanding of how this expertise fits within the broader endeavour of designing and building intelligent systems. The two researchers employed on the project will develop a set of sought-after skills highly valued by both industry and academia.