Data modelling in robotic simulations

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 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 a diagrammatic notation to model and simulate data-intensive robotic applications.  It will adopt and extend a domain-specific notation for mobile and autonomous robots called RoboChart. It is being developed under a ten-year project involving a large team of researchers in York, and collaborators worldwide (https://robostart.cs.york.ac.uk). Using RoboChart, we can define packages that specify data used and generated in a robotic system.  This project will investigate how these data structures can be implemented in simulations to ensure that properties defined in RoboChart are checked at runtime during simulation.  

Existing tools and techniques for runtime verification need to be exploited and specialised to RoboChart and to robotic simulators.  While we have suggestions for a variety of tools that can be useful, there is scope to explore new approaches.

Applications and examples are available from RoboStar and the Institute for Safe Autonomy.  

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:

  1. RoboChart is supported by RoboTool (https://robostar.cs.york.ac.uk/tools/) and is described in a reference manual (https://www.cs.york.ac.uk/circus/publications/techreports/reports/robochart-reference.pdf).
  2. Recent publication on RoboChart: A. Miyazawa, P. Ribeiro, W. Li, A. L. C. Cavalcanti, J. Timmis, and J. C. P. Woodcock. RoboChart: modelling and verification of the functional behaviour of robotic applications. Software & Systems Modeling, 18(5):3097--3149, 2019. [ bib | DOI | http ]
  3. JML is an example popular tool for runtime verification:  G. T. Leavens, A. L. Baker, C. Ruby,  Preliminary design of JML: a behavioral interface specification language for Java. ACM SIGSOFT Software Engineering Notes, 31(3):1-38, 2006.