A model-based verification for safe and trusted concurrent robotics systems

Robotics applications involve programming concurrent components
synchronising through messages while simultaneously executing motion
actions that control the state of the physical world.  Today, these
applications are error-prone as they are typically programmed in
low-level imperative programming languages which provide little
support for abstraction or reasoning.

This PhD project develops *model-based verification techniques* for
ensuring the safety and trustworthiness of concurrent robotics.

The model used in this project will be based on models of
concurrent processes, logics for reasoning and programming language
theories. With this model, one can compositionally reason about
complex coordinated robotic control [1] and ensures safety properties
such as:

–*deadlock-freedom* (communication safety), i.e. the robotics system
does not get stuck

–*collision freedom* (physical safety), i.e.
any two components are always separated in space.

The model is integrated into programming languages for robotics
controls [2] and applied to operate real robotics systems — the Smart
Robotics Laboratory at Imperial. For ensuring scalability, our method
establishes a hybrid verification technique, combining both static
(compile time) verification and dynamic (runtime) verification
approaches.  A long-term aim is to contribute to build public trust in
robotics and AI via model-based verifications and programming-based

The state of the art includes the Robot Operating System (ROS, see
www.ros.org), an open-source (mobile) robot middleware stack allowing
to prototype multi-robot communication and interaction–however, it
does not come with any form of assurances, quality of service
monitoring or models of different actors. The proposed project would
thus enable a true step-change in the way multi-robot systems behave
in a safer and more trustworthy way.


The student will develop a model-based verification theory extending
[2] and implement it by integrating existing programming languages
for multi-robot systems [1].
This project strongly inlines EPSRC Cross-Disciplinarity and
Co-Creation Priority: the PhD student is jointly supervised by Stefan
Leutenegger and Nobuko Yoshida at Imperial.

The project will be supported through the availability of the
Robot Arena located at Imperial College’s Department of Computing, a
5x5x5 m workspace including accurate an motion tracking system
facilitating fast testing cycles of complex multi-robot systems.
YEAR 1: Learning basic concurrent models, programming theories and a
basic theory of robotics systems. Design and implement simple use
cases based on a specification and programming languages developed in

YEAR 2: Developing a new model-based technique to specify and reason
behaviours of complex multi-robotics systems compositionally, and
identifying their requirements. The task requires an integration of
logical systems, advanced concurrency models and
programming language theories to capture message-passing between
concurrent components and controls of physical systems.

YEAR 3: Applying the model and verification techniques
by extending the framework developed in [2] and 
integrating into multi-robotics systems located in the Robot Arena.

YEAR 4: Refining the implementation and the theory, expanding the case
studies, and writing up his/her thesis.

[1] Tzoumanikas, Li, Grimm, Zhang, Kovac,
Leutenegger, Fully autonomous MAV flight and landing on a moving target using visual-inertial estimation and model-predictive control, Journal of Field Robotics, 2018,
https://www.doc.ic.ac.uk/~sleutene/publications/jfr_2018_final.pdf (a complex robotic system as operated by the Smart Robotics Lab)

[2] Majumdar, Pirron, Yoshida, Zufferey:
Motion Session Types for Robotic Interactions, the 33rd European Conference on Object-Oriented Programming (ECOOP’19), http://drops.dagstuhl.de/opus/volltexte/2019/10820/

Project ID



Nobuko Yoshidahttps://www.imperial.ac.uk/people/n.yoshida


Logic, Verification