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 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 (https://www.cs.york.ac.uk/circus/RoboCalc/). RoboChart is supported by RoboTool (https://www.cs.york.ac.uk/circus/RoboCalc/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 https://www.cs.york.ac.uk/circus/RoboCalc/ and the York Robotics Laboratory.
Prerequisites: This project is ideal for a student interested in modelling and specification, and the application of tools. Programming experience is essential, and a good mathematical background is important.
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 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 (https://www.cs.york.ac.uk/circus/RoboCalc/). RoboChart is supported by RoboTool (https://www.cs.york.ac.uk/circus/RoboCalc/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 https://www.cs.york.ac.uk/circus/RoboCalc/ and the York Robotics Laboratory.
Prerequisites: This project is ideal for a student interested in modelling and specification, and the application of tools. Programming experience is essential, and a good mathematical background is important.
References
RoboChart is described in a reference manual ( http://barom.org.uk/robochart/documents/robochart-reference.pdf).
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. [ bib (https://www-users.cs.york.ac.uk/~alcc/publications/publications_bib.html#MRLCT17)
DOI (https://ieeexplore.ieee.org/document/8206238)
.pdf (https://www-users.cs.york.ac.uk/~alcc/publications/papers/MRLCT17.pdf)]
Recent publication on 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 (https://www-users.cs.york.ac.uk/~alcc/publications/publications_bib.html#MRLCT17)
DOI (https://link.springer.com/chapter/10.1007%2F978-3-319-66845-1_2)
.pdf (https://www-users.cs.york.ac.uk/~alcc/publications/papers/RMLCT17.pdf) ]
Examples of tools that might be considered are SPIN (http://spinroot.com/spin/whatispin.html), nuSMV (http://nusmv.fbk.eu/), and PRISM (https://www.prismmodelchecker.org/).
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. [ bib (https://www-users.cs.york.ac.uk/~alcc/publications/publications_bib.html#MRLCT17)
DOI (https://ieeexplore.ieee.org/document/8206238)
.pdf (https://www-users.cs.york.ac.uk/~alcc/publications/papers/MRLCT17.pdf)]
Recent publication on 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 (https://www-users.cs.york.ac.uk/~alcc/publications/publications_bib.html#MRLCT17)
DOI (https://link.springer.com/chapter/10.1007%2F978-3-319-66845-1_2)
.pdf (https://www-users.cs.york.ac.uk/~alcc/publications/papers/RMLCT17.pdf) ]
Examples of tools that might be considered are SPIN (http://spinroot.com/spin/whatispin.html), nuSMV (http://nusmv.fbk.eu/), and PRISM (https://www.prismmodelchecker.org/).
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
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
Search Suggestions
Based on your current searches we recommend the following search filters.
Check out our other PhDs in York, United Kingdom
Check out our other PhDs in Computer Science & IT
Start a new search with our database of over 4,000 PhDs
PhD Suggestions
Based on your current search criteria we thought you might be interested in these.
Robotic Implants to Control Body Functions
University of Sheffield
Rolls-Royce sponsored PhD Scholarship – Design and Simulation of Stiffness-Adjustable Robotic Systems for Performing on-Wing Repair of Aero-Engines - (ENG 1318X1)
University of Nottingham
Predicting the Uncertainty of Electromagnetic Simulations
University of York
