Runtime verification of robotic aspects of the Mars rover

The Curiosity Mars rover is one of the most complex and successfully deployed systems in planetary exploration to date, sent by NASA to explore the surface of Mars. With limited autonomy on-board, the ground-control team makes most decisions. 

Communication of messages from Earth to Mars could take between 4 to 24 minutes, depending on the orbital position of the planets at the time of transmission. This time-gap tends to affect the speed at which the rover may react to its environment. If the rover were to move autonomously, it would be able to explore the terrain and collect data significantly faster. However, one major challenge to the increased use of autonomous exploration in such scenarios is the lack of assurances that its behaviour would work as expected.


In this project, runtime verification was used to ensure that the case study ‒ a simulated Curiosity Mars rover ‒ would not execute any commands that would damage the spacecraft. The rover system would decide upon any subsequent movements it should take, and would then be monitored by a built-in monitoring system. The two systems would communicate between themselves, ensuring that the next command executed would not damage the rover. This would eliminate the need for ground control to safeguard the rover, consequently doing away with the time-delay issue.


Monitors were implemented to supervise elements of the rover, in order to ensure that any invalid states reached were stopped, and possibly altered, to allow the rover to continue exploring. For instance, monitors were set up to protect against collisions between the rover and any objects, ensuring that the mast would stop moving beyond a certain angle.

The conclusion reached on the basis of tests run to date, was that runtime verification is a feasible approach in enhancing the exploration of the rover. This was largely due to the fact that communication between systems all
hosted locally on the rover would take effect substantially faster than inter-planetary communication.

Figure 1. Screenshot of the simulated Curiosity rover on Martian terrain

Figure 2. Execution flow of the rover and monitoring systems

Student: Mattea Fenech

Supervisor : Dr Christian Colombo