Demonstrating SPARK with a Mars Rover (Part 2): The Safety Property

Now, SPARK says that the first Loop Invariant, where “Cmd = Last_Cmd”, fails on the first iteration. Therefore, the if statement containing the case statement with the Rover commands can be ignored in our debugging. Let’s talk through how the “Run” procedure works again, with this knowledge in mind, and focus on the first iteration of the loop.

The “Run” procedure initializes “Cmd” to “None”. When the loop starts, the buttons on the remote control are polled. Then the value of “Cmd” is copied to “Last_Cmd”, so now “Cmd” and “Last_Cmd” are both “None”. The safety threshold is then checked. If the Rover is too close to an obstacle, the Up button is released. The buttons are then converted to a command, which is assigned to “Cmd”.

It’s possible that none of the buttons are pressed, either because the user isn’t pressing a button or because the user was pressing the Up button, but the Rover was too close to an obstacle. So, it’s possible that “Cmd” will (again) be assigned “None”. Thus, it’s possible that “Cmd = Last_Cmd”. And in that case, the Rover will continue doing whatever it was doing before.

From the information available in this procedure, there’s no reason to assume that the Rover wasn’t previously driving straight forward. And even though the safety threshold was checked, because “Cmd = Last_Cmd”, it’s not going to change the Rover’s turn or motor powers. Therefore, the safety property could indeed be violated in the first iteration. SPARK is correct.

Has a bug been found that could have resulted in the Rover crashing? No, when it comes to the current Rover demo. Recall that, on the way out of autonomous-control mode, everything is stopped, as noted above. This guarantees that when “Cmd = Last_Cmd” in the first iteration, the Rover will (continue to) be stopped, and the safety property isn’t violated.

But SPARK doesn’t know this. And the importance of stopping the Rover when handing off to the remote-control mode isn’t documented anywhere. Therefore, if this module were reused in a different context, this unwritten assumption could be violated, leading to the possibility of an accident. And that sounds far-fetched, there are high-profile examples of exactly this happening in safety-critical systems. So, let’s fix it.

Fixing the Remote-Control Mode

The remote-control mode problem can be fixed in a couple of different ways.

A precondition could be introduced that requires the Rover to be stopped — or in some similarly safe state — before the remote-control mode is called. This could be implemented using the available getters, for example: