Safe-ROS: An Architecture for Autonomous Robots in Safety-Critical Domains

TL;DR

Safe-ROS tackles the lack of formal safety guarantees in ROS-based autonomous robots by introducing a Safety System (SS) with a formally verifiable Safety Instrumented Function (SIF) that oversees a Safety-Related Autonomous System (SRAS). The SIF is implemented as a Gwendolen-based BDI agent and verified using AJPF, with requirements elicited via FRET and translated into an LTL property $G(too_close \rightarrow F(stopped))$, while the orchestrator ensures runtime safety through Dafny-based proofs. The prototype, demonstrated in a nuclear inspection scenario using an AgileX Scout Mini in Gazebo and lab tests, shows that the SS can override SRAS decisions to guarantee a safe state under hazard conditions. This work provides a reusable architectural pattern for safety supervision in ROS-based systems and lays groundwork for extended verification, real-time consideration, and broader domain deployment in safety-critical applications.

Abstract

Deploying autonomous robots in safety-critical domains requires architectures that ensure operational effectiveness and safety compliance. In this paper, we contribute the Safe-ROS architecture for developing reliable and verifiable autonomous robots in such domains. It features two distinct subsystems: (1) an intelligent control system that is responsible for normal/routine operations, and (2) a Safety System consisting of Safety Instrumented Functions (SIFs) that provide formally verifiable independent oversight. We demonstrate Safe-ROS on an AgileX Scout Mini robot performing autonomous inspection in a nuclear environment. One safety requirement is selected and instantiated as a SIF. To support verification, we implement the SIF as a cognitive agent, programmed to stop the robot whenever it detects that it is too close to an obstacle. We verify that the agent meets the safety requirement and integrate it into the autonomous inspection. This integration is also verified, and the full deployment is validated in a Gazebo simulation, and lab testing. We evaluate this architecture in the context of the UK nuclear sector, where safety and regulation are crucial aspects of deployment. Success criteria include the development of a formal property from the safety requirement, implementation, and verification of the SIF, and the integration of the SIF into the operational robotic autonomous system. Our results demonstrate that the Safe-ROS architecture can provide safety verifiable oversight while deploying autonomous robots in safety-critical domains, offering a robust framework that can be extended to additional requirements and various applications.

Figures (5)

• Figure 1: Research methodology: Our approach to incorporating formal methods throughout our safety architecture.
• Figure 2: ROS node graph of the autonomous system. Ovals represent nodes, rectangles denote topics, and arrows indicate message flow. Showing which nodes publish to or subscribe to which topics.
• Figure 3: Integration of SRAS with the SS ( Gwendolen BDI Agent) on the same hardware. Sharing mobile platform, LiDAR percepts, and computational resources, and communicating via java_rosbridge.
• Figure 4: Requirement in FRET. We use FRET to translate the requirement from natural language into Linear Temporal Logic (LTL). For model checking, we use the Future Time interpretation.
• Figure 5: Simulation and physical testing of the implemented architecture