Verification of system-wide safety properties of ROS applications

Abstract:

Robots are currently deployed in safety-critical domains but proper techniques to assess the functional safety of their software are yet to be adopted. This is particularly critical in ROS, where highly configurable robots are built by composing third-party modules. To promote adoption, we advocate the use of lightweight formal methods, automatic techniques with minimal user input and intuitive feedback.
This paper proposes a technique to automatically verify system-wide safety properties of ROS-based applications at static time. It is based in the formalization of ROS architectural models and node behaviour in Electrum, over which system-wide specifications are subsequently model checked. To automate the analysis, it is deployed as a plug-in for HAROS, a framework for the assessment of ROS software quality aimed at the ROS community. The technique is evaluated in a real robot with positive results.

Biography:

Nuno Macedo is an Assistant Professor of the Faculty of Engineering of University of Porto (FEUP) and a researcher at the High-Assurance Software Laboratory (HASLab) of INESC TEC. He focuses on developing, teaching and applying formal techniques for software engineering with the goal of promoting the development of dependable software. His main research interest is in trustworthy software design, particularly approaches based on lightweight formal methods backed by model checking and model finding. He has also tailored such techniques for the robotics domain to promote the development of safe robotics software.