Keynotes

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

The development of computerized proofs has led to the development of a variety of set theories and types theories (such as the B set theory, the Calculus of constructions, Simple type theory, etc.) in which these proofs are expressed. After several decades of research on these theories, we understand better their relationship and how proofs can and cannot be translated from one theory to another. This permits to foresee a next step in the development of formal methods, where the same proof can be used in different theories.