Runtime verification of robotic aspects of the Mars rover

Abstract

The Curiosity Mars rover is one of the most sophisticated successfully deployed systems in the history of planetary exploration. With limited autonomy on board, the ground control team makes most of its decisions. Communication from Earth to Mars may cause messages to take between 4 to 24 minutes to transmit according to the orbital position of the planets at the time of transmission. Could the rover move autonomously, it would be able to explore the terrain and collect data significantly quicker. However, one major challenge to the increased use of autonomous exploration in such scenarios is the lack of assurances that its behavior will work as expected. In this dissertation, runtime verification was used to ensure the case study, a sim‐ ulated Curiosity Mars rover, would not execute any commands which would damage the rover. A separate control system was used to decide the next movements it should take and then be monitored by a built‐in monitoring system. The 3 systems communicated between themselves ensuring the next command executed would not damage the rover hence removing the need for ground control to safeguard the rover. The experimental setup confirmed the effectiveness of the proposed RV system. It demonstrated that the RV system outperformed the traditional method of manual ver‐ ification by a significant margin, enabling faster and more efficient command verification without relying on a ground control team for each command. This leaves lots of room for implementing a command system for full autonomy to save in the time delay created by having to communicate between Earth and Mars