Static verification of robotic simulationsRobotics 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 ten-year project involving a large team of researchers in York, and collaborators worldwide (https://robostart.cs.york.ac.uk). RoboChart is supported by RoboTool (https://robostar.cs.york.ac.uk/tools/), 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 RoboStar and the Institute for Safe Autonomy. 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. 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. Resources:
|