Postgrad LIVE! Study Fairs

Birmingham | Edinburgh | Liverpool | Sheffield | Southampton | Bristol

University of Bristol Featured PhD Programmes
University of Hong Kong Featured PhD Programmes
Swansea University Featured PhD Programmes
University of Edinburgh Featured PhD Programmes
University of Manchester Featured PhD Programmes

Static Verification of Robotic Applications - identifying how robot engineers can use diagrammatic notations for verification of properties of robots

Project Description

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 can use diagrammatic notations for verification of properties of robots. It will adopt and extend a domain-specific notation for mobile and autonomous robots called RoboChart. It is being developed under a five-year project involving a team of seven researchers in York, and collaborators worldwide (

RoboChart is supported by RoboTool (, which enables the creation of diagrams, and automatic generation of code for verification using a specific tool. Following feedback from the robotics community, this project will explore the use of different tools suitable for verification of different properties, possibly involving time. It will also ensure that the verification is consistent with those already possible using RoboTool.

Applications and examples are available from and the York Robotics Laboratory.

See recent publications on RoboChart in references section.

Research supervision
If successful, you will conduct your research under the supervision of Prof. Ana Cavalcanti ( and Prof. Jim Woodcock (
Ana Cavalcanti holds a Royal Academy of Engineering Chair on Emerging Technologies to carry out work on Software Engineering for Robotics ( The project will contribute to that agenda of work and involve interaction with the industrial patterns in RoboCalc and in a new EPSRC project RoboTest ( and .

Funding Notes

If successful, you will be supported for three years. Funding includes:
£14,777 (2018/19 rate) per year stipend,
Home/EU tuition fees,
RTSG (training/consumables/travel) provision.

1. Apply to study
You must apply online for a full-time PhD in Computer Science.
You must quote the project title (Architectural and Data Modelling for Robotic Applications Studentship) in your application.

2. Provide a personal statement of 500-1,000 words with your initial thoughts on the research topic. A formal research proposal is not required.

NOTE: Applications are processed as soon as they are received.


1. A. Miyazawa, P. Ribeiro, W. Li, A. L. C. Cavalcanti, and J. Timmis. Automatic property checking of robotic applications. In IEEE/RSJ International Conference on Intelligent Robots and Systems, pages 3869--3876, 2017. []

2. 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. []

3. Examples of tools that might be considered are SPIN (, nuSMV (, and PRISM (

How good is research at University of York in Computer Science and Informatics?

FTE Category A staff submitted: 34.80

Research output data provided by the Research Excellence Framework (REF)

Click here to see the results for all UK universities

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
* required field
Send a copy to me for my own records.

Your enquiry has been emailed successfully

FindAPhD. Copyright 2005-2018
All rights reserved.