Case Study: Runtime Safety Verification of Neural Network Controlled System

TL;DR

This paper demonstrates the application of a reachability analysis tool for real-time safety verification of a neural network-controlled Turtlebot, introducing a controller switching strategy to enhance safety in obstacle-rich environments.

Contribution

It presents a novel runtime safety verification approach using POLAR-Express for neural network controllers in robotics, with a safe switching strategy to improve operational safety.

Findings

POLAR-Express effectively verifies safety in real-time scenarios.

The controller switching strategy improves obstacle avoidance safety.

Experiments validate the approach in a simulated environment.

Abstract

Neural networks are increasingly used in safety-critical applications such as robotics and autonomous vehicles. However, the deployment of neural-network-controlled systems (NNCSs) raises significant safety concerns. Many recent advances overlook critical aspects of verifying control and ensuring safety in real-time scenarios. This paper presents a case study on using POLAR-Express, a state-of-the-art NNCS reachability analysis tool, for runtime safety verification in a Turtlebot navigation system using LiDAR. The Turtlebot, equipped with a neural network controller for steering, operates in a complex environment with obstacles. We developed a safe online controller switching strategy that switches between the original NNCS controller and an obstacle avoidance controller based on the verification results. Our experiments, conducted in a ROS2 Flatland simulation environment, explore the capabilities and limitations of using POLAR-Express for runtime verification and demonstrate the effectiveness of our switching strategy.