Blog
Demonstrating SPARK with a Mars Rover (Part 1): Cyber-Physical Systems
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.
