The High-Assurance ROS Framework
This addresses the need for more reliable robotics software for developers using ROS, but it is incremental as it builds on existing static analysis methods.
The paper tackles the problem of improving the quality and reliability of robotics software developed with ROS by introducing the HAROS framework, which uses static analysis to extract models from source code and enables analyses like Model Checking and Runtime Verification, and it has been applied to real-world examples to help developers find and correct issues.
This tool paper presents the High-Assurance ROS (HAROS) framework. HAROS is a framework for the analysis and quality improvement of robotics software developed using the popular Robot Operating System (ROS). It builds on a static analysis foundation to automatically extract models from the source code. Such models are later used to enable other sorts of analyses, such as Model Checking, Runtime Verification, and Property-based Testing. It has been applied to multiple real-world examples, helping developers find and correct various issues.