Heterogeneous Verification of an Autonomous Curiosity Rover

TL;DR

This paper presents a heterogeneous verification approach for an autonomous Mars rover model, combining formal and non-formal methods to ensure system reliability and enable faster, more autonomous decision-making.

Contribution

It introduces a novel heterogeneous verification framework for complex autonomous systems, integrating multiple techniques to verify different system components at various abstraction levels.

Findings

Verification of ROS nodes enhances system reliability.

Heterogeneous techniques provide comprehensive assurance evidence.

Autonomous decision-making can be validated effectively.

Abstract

The Curiosity rover is one of the most complex systems successfully deployed in a planetary exploration mission to date. It was sent by NASA to explore the surface of Mars and to identify potential signs of life. Even though it has limited autonomy on-board, most of its decisions are made by the ground control team. This hinders the speed at which the Curiosity reacts to its environment, due to the communication delays between Earth and Mars. Depending on the orbital position of both planets, it can take 4--24 minutes for a message to be transmitted between Earth and Mars. If the Curiosity were controlled autonomously, it would be able to perform its activities much faster and more flexibly. However, one of the major barriers to increased use of autonomy in such scenarios is the lack of assurances that the autonomous behaviour will work as expected. In this paper, we use a Robot Operating System (ROS) model of the Curiosity that is simulated in Gazebo and add an autonomous agent that is responsible for high-level decision-making. Then, we use a mixture of formal and non-formal techniques to verify the distinct system components (ROS nodes). This use of heterogeneous verification techniques is essential to provide guarantees about the nodes at different abstraction levels, and allows us to bring together relevant verification evidence to provide overall assurance.