This research concerns assuring safety of autonomous robots. A robot is a machine that is capable of performing a complex sequence of steps, in order to achieve some goal. Autonomous robots act independently and do not require the direct intervention of a human operator. For example, autonomous vehicles are cars, lorries, or other road vehicles that are able to drive themselves to a destination without the need for a human driver. Another example are robot carers, that are able to assist elderly or disabled people with every day tasks, such as retrieving items, cleaning, playing games, and so on. Autonomous robots therefore present a number of exciting future opportunities for overcoming societal challenges.
Robots are computer systems, and the software that runs on them is very complex, far more so than a typical desktop, laptop computer, or mobile phone. Such computers have very simple inputs, like keyboard, mouse, and touchscreen. Robots, however, are "cyber-physical systems": they are both computational (cyber) devices, but they also interact with their physical environment. They have both sensors, that allow them to "see", "hear", and "feel" the world, and also actuators which allow them to manipulate objects in the world. For example, a care robot may have arms that it can move, and wheels to move around with. The software as a robot therefore has to be constantly monitoring its environment, and be able to quickly, appropriately, and, most importantly, safely respond to the changing environment.
If we cannot guarantee that a robot carries out its tasks safely, we cannot risk using them, as human injury or even death could result. A recent example concerns a Tesla Model S automated car that was unable to see a large white lorry crossing its path, and ploughed into the side of it killing its driver. Such tragic accidents reveal why safety is an utmost concern.
Our research will employ mathematical and logical techniques in an attempt to demonstrate that a robot is safe to operate in its target environment. We will employ a document called a "safety case" that contains a credible and convincing safety argument. This argument must, of course, be supported by evidence, and our technique will provide this through "model-based design", where computerised models of individual system parts are created as virtual prototypes. Such models can be described using complicated mathematics, such as algebra, differential equations, and probabilistic models. Probability, in particular, is very important since robots need to plan for possible uncertainty in there environment - such as a human being in an unexpected place.
Mathematics allows us to be rigorous - considering a large range of possible scenarios that would be very expensive to test in the real world. However, it is also difficult for a human to do the necessary mathematics manually. We will therefore use software called an "automated theorem prover" to try and show that each of the robot models behaves correctly and safely. This will include new techniques specifically for reasoning about cyber-physical systems.
We will apply our new techniques to a number of industrial problems, gleaned from our a number of robotics companies that we will partner with. This will allow us to provide guidance to them in ensuring their systems are safe. Our hope is that ultimately our project will ensure that robots can be safely introduced into our society, and thus open up a host of exciting future business opportunities.
|