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

The article discusses how the Ada SPARK programming language is used to develop safety- and security-critical systems, focusing on a Mars Rover Demo platform as a real-life example of a cyber-physical system. The platform integrates embedded software with hardware components to sense surroundings and act in real-time. The article delves into formalizing safety properties, introducing getters for HAL (Hardware Abstraction Layer), and ensuring the system's integrity. The team demonstrates how SPARK can address safety and reliability issues, emphasizing the importance of formal verification and safety monitoring in high-integrity embedded development.