Simulation and verification of the Mars Curiosity Rover as described in the NFM 2020 paper.
Videos of the simulation and the runtime verification (click on the image to open the video).
The first video shows the violation of the speed property and the curiosity flips.
The second video shows the correct behaviour using a filtering monitor that removes the erroneous message.