Heterogeneous Verification of an Autonomous Curiosity Rover

R.C. Cardoso, M. Farrell, M. Luckcuck, A. Ferrando, M. Fisher

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review


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 min 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.
Original languageEnglish
Title of host publicationNFM 2020: NASA Formal Methods
Publication statusE-pub ahead of print - 10 Aug 2020

Publication series

Name Lecture Notes in Computer Science


Dive into the research topics of 'Heterogeneous Verification of an Autonomous Curiosity Rover'. Together they form a unique fingerprint.

Cite this