Experiment on Verification of a Planetary Rover Controller

In this paper, we report an experiment on the verification of the K9 Rover Executive, an experimental platform for autonomous vehicles targeted for the exploration of the Martian surface developed at NASA Ames. The Executive provides a means to control and command the vehicles through predefined plans, that are hierarchical descriptions of actions annotated with real-time constraints. The verification concerns the correctness of the Executive, which must execute the plans according to their semantics.