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

This is part two of a four-part series highlighting the Ada SPARK programming language that’s designed to facilitate the creation of safety- and security-critical systems. It implements the software for the Ada Mars Rover demo platform.

In this part, we take a slower look at the safety aspects of the system. The code employs Ada contracts that allow the application to be provably correct at compile time via static analysis.

The Safety Property

With getters in place, the team added the safety property to “rover.ads”. This makes it available anywhere in the Rover package hierarchy:

The safety distance is set to 20:

This matches the design of the remote-control mode.

Proving Controller Safety

The monitor is then attached to the controllers, which is done top-down. Contracts are often added to SPARK code bottom-up for proof. However, in this case, it’s easier to think about what’s going on and decide where contracts are needed using a top-down approach, starting with “Rover.Tasks.Demo”.

Although not strictly necessary (since the demo loop never terminates), a postcondition can be added in the “rover-tasks.ads” file like this:

Such an approach ensures that, if the behavior of “Demo” changes and it’s reused in another context, it will leave the Rover in a safe state.

Looking at the body reveals a single loop that executes the autonomous-control mode followed by the remote-control mode, forever. The team added the Loop Invariant like this:

Of course, this doesn’t prove yet: First, the team needs to add “Rover.Cannot_Crash” as a postcondition of “Rover.Remote_Controlled.Run”, first. Since this property is intended to be invariant, it’s also made a postcondition of “Rover.Autonomous.Run”.

Let’s start with the autonomous-control mode, as it’s actually simpler to prove than the remote-control mode!

Autonomous-Control Mode

The postcondition to ”rover-autonomous.ads” is added like this:

A precondition asserts the safety property is unnecessary because the first thing “Run” does is stop everything:

Then a Loop Invariant to the body of “Run” is added:

Again, this won’t prove without a necessary postcondition to “Find_New_Direction”. Since “Find_New_Direction” is local to the body, it can be added like this:

SPARK proves that the postcondition is guaranteed by the body of “Find_New_Direction” without any additional proof annotations at proof Level 1. And SPARK proves the loop in “Run” and the postcondition for “Run” at this point.

Before moving on, however, it should be considered that, since the safety property is meant to be invariant (never violated), the behavior of `Go_Forward` warrants investigation. `Go_Forward` starts by unconditionally commanding the robot to move forward and then enters a loop looking for obstacles. Given this initial motion, forward movement must not occur unless the safety property holds. We’ll make this a precondition of “Go_Forward”.

Why isn't the safety property a postcondition? Let’s look at the loop in “Go_Forward”:

There are two conditions under which Go_Forward exits this loop: (1) if the user presses a button, and (2) if the distance to an obstacle is less than 30 (which is more conservative than the safety threshold). Unfortunately, neither of these conditions on its own is enough to say that it’s safe.

For (1), the Rover could be too close to an obstacle (and still be commanded to move straight forward). For (2), the upper bound on the distance is known, but not the lower bound. We’d have to know that the distance is, e.g., greater than or equal to 20 but less than 30. Vehicle dynamics and the update rate of the sonar may guarantee this, but the information isn't available simply from the code.

Thus, if the team tried to prove the safety property as a Loop Invariant and then as a postcondition, they would not succeed.

[Footnote: This is part of the reason the team doesn’t use a “Type_Invariant” for the safety property. Since a “Type_Invariant” is asserted at subprogram boundaries, it’s both too restrictive (sometimes the software needs to temporarily break the invariant, as seen here) and not restrictive enough ( the invariant must be asserted in critical “Run” loops). Furthermore, a “Type_Invariant” must be attached to a type (as the name suggests). The invariant is asserted over instances of the type at the boundaries of subprograms. For the Mars Rover, the software doesn’t have such an instance that’s passed around — the state is global (and internal to the “Rover_HAL” package). The team would have had to do significant refactoring to use a “Type_Invariant”.]

Arguably, it’s okay that the safety property isn’t established as an invariant or postcondition here. It’s inferred that it’s safe because of the second exit condition, and “Find_New_Direction” doesn’t assume the safety property to do its job.

With the contracts on “Go_Forward” and “Find_New_Direction” in place, SPARK proves everything in “Rover.Autonomous”.

Note: On the way out, the autonomous-control mode stops everything:

