Verifiable Autonomy

Lead Research Organisation: University of Sheffield
Department Name: Automatic Control and Systems Eng


Autonomy is surely a core theme of technology in the 21st century. Within 20 years, we expect to see fully autonomous vehicles, aircraft, robots, devices, swarms, and software, all of which will (and must) be able to make their own decisions without direct human intervention. The economic implications are enormous: for example, the global civil unmanned air- vehicle (UAV) market has been estimated to be £6B over the next 10 years, while the world-wide market for robotic systems is expected to exceed $50B by 2025.

This potential is both exciting and frightening. Exciting, in that this technology can allow us to develop systems and tackle tasks well beyond current possibilities. Frightening in that the control of these systems is now taken away from us. How do we know that they will work? How do we know that they are safe? And how can we trust them? All of these are impossible questions for current technology. We cannot say that such systems are safe, will not deliberately try to injure humans, and will always try their best to keep humans safe. Without such guarantees, these new technologies will neither be allowed by regulators nor accepted by the public.

Imagine that we have a generic architecture for autonomous systems such that the choices the system makes can be guaranteed? And these guarantees are backed by strong mathematical proof? If we have such an architecture, upon which our autonomous systems (be they robots, vehicles, or software) can be based, then we can indeed guarantee that our systems never intentionally act dangerously, will endeavour to be safe, and will - as far as possible - act in an ethical and trustworthy way. It is important to note that this is separate from the problem of how accurately the system understands its environment. Due to inaccuracy in modelling the real world, we cannot say that a system will be absolutely safe or will definitely achieve something; instead we can say that it tries to be safe and decides to carry out a task to its best ability. This distinction is crucial: we can only prove that the system never decides to do the wrong thing, we cannot guarantee that accidents will never happen. Consequently, we also need to make an autonomous system judge the quality of its understanding and require it to act taking this into account. We should also verify, by our methods, that the system's choices do not exacerbate any potential safety problems.

Our hypothesis is that by identifying and separating out the high-level decision-making component within autonomous systems, and providing comprehensive formal verification techniques for this, we can indeed directly tackle questions of safety, ethics, legality and reliability. In this project, we build on internationally leading work on agent verification (Fisher), control and learning (Veres), safety and ethics (Winfield), and practical autonomous systems (Veres, Winfield) to advance the underlying verification techniques and so develop a framework allowing us to tackle questions such as the above. In developing autonomous systems for complex and unknown environments, being able to answer such questions is crucial.
Description A fundamental problem of verifying autonomous intelligent systems (AIS) in unstructured environments is the complexity of ways in which the decision making system of the AIS can interact with the physical environment and other agents in the environment.

1. The project have produced generic theory and algorithm to reduce this complexity to bring nearer the possibility of formal verification and ultimately legal certification of these products. We designed and published the theory of verifiable limited instruction agents (LISA).

2. We have addressed and demonstrated verification of decision making by platoon members on motorways

3. We have addressed the complexity problem of out-of-line of-sight UAS flights and published theoretical paper on the remaining issues to be resolved.

4. We have laid down the foundations of machine learning of reliable decision making by autonomous cars from human drivers on A and B roads and working on an Innovate UK project to transfer the results for industrial use.

5. We have demonstrated the use of theorem proving for verification of control theory based algorithms - a first result of its kind

6. Developed stochastic verification methods for robot cooperation results

7. Developed model checking based verification methods for the logical consistency checks of a single robot before it executes its plans.

8. We have developed error bounds based guaranteed methods of state estimation for autonomous robots (applicable in self localization and mapping).

9. Demonstrated methods on an autonomous electrical van of Tata Motors for autonomous parking that includes finding a parking space.

10. Developed verification of sEnglish behaviour scripts of robots in well defined environments

11. Verifiability of robot reasoning in autonomous arm operations has been developed through abstractions provided by sEnglish scripts of reasoning in the RAIN project.
Exploitation Route The outputs of the two Innovate UK projects will be directly utilised by companies (SysBrain Ltd and MIRA) we are working with.

SysBrain develops UAV software modules for mission verification by the pilot and MIRA transfers pour platoon verification results to their partners.

Demonstrated verifiable autonomous parking, including finding a parking space, on a Tata electrical van that we converted into an autonomous vehicle.
This result has the prospect of being taken forward by some companies.

Demonstration of verifiability of robot arm movements when under intelligent agent control (in the RAIN project).
Sectors Aerospace, Defence and Marine,Agriculture, Food and Drink,Construction,Environment,Manufacturing, including Industrial Biotechology,Transport

Description 1. Impact on legislators for small UAS: the area of small and micro Autonomous Arial Systems' situational awareness-assessment has been addressed in a journal paper and principles of modelling, and complexity reduction for practical purposes, have been developed that raised the interest of the Civil Aviation Authority and currently affects UAV-pilot interaction systems for beyond-visual line of sight systems. Cooperation with SysBrain Ltd helps industrial impact development. 2. Initial impact on industrial development: verifying and certifying vehicle platoons on motorways has been studied and results have been published and are currently being transferred to industry with help from MIRA. 3. In 2018-19 an autonomous electrical van has been demonstrated to find parking space and autonomously park in a parking lot with verifiable system decisions which take into account probabilistic models of the environment containing vehicle pedestrian movements. This project was in part supported by Tata Motors and SysBrain Ltd. 4. in 2021 verifiability of robot arm operations has been ensure using methods developed under this project, via natural abstractions in the agents reasoning script and derived temporal logic.
First Year Of Impact 2021
Sector Aerospace, Defence and Marine,Agriculture, Food and Drink,Construction,Energy,Environment,Manufacturing, including Industrial Biotechology,Security and Diplomacy,Transport
Impact Types Societal,Economic

Description Connected Autonomous Vehicles
Amount £73,000 (GBP)
Organisation Innovate UK 
Sector Public
Country United Kingdom
Start 04/2016 
End 05/2017
Description Contributions to the theory of verification for onboard decisions of unmanned aerial vehicles on BVLOS missions 
Organisation SysBrain Ltd
Country United Kingdom 
Sector Private 
PI Contribution SysBrain Ltd has held an Innovate UK project on "Verification of Decisions by UAVs in Complex Environments" . The EPSRC project "Verifiable Autonomy" contributed by model checking theory to the companies successful software development.
Collaborator Contribution SysBrain Ltd provided the sEnglish Publisher robot reasoning development platform and within that the limited instruction set agent (LISA) architecture. Relative to its 2008 edition this new software was operated from the Eclipse integrated development environment with an sEnglish parser and agent complier to ROS implemented in MATLAB and compiled into an executable module for us by the Eclipse interface. This software has been used by 2 PhD students (Suradet Tantrairatn and Paolo Izzo) , both of whom successfully defended their these and were awarded the PhD. Dr Tantrairatn used the SysBrain software for programming the onboard intelligence of a UAV which is able to re-estimate its dynamics in case of failure mid-flight and develops its new nonlinear feedback controller to continue to fly the plane. This contributed to the verifiably safe autonomous fight of the UAV using SysBrain's Eclipse/MATLAB based software. Dr Izzo has applied probabilistic model checking to verify the reliability of autonomous surface vehicle operations for Thales UK Ltd who using our results.
Impact a CDC 2016 conference paper
Start Year 2015
Description Floow Ltd: driver experience based learning 
Organisation Floow Ltd
Country United Kingdom 
Sector Private 
PI Contribution Providing academic lead in discussion with the company and encouraging them to lead an Innovate UK project proposal where ACSE Sheffield would be the main partner.
Collaborator Contribution Guidance on what useful academic/ industrial research could be done to advance progress towards safe an effective autonomous vehicles appearing on our roads.
Impact Helped formulate Innovate UK proposal, as partners, which was awarded and its project is due to start shortly.
Start Year 2015
Description MIRA: certifiable autonomous vehicles 
Organisation Medicines and Healthcare Regulatory Agency
Department Safety and Autonomy
Country United Kingdom 
Sector Public 
PI Contribution We have investigated the technical challenges and demonstrated solutions to safe decision making by platoons of autonomous vehicles on motorways. We have laid down the theoretical foundations of decision making systems for future autonomous cars, which will be statistically better than the best human drivers in terms of avoiding or being part of accidents.
Collaborator Contribution MIRA so far contributed with insightful discussions about the challenges. (We are planning to go into closer collaboration by using their extensive testing grounds for autonomous ground vehicles.)
Impact We have published academic papers on our platooning solutions. We informed the public in newspaper articles.
Start Year 2014
Description NNL: autonomous robots for the nuclear industry 
Organisation National Nuclear Laboratory
Country United Kingdom 
Sector Public 
PI Contribution Under our Reconfigurable Autonomy EPSRC project we have been working on robustly operating autonomous robot arms for sorting and segregating radioactive materials. The methods have been demonstrated in the laboratories of the Department of ACSE at Sheffield. The challenge is to make these arms to need little servicing, which is expensive in an active environment. The methods we developed will enable long term operation of the robots to self-recofigure and maintain themselves thereby providing much needed continuous productivity. The methods we developed are of key importance to the future profitability and ultimately the survival of the UK's nuclear decommissioning industry.
Collaborator Contribution They enables us to understand the problems of the industry. They provided us case study for our research in the form of the sort and segregate problem of nuclear materials. Currently there is £30k on offer from Sellafield/NNL to transfer our methods onto concrete industrial arms at Workington.
Impact We have produced methodology demonstrators with the help of this collaboration, which we recorded in videos. We have written as series of academic papers on our robot self-reconfiguration methodologies, where we refer to the applicability and importance of our methods for the nuclear industry.
Start Year 2015
Description Network Rail 
Organisation Network Rail Ltd
Country United Kingdom 
Sector Private 
PI Contribution Meetings between research staff at Sheffield University and a team of technologist from Network Rail, lead by Blacktop
Collaborator Contribution Informed us of their application needs for autonomous vehicles in the maintenance of tracks and buildings.
Impact We have developed octo-copter drone platforms in the laboratories of the department of ACSE, which are potentially suitable in the canning applications of Network Rail.
Start Year 2014
Description TATA Motors: reliable autonomous vehicles 
Organisation TATA Steel
Department Tata Motors European Research Centre
Country United Kingdom 
Sector Private 
PI Contribution PhD studentship supervised to work on verification methodologies directly relevant to safe operation of autonomous vehicles to be designed by Tata Motors European Research Centre.
Collaborator Contribution Loan of steer by wire vehicle for development of reliable sensing and control at low speed urban operations of an autonomous vehicle.
Impact 2 PhD studentships, media publicity and Innovate UK award to ACSE Sheffield as part of an industry lead project by Floow Ltd.
Start Year 2014
Description Thales UK: autonomous surface vehicles development 
Organisation Thales Group
Department Thales Research & Technology (Uk) Ltd
Country United Kingdom 
Sector Private 
PI Contribution Developing mission management systems for autonomous surface vehicles using intelligent agent technologies derived from our EPSRC projects on Engineering Autonomous Spacecraft Software and Verifiable Autonomy.
Collaborator Contribution Described their problem, systems and approach they are taking to ASV autonomy.
Impact PhD studentship supported by Thales UK: it produces simulation based demonstration of ASV autonomy at sea.
Start Year 2015
Title TORCSLink 
Description This robot plugin for The Open Race Car Simulator (TORCS) allows you to develop a vehicle control system in MATLAB and Simulink. An example Simulink model is provided which demonstrates an Automatic Cruise Control system. 
Type Of Technology Software 
Year Produced 2015 
Open Source License? Yes  
Impact Used extensively by the collaborators of the Verifiable Autonomy project to design and develop both low level (continuous) vehicle control and high level (discrete, agent based) decision making. Allows for rapid prototyping of systems in a high fidelity environment. Also used by a number of other institutions outside of the collaboration, repository has been forked 4 times by other projects. 
Company Name SysBrain Ltd 
Description The company's strategy, on software development environments for autonomous robots, has been fundamentally influenced by a series of EPSRC research grants, starting from the natural language programming through to latest ROS based design systems of the company where robot decision making is verifiable by design. 
Impact The company's software, sEnglish Publisher, has been given with free licence to PDRAs and research students on all EPSRC research projects of the grant holder. This lead to application developments for autonomous surface vehicles with Thales UK, autonomous van with Tata Motors and to research carried out on autonomous drones at the university using the company's software. There was also an EU proposal with the participation of university partners: University of Surrey and University Liverpool where SysBrain Ltd was a key partner.
Description Public Engagement (Sheffield) 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach Regional
Primary Audience Public/other audiences
Results and Impact 3 day event in different locations across Sheffield City Centre, consisting of talks and hands on demonstrations. Provided a demonstration which illustrated the benefits of an autonomous controller when conducting a complex aerial survey task with a remotely piloted aircraft. Gave members of the public the opportunity to take control of the demonstration, and ask questions about the technology involved.
Year(s) Of Engagement Activity 2015
Description V&V EPSRC Network Workshop 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Postgraduate students
Results and Impact EPSRC Network Workshop on "Modelling of Sensing and Control for Verification of Robots"
Year(s) Of Engagement Activity 2017