On the 29th of September Ana Cavalcanti [presented RoboCalc] to the Formal Aspects of Computing Science Specialist Group (FACS), the British Computer Society (BCS) Specialist Group for practitioners in Formal Aspects of Computing Science.
There are many challenging aspects involved in ensuring safety of mobile and autonomous robots.
Perhaps surprisingly, the engineering of their software needs attention; current practice suffers from costly iterations of trial and error, with hardware and environment in the loop. The modern outlook of the applications is not matched by the outdated practices on validation and verification.
In this seminar, we propose a model-based approach for early analysis and sound generation of (co-)simulations. Simulation is the favoured technique for analysis in this domain, and co-simulation enables the orchestrated use of a variety of simulation tools. Our approach is based on RoboChart, a domain-specific modelling notation with a formal semantics, and on analysis based on model checking and theorem proving to complement simulation. RoboChart is a UML-like notation that includes timed and probabilistic primitives for modelling of controllers.
For modelling of the robotic platform and the environment, we adopt Simulink. Model composition is described using a SysML profile. A CSP-based semantics, used as a front-end for a Unifying Theories of Programming model, formalises RoboChart, Simulink, the SysML profile, and co-simulation based on an industry standard: the Functional Mockup Interface (FMI).