Integrating formal methods for modelling and simulation of swarm robotics

Ana Cavalcanti delivered a keynote on RoboCalc during iFM 2018.

Abstract

There are many challenging aspects involved in ensuring safety of mobile and autonomous robots. One aspect that has been neglected is software engineering. The state-of-practice uses costly iterations of trial and error, often with hardware and environment in the loop, after an ad hoc use of simulations. It is clear that the modern outlook of the robotic applications is not matched by the outdated practices of design and verification when it comes to controller software.

We present two new domain-specific languages for robotics: RoboChart and RoboSim. They support a model-based approach for early formal validation and sound generation of simulations. In robotics, simulation is the favoured technique for analysis. In our work, simulation is complemented by analysis based on model checking, using CSP, tock-CSP, and the refinement model checker FDR, and theorem proving, using Isabelle/UTP. Our ultimate goal is to support reasoning and code generation using a variety of techniques, but relying on theorem proving to deal with data-rich and large systems, especially with models for swarm applications.

RoboChart is a UML-like notation that includes timed and probabilistic primitives for modelling of controllers. We link it to RoboSim, another graphical notation defined as a gateway between RoboChart models and customised simulations developed for traditional robotics simulators. RoboChart enforces design patterns appropriate to deal with robotic applications and now includes also notation to model collections of robots as present in swarms.

Our approach is predicated on a few principles. First, we adopt notations akin to those in current use by practitioners, namely, notations based on state machines, to ensure usability. Second, we enforce specific architectural patterns relevant for the area, and define precise languages that can be used for automatic generation of mathematical models. Third, our goal is to hide the formalisms from practitioners entirely. Via specialisation and automation, we seek both scalability and usability. Finally, we investigate the integrated use of a variety of techniques together to tackle the different needs of verification and development.