Safe and Reliable Concurrent Robotics Programming with Choreographies

PI: Nobuko Yoshida, Imperial College London

A verification system for robotics systems that can faithfully model and uniformly reason about more complex interactions and that scales to larger implementations remains a grand challenge in computer science.

Robotics applications are typically programmed in low level imperative programming languages, leaving the programmer to deal with dynamic controllers affecting the physical state, geometric constraints on components, and concurrency and synchronisation. The combination of these features -control, geometry, and concurrency -makes developing safe robotic applications difficult.

This project investigates a new, safe recovery system with compositional verification framework for concurrent robotics applications. Ensuring the reliability of concurrent robotics systems is highly challenging, as any of the components may fail, buy they must correctly communicate and synchronise with each other under physical constraints.

Our key objective is to combine the verification mechanism of choreographies with the fault-tolerance of robotics software architectures and to guarantee reliability and safety of concurrent robotics systems in the presence of failure.