FindA University Ltd Featured PhD Programmes
Xi’an Jiaotong-Liverpool University Featured PhD Programmes
Peter MacCallum Cancer Centre Featured PhD Programmes

Model-based engineering in swarm robotics

Department of Computer Science

About the Project

Research areas: Autonomous and self-adaptive systems; Cyber Physical Systems; Formal specification languages, methods and tools;
Real time languages and systems; Safety of autonomous and self-adaptive systems; Software engineering

Robotics is a very exciting area of application; not only it is fun, but it also has potential for huge economic and social impact. A lot has been achieved, and a lot is expect to happen in the next decade or so. Software engineering techniques that provide appropriate and specific support for robot engineers, however, are few and far between.

This project will identify how robot engineers use diagrammatic notations for specification of requirements and designs of applications that use swarm robotics. In this case, we have a collection of robots that work independently, but collaborate in achieving a common goal. The use of a collection permits simpler designs of the units and provides fault tolerant. The project will characterise the modelling notation to be used, and develop support for verification of designs using tools. Verification can cover properties related to interaction patterns and timing and to assumptions about the environment. Existing tools and techniques need to be exploited and specialised to the diagrammatic notation. While we have suggestions for a variety of tools that can be useful, there is scope to explore new approaches.

The work will build on experience and results developed under a five-year project involving a team of seven researchers in York, and collaborators worldwide ( Additional applications and examples are available from the York Robotics Laboratory (

Prerequisites: This project is ideal for a student interested in modelling and specification. Programming experience is essential, and a good mathematical background is important.


We have a tool to deal with single robots:

The tools uses a diagrammatic notation called RoboChart:

P. Ribeiro, A. Miyazawa, W. Li, A. L. C. Cavalcanti, and J. Timmis. Modelling and verification of timed robotic controllers. In N. Polikarpova and S. Schneider, editors, Integrated Formal Methods, pages 18--33. Springer, 2017. [ bib (


.pdf ( ]

Email Now

Insert previous message below for editing? 
You haven’t included a message. Providing a specific message means universities will take your enquiry more seriously and helps them provide the information you need.
Why not add a message here

The information you submit to University of York will only be used by them or their data partners to deal with your enquiry, according to their privacy notice. For more information on how we use and store your data, please read our privacy statement.

* required field

Your enquiry has been emailed successfully

FindAPhD. Copyright 2005-2020
All rights reserved.