  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.
