This is Part 3 of the four-part series on how the SPARK programming language was used to manage and control a model Mars Rover robot. This article looks at the improvements using Ada’s contract support in SPARK to improve the support for this cyber-physical system.

Using Cyber-Physical Systems (CPS)

Cyber-physical systems (CPS) are integrated solutions that combine computation with physical processes, blurring the boundaries between the digital and physical worlds. They rely on tight interaction between software, networking, and mechanical or electronic components, often using sensors, actuators, and embedded systems to perceive, analyze, and influence their environment. Examples span a wide range of industries, including smart grids, autonomous vehicles, medical monitoring, industrial control systems, robotics, and avionics.

Because they coordinate sensing, computation, and actuation, CPS is an ideal framework for understanding the challenges and opportunities in high-integrity embedded development.

Our new Ada Mars Rover demo platform is a hands-on example of a CPS in action. Like real-world rovers, it integrates embedded software with hardware components to sense its surroundings, process data, and act accordingly — all in real-time. Beyond showcasing the principles of CPS, the project is designed to highlight the strengths of the SPARK language and tools for developing high-integrity software in safety- and mission-critical domains.

Stage 2: Improving the System

Following this initial work, the team was inspired to take another look at what he was proving. In this section, Tony Aiello takes things a step further.

Tony was increasingly unhappy with this loop, in “Autonomous_Mode.Run”:

The loop invariant states that the Rover.Cannot_Crash, so we know that the Rover isn’t in an unsafe state _at that point_ — but the team didn't like their failure to assert the safety property after “Go_Forward” (“Rover.Cannot_Crash” isn’t a postcondition of “Go_Forward” here). They proved that, after finding a new direction, the Rover would be in a safe state. However, they didn’t prove that after going forward, the Rover would be in a safe state.

This was addressed in stage one by making an informal argument about the vehicle dynamics and its impact on the correctness of the code:

Now, this is a valid approach to dealing with code that depends on real-world assumptions which can’t be checked in software. But it felt unsatisfying for this demo. In this section, the Rover demo is updated to formalize the informal argument made in the prior section.

The result is a more satisfying autonomous mode that does a better job of guaranteeing that the Rover can’t crash.

Proving “Go_Forward”

Here’s the complete “Go_Forward” subprogram from before (with a couple of the magic numbers replaced by constants):

It would be great to prove that the Rover is safe during the loop and when the subprogram returns. “Rover.Cannot_Crash” should be added to the postcondition and as a loop invariant. The loop invariant should be placed after the second exit statement, like this:

SPARK will prove the loop invariant: At that point in the loop, it’s assured that Distance is greater than 40, which is greater than our safety threshold of 20.

However, SPARK can’t prove the postcondition. Execution may exit when the measured distance falls below 40, but, as noted in the previous section, there’s no guarantee that the Rover remains above the safety threshold of 20. The Rover could be moving quickly enough for the distance to drop from, for example, 41 to 19 in a single loop iteration. Additional information is therefore required.

Unfortunately, the additional information needed doesn’t exist anywhere in the software. Instead, this extra information is a physical property of the system — the Rover simply isn’t able to move fast enough on its own so that it could close the difference between the distance and safety thresholds in 40 ms. The design of software depends on this fact, which needs to be communicated to SPARK.

One option is to use an assumption. An assumption — unlike an assertion — will not be proved by SPARK. SPARK will simply use the assumption to help prove subsequent checks. The assumption can be added like this:

But… this still doesn’t prove! Why not?

Two exit statements are in the loop.

There can be confidence that the postcondition at the second exit statement has been addressed, because of the new assumption. But the first exit statement remains unaddressed. (This can be verified by asserting “Rover.Cannot_Crash” just before the first exit statement; SPARK will fail to prove this assertion.)

To do this, the precondition on “Go_Forward” needs to be strengthened. The Rover must be in a safe state, but “Rover.Cannot_Crash” is too weak to enable us to prove “Rover.Cannot_Crash” as our postcondition at the first exit, the first time around the loop. Why? Because “Rover.Cannot_Crash” is true if the sonar distance is greater than the safety threshold, OR it’s not moving straight forward.

Therefore, the precondition holds if, e.g., it’s moving backwards and the sonar distance is 5. But then the first thing “Go_Forward” does is start moving forward. If it took the first exit, it wouldn’t be safe anymore. (Moreover, our assumption would definitely be invalid in this case!)

So, the precondition should replace “Rover.Cannot_Crash” with the stronger expression “Rover_HAL.Get_Sonar_Distance >= Rover.Safety_Distance”.

Now SPARK can fully prove “Go_Forward”, given the assumption that was added.

Relaxing the Assumption

While this works, I don’t like it. As we just saw, assumptions are a bit dangerous. Since SPARK can’t check them, it’s far too easy to assume something that just isn’t valid. (It’s also sometimes easy to assume something that’s trivially false, which has disastrous implications for the remainder of the analysis, since in logic False → False is True.)—Tony Aiello, AdaCore

First, assuming “Distance >= Rover.Safety_Distance” outright is far too strong. If an error were made in defining “Sonar_Sampling_Delay” and set to 400 ms or 4000 ms, would the Rover still be safe? There’s an implicit understanding of the Rover’s dynamics that informed the belief the code was correct; instead, that understanding could be encoded explicitly.

The Rover must have a maximum speed that it can achieve. Let’s define “Max_Speed” to be 0.5 units per millisecond. It’s actually been measured to be 0.012 units per millisecond. In the final code, we set “Max_Speed” to 0.015 for a bit of additional margin — we don’t need to squeeze all of the possible performance out of the system

It then becomes possible to compute the maximum distance the Rover could travel within a given number of milliseconds and use this in the assumption instead. By recording the last distance measurement, one can state: “Distance >= Last_Distance - Sonar_Sampling_Delay * Max_Speed”.

Taking types into account, the assumption can be rewritten as:

To do this, it’s necessary to introduce “Last_Distance”, declared as “Ghost” (since it’s required solely for proof). An initial value for “Distance” is also needed, as it will be read (to assign to “Last_Distance”) prior to polling the sonar. Initialization should set “Distance” to “Rover.Safety_Distance”, as specified in the precondition.

When the proof is repeated, it fails: SPARK can’t prove the postcondition. If “Rover.Cannot_Crash” is asserted before the second exit statement, it becomes evident that this is the path along which SPARK is unable to prove the postcondition. The assertion can’t be proved, but SPARK does prove the postcondition under the assumption that the assertion holds.

Intuitively, the failure to prove the assertion indicates that “Last_Distance” is the problem: SPARK is told that the distance to the obstacle is greater than a function of “Last_Distance”, but SPARK’s clearly not seeing that this relationship is as strong as needed.

The intuition can be confirmed by strengthening the assertion to “Distance >= Rover.Safety_Distance”, which SPARK can’t prove. Further confirmation that the problem is “Last_Distance” is accomplished by adding an assertion about “Last_Distance” in front of the assumption.

You need to know that “Last_Distance >= Distance_Threshold” for the assumption to establish that “Distance >= Rover.Safety_Distance”; if asserted, SPARK can’t prove it. Three changes are needed to fix it.

First, because “Last_Distance” is assigned the value of “Distance” that was constrained in the _prior_ iteration of the loop, the constraint on “Distance” must be expressed as a loop invariant. (Remember that, in SPARK, loops represent cut points in the analysis for any variables assigned during the loop. Only type properties and properties established in loop invariants are carried from one loop iteration to the next.)

Accordingly, “Distance >= Distance_Threshold” is added as a new loop invariant, next to “Rover.Cannot_Crash”. This ensures that SPARK will know that “Last_Distance >= Safety_Threshold” on subsequent loop iterations.

But what about the first iteration? This leads to the second and third changes. The precondition must be strengthened from “Rover_HAL.Get_Sonar_Distance >= Rover.Safety_Distance” to “Rover.Get_Sonar_Distance >= Distance_Threshold” and the initialization of “Distance” must be updated to match. It will ensure that, on the first iteration, “Last_Distance >= Safety_Threshold”.

With these changes, when SPARK is rerun, the postcondition is proved.

It would be possible to stop at this point, but retaining this assumption in the code remains undesirable. The presence of a validation-worthy assumption isn’t immediately evident, and reusing this dynamics model elsewhere would require repetition.

Fortunately, SPARK has the tools to modularize these kinds of assumptions.

Modularizing the Assumption

The assumption is modularized in the same way that we might introduce a lemma or describe the contract on a binding to another language: Declare a procedure whose postcondition is the assumption and mark it Ghost and Import.

Since SPARK’s analysis is modular, when this procedure is called, SPARK will assume the postcondition whenever the precondition (which is empty here) is met. The assumption in “Go_Forward” can now be replaced with a “call” of this Ghost procedure.

Here’s the final form of “Go_Forward” that incorporates all of the changes and is fully proved: