CyPhyAssure: Compositional Safety Assurance for Cyber-Physical Systems

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.

Autonomous robot technology promises to provide a variety of societal and economic benefits. Autonomous vehicles, for example, promise to make roads safer, and give better use of transport capacity. However, these benefits can only be harnessed by society if the technology has both public trust, and regulatory acceptance. There can often be understandable scepticism towards the technology, due to its unpredictable nature, and so methods are needed to assure their safety.

The outcome of our project is unified assurance technology that can be applied to engineer safe autonomous robots, which will be validated through application to industrial demonstrators. This assurance platform will have a transformative effect in the field of safety assurance for autonomous robots by harnessing results from automated formal verification to produce safety cases undergirded by specific mathematical guarantees of their consistency and adequacy of the evidence. In particular, our software will provide a potential route to regulatory acceptance for autonomous robots, through the production of internally verified safety certificates. Moreover, automating the safety process provides a means to dynamically re-certify a robot when some of the underlying behavioural models change, perhaps due to machine learning, which could provide the disruptive development of self-certifying autonomous robots.

The economic and societal impacts of this work will be mainly realised through industrial collaboration. Provision of advanced automated techniques for assurance has the potential to open a variety of new markets, by supporting both consumer trust in novel AR technology, and regulatory acceptance. Our industrial demonstrators will enable us to translate our scientific results from academia to industry. Our partners provide us with a broad spectrum of players within the fields of safety, verification, and autonomous systems in the complementary areas of railways, marine, automotive, and aerospace. Through regular collaboration, and supported by our demonstrator repository and technology, our project will have a positive impact on industrial certification. It will reduce time to market, through virtual prototyping, and thus provide cost reduction. It will also improve confidence in correctness of safety cases, improve productivity, and prevent costly corrections at the engineering phase. Our industrial partners will periodically trial our technology and provide feedback to enable appropriate alignment.

Our partners are ClearSy, DRisQ, and UTRC, who will support complementary demonstrators. DRisQ, based in Malvern, are safety and certification experts, with a portfolio of existing formal verification solutions, which have been applied to robotics. They are well placed to both provide requirements to our assurance framework, and also potentially to link with their products. United Technologies Research Centre (UTRC), in Ireland, is the research and innovation division of United Technologies (UTC). UTC is multinational conglomerate that manufactures products in several areas, including the aerospace domain, and own the famous Pratt & Whitney aircraft engine brand. They are therefore experts in certification of large scale aerospace systems, including UAVs. ClearSy, based in France, specialises in the production of safety-critical systems and software, and are experts in railway certification. They have worked on major railway projects in São Paulo, Stockholm, and France, including driverless trains. Successful application our technology within these industries will act as a springboard for future commercial exploitation, such as a start-up company which supports our technology.