Design and verification for ROS software
Robotics is a very exciting area of application; not only is it
fun, but it also has potential for huge economic and social impact.
A lot has been achieved, and a lot is expected 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 and modern verification techniques (testing,
simulation, and even proof) to develop control software that is to
be simulated and
implemented using a popular middleware for
robotics, namely, ROS. It will adopt and extend domain-specific
notations and techniques for mobile and autonomous robots provided
by the RoboStar
framework
Using RoboStar notations, we can define design
models for general robotic control software, and automatically
generate simulation code, tests, and even models for proof. This
project will further specialise the notations and techniques to the
architecture pattern (based on nodes) and communication paradigm
(publish/subscribe) adopted by ROS. The overall goal is to generate
automatically, and, therefore, at a lower cost, ROS code that is
verified, and is linked to associated artefacts that provides
evidence of quality. This may optionally include the verification of
key components of ROS and work on deployment of ROS applications on
real robots.
Applications and examples are available from
RoboStar
, the YorRobots
network, and York’s
Institute on Safe Autonomy. RoboStar development and
verification is supported by
RoboTool.
Prerequisites: This project is ideal for a student
interested in modelling and specification. Programming
experience is essential, and a good mathematical background is
important.
Resources:
- A. L. C. Cavalcanti, W. Barnett, J. Baxter, G. Carvalho, M.
C. Filho, A. Miyazawa, P. Ribeiro, and
A. C. A. Sampaio.
RoboStar Technology: A Roboticist's Toolbox for Combined Proof,
Simulation, and
Testing, pages 249--293. Springer
International Publishing, 2021. [ bib |
DOI |
.pdf ]
- A. L. C. Cavalcanti. RoboStar Modelling Stack: Tackling the
Reality Gap. In 1st International
Workshop on Verification of
Autonomous & Robotic Systems, VARS 2021. Association for
Computing Machinery, 2021. [ bib |
DOI ]
- A comprehensive list of publications is provided in the
RoboStar
site.
To apply
- You must
apply online for a full-time PhD in Computer Science.
- You must quote the project title ‘Design and verification
for ROS software’ in your application.
- There is no need to write a full formal research
proposal (2,000-3,000 words) in your application to
study, as
this studentship is for a specific project.
|