Demonstrating SPARK with a Mars Rover (Part 1): Cyber-Physical Systems

The Ada SPARK programming language was designed to facilitate the creation of safety- and security-critical systems. It includes a variety of features like contracts that let developers specify software requirements and specifications.

AdaCore’s Ada Mars Rover Demo platform is a hands-on example of a cyber-physical system (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.

What follows is the first of a four-part series that takes a deep dive into the use of SPARK with our Mars Rover Demo platform.

Using Cyber-Physical Systems

Cyber-physical systems 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.

Writing a Safety Monitor for a Mars Rover!

As an initial step, a new hardware abstraction layer (HAL) was introduced on top of the existing HALs developed for the various pieces of hardware that comprise the Mars Rover. The result is a façade that provides a simplified and unified view of the Mars Rover hardware, a single point at which the hardware can be replaced by a simulator, and an opportunity to introduce the necessary SPARK contracts to enable proof for the rover software.

Once the team completed the work on the HAL, the entirety of the Rover software proved at SPARK silver. That is, SPARK proved the absence of run-time exceptions (AoRTE).

The team wanted to take this a step further and introduced a gold-level property — a functional property about the software that the team could imagine was traced to the Mars Rover requirements. A fairly obvious property suggests itself when considering the Rover: It shouldn’t crash into obstacles. So, the team formalized this property and proved it.

Formalizing the Safety Property

It’s perhaps a bit cheeky to suggest that it's possible to prove the Rover won’t crash into obstacles. Many things can go wrong over which the software has no control: an obstacle could roll into the Rover's path at the last minute; a hardware fault could leave both motors stuck at full power; the sonar could fail to detect an obstacle, etc. So, when the team says, “the Rover cannot crash,” it means the Rover won’t attempt to go forward when it knows there’s an obstacle.

Here’s how to write the safety requirement in natural language:

The Mars Rover shall not proceed straight forward (i.e., directly forward, without turning) when the distance to an obstacle is less than the Safety Threshold.

This maps naturally to a safety monitor: a function that inspects controller inputs and state and verifies that controller outputs remain acceptable. Here, the monitor considers the input representing obstacle distance and the outputs indicating forward motion (both motors with positive power and turn mode set to straight).

Looking at the HAL ("rover_hal.ads"), the Rover is expected to poll the sonar for distance:

The Rover is expected to set the turn mode and the motor power for each wheel:

Given this information, the requirement can be formalized like this:

where the `Last_` prefixes indicate some means to refer to whatever the last value that was retrieved (in the case of the sonar) or set (in the case of the turn and motor powers).

These properties can be validated by examining how the Rover’s controller modes are implemented. In “rover-remote_controlled.adb,” for example, there are sequences of calls to the HAL such as the following:

Providing Getters

If the HAL exposed getters, they could simply be used to express the formalized safety requirement. However, the HAL provides setters only. Getters, therefore, need to be introduced so that they can be referenced in the formalized requirement. SPARK permits this without requiring implementations of the getters, as will be shown. [Note: Other approaches are possible, but this is the most elegant. It follows DRY and avoids YAGNI (getters haven’t been needed to date, so they’re unlikely to be required for non-proof purposes).]

The Turn Getter

SPARK provides the capability to model the behavior of getters using uninterpreted functions and abstract state.

An uninterpreted function is a ghost function that’s declared but never implemented. Abstract state indicates to SPARK that the getter is associated with state, which may change as a consequence of invoking the setter. These constructs are introduced as follows:

First, the abstract state is introduced:

Then, the getter function is declared like this:

This gives the means to talk about the last turn value that was set. Then it can be tied to the model of a getter to the setter, which may be done by updating the setter as such:

The abstract state is used to tell SPARK, through the Global annotation, that the setter changed something that the getter needs to know about. And in the postcondition of “Set_Turn,” it’s specified that when proof code calls “Get_Turn”; the value returned will equal the value given in the formal parameter “Turn.” This declares that “Get_Turn” behaves like a getter should.

The Power Getter

It might be assumed that the getter for motor power can be written in exactly the same way, like this:

Unfortunately, a problem then arises when attempting to prove the following:

The first and third assertions can be proved, but not the second. What’s going on?

Looking closely at “Set_Power,” SPARK has been told how “Get_Power” will behave when called with Side specified — but not that “Get_Power” will continue to return the same value as before when called with any other Side specified. That this should be true is obvious, but without having stated it, SPARK will not assume it. (This is the safe approach; SPARK isn’t doing anything wrong here.)

It’s necessary to adjust “Set_Power” so that it will maintain that relationship. Since there are only two sides, the simplest approach is to do this:

The Distance Getter

For completeness, here’s the getter for “Sonar_Distance” (there’s nothing surprising going on here):