A Model-based Approach to the Development and Verification of Robotic Systems for Competitions

This paper proposes the adoption of modern Software Engineering techniques in the context of the development of robotic systems. Particularly, we use a design language, RoboChart, and a tool set, RoboTool, which support modelling, verification (via model checking) and simulation of such systems, among other facilities. Our application domain is an Unmanned Aerial Vehicle (UAV) and its control system, targetting at competition challenges. This system needs to be capable to perform navigation tasks in indoor environments and achieve some goals like detecting and finding objects, landing spots and maintaining a stable flight. We emphasise the important role of a design model both concerning formal verification of classical and domain-specific properties and as a basis for a systematic strategy to develop trustworthy implementations.