Department of Computer Science

Systematic automated testing of Robotic Systems based on Formal Models

Rob Hierons

University of Sheffield


Robotic systems form the basis for advances in areas such as manufacturing, healthcare, and transport. A number of areas in which robotic systems are being used are safety-critical and so there is a need for software development processes that lead to robotic systems that are safe, reliable and trusted. Testing will inevitably be an important component.

This talk will describe recent work on automated testing of robotic systems. The work is model-based: it takes as input a state-based model that describes the required behaviour of the system under test. Models are written in either RoboChart [1], a state-based language for robotics, or RoboSim, a simulation language for robotics. These languages have been given a formal semantics, making it possible to reason about models in a sound manner. This talk will describe how the existence of such a formal semantics makes it possible to automate the generation of sound test cases for use in simulation and possibly deployment testing. Testing is systematic since test cases target potential faults. This line of research builds on work on RoboChart and RoboSim [2], within RoboStar, and has the potential to contribute to certification by supporting automated, systematic testing within a simulation.


[1] A. Miyazawa, P. Ribeiro, L. Wei, A. L. C. Cavalcanti, J. Timmis, J. C. P. Woodcock: RoboChart: modelling and verification of the functional behaviour of robotic applications. Software & Systems Modeling. (2019).

[2] A. L. C. Cavalcanti, A. C. A. Sampaio, A. Miyazawa, P. Ribeiro, M. S. Conserva Filho, A. Didier, W. Li, J. Timmis: Verified simulation for robotics. Science of Computer Programming. 174, 1–37 (2019).

Department of Computer Science
Deramore Lane, University of York, Heslington,
York, YO10 5GH, UK
Tel: 01904 325500