This will become important in a moment!

Remote-Control Mode

Both a precondition and a postcondition are added to “rover-remote_controlled.ads” like this:

The precondition gives some confidence that the Rover isn’t already in trouble (although, as can be seen, it’s not as strong as desired, given how the remote-control mode was originally written!).

As above, the safety property in a Loop Invariant is added at the bottom of the loop in the body of “Run”.

And … SPARK can’t prove this — at any proof Level:

When proof failures like this show up, a good approach is to talk through why you believe the property should hold. Let’s look at the loop again:

The distance is read, compared with the safety threshold, and the Up button is released if the Rover is too close to an obstacle. The buttons are then converted into a command, and the turn and motor power are set accordingly. Releasing the Up button should prevent forward motion. This information is contained in the function “To_Command”.

But SPARK’s analysis is modular: It only knows about the current subprogram (and its nested subprograms, if any) and expression functions. On inspection of “To_Command”, it’s neither a nested function nor an expression function. And because it has no contract, SPARK has no idea what it’s doing and assumes that the result could be any valid value of the “Remote_Command” type. In essence, critical information is hidden from SPARK!

To remedy that, let’s turn this into an inline expression function so that SPARK can see what’s happening:

At this stage, it might be expected that SPARK has sufficient information to prove the property. However, when the analysis is run again, SPARK still reports that the loop invariant may not hold.

The structure of the loop is fairly straightforward: All of the information SPARK needs appears to be there — provided that the new command “Cmd” isn’t equal to the old command “Last_Cmd”. If the two commands are the same, though, the Rover continues to operate based on the turn and motor power levels previously set.

In general, SPARK forgets everything that happened in the previous loop iteration when considering the current loop iteration. Only information that’s asserted via Loop Invariants is carried forward into the next iteration. So, SPARK essentially doesn’t know what our getters will return, unless “Cmd /= Last_Cmd”. What should be communicated to SPARK?

Looking at the case statement and recalling our safety property, the following should be remembered:

The intuition is that because the system doesn’t move forward when the safety threshold is violated, it’s only necessary to make sure that, when the safety threshold is violated, it's not going straight with positive motor values. Turning is acceptable, as is proceeding straight in reverse.

With this Loop Invariant, SPARK proves the safety property. Therefore, this Loop Invariant is indeed useful. Unfortunately, it doesn’t prove: SPARK says it may fail in the first iteration (but SPARK does prove that it holds in subsequent iterations, which leads to the belief that it’s probably the right Loop Invariant). Why not?

A useful approach to debugging a proof like this is to consider the relationship between the invariant and the structure of the code. Here, as said above, there are two cases of interest: “Cmd = Last_Cmd” and “Cmd /= Last_Cmd”. The Loop Invariant can be split, expressing these two cases as such:

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:

With this change, SPARK fully proves “Rover.Remote_Controlled” at Level 1. (To fully discharge the proof for the demo, these constraints would need to be added to the postcondition of “Rover.Autonomous.Run”).

It does seem a pity that the Rover has to be stopped to activate the remote-control mode, though. An enhanced version of the demo could allow a user to take control seamlessly by pressing the remote-control button that corresponds to the Rover’s current motion.

A new “Rover_Command” that represents the initial, invalid state of “Last_Cmd”, to better handle the first loop iteration, is introduced. The new command is added like this:

The case statement is then updated to account for the new command by removing the case for “None” and adding a “when others” at the bottom:

These changes ensure that, in the first iteration, “Cmd /= Last_Cmd”, because “To_Command” can never generate this “Invalid” command. As a result, greater flexibility is enabled in how the remote-control mode can be activated while still preserving the safety property. With this change, SPARK fully proves the demo at Level 1.

It’s been demonstrated how to formalize a safety requirement for a simple Mars rover and use it to prove that the controller never issues a command that would cause a collision. They implement the formalism with ghost state and uninterpreted functions that model getters, without altering the executable semantics of the rover HAL.

After attaching the model to the code, they uncover an unstated assumption in the remote-control mode that could have permitted a crash if that mode were reused as a component in a new system. In turn, they correct the remote-control mode to ensure safety regardless of how it’s invoked. Finally, they show that SPARK proves the model at Level 1 with minimal reliance on intermediate assertions.