RoboStar technology - a roboticist’s toolbox for combined proof and sound simulation

Ana Cavalcanti

University of York

Abstract

Simulation is a favoured technique adopted by roboticists to evaluate controller design and software. Often, state machines are drawn to convey overall ideas; they are used as a basis to program tool-specific simulations. The simulation code, written in general or proprietary programming languages, is, however, the only account of the robotic system. In this talk, we present a modern approach to design that supports the automatic generation of simulation code that is guaranteed to be correct, and complements the use of simulation with model checking and theorem proving.

This approach, under development by the RoboStar group (https://www.cs.york.ac.uk/robostar/), uses two domain-specific languages: RoboChart and RoboSim. RoboChart [1] includes a controlled subset of UML-like state machines, a customised component-model, and primitives to specify timed and probabilistic properties. RoboChart is an event-based notation for design; RoboSim [2] is a matching cycle-based diagrammatic notation for simulation. RoboSim also includes block diagrams enriched to specify physical and dynamic behaviours of robotic platforms.

Both RoboChart and RoboSim can be used to generate automatically mathematical models that can be used for verification [3]. In the RoboStar approach, the mathematical models are hidden from practitioners, but can be used to prove properties of models, and consistency between designs and simulations. We have experience with FDR, PRISM, and Isabelle.

RoboChart and RoboSim can complement approaches that cater for a global view of the system architecture by supporting modelling and verification of the functional component-behaviour, covering interaction, time, and probabilistic properties. It also complements work on deployment of verified code.

References

[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).

[3] A. Miyazawa, P. Ribeiro, W. Li, A. L. C. Cavalcanti, J. Timmis: Automatic Property Checking of Robotic Applications. In: The International Conference on Intelligent Robots and Systems. pp. 3869–3876 (2017).