Software at the wheel

Main image credit: 

The automotive industry is undergoing a software-driven transformation. From advanced driver-assistance systems (ADAS) to fully autonomous vehicles, software has become the primary enabler of innovation, functionality, and safety. But as vehicle software grows in scale and complexity, so do the challenges, particularly in ensuring safety in life-critical scenarios.

To address these challenges, the automotive sector relies on ISO 26262—an international standard for the functional safety of electrical and electronic systems in production vehicles. Covering the full lifecycle from concept to decommissioning, ISO 26262 defines processes that systematically reduce the risk of system failures.

At the heart of the standard are Automotive Safety Integrity Levels (ASILs), which classify potential hazards from A (lowest) to D (highest) based on severity, exposure, and controllability. The higher the ASIL, the more rigorous the required development and verification processes.

As software becomes more integral to vehicle systems, traditional testing techniques are no longer sufficient to ensure safety. Even in memory-safe programming environments, subtle errors and design flaws can still lead to vulnerabilities. 

Formal verification offers a mathematically grounded approach to system assurance. Rather than relying on test coverage or simulation alone, formal methods use proofs to verify that a system behaves exactly as specified under all conditions.

There are two primary ways these techniques are being adopted in automotive development:

• Toolchain Integration: Formal methods can be embedded directly into development workflows, enabling automated, continuous verification of safety and security properties throughout the software lifecycle.

• Verified Components: Developers can leverage formally verified building blocks, reducing reliance on potentially vulnerable third-party libraries.

AdaCore’s SPARK language and verification toolset have been purpose-built for high-assurance software. SPARK enables the formal proof of key safety and security properties, eliminating entire classes of runtime errors such as buffer overflows, integer overflows, and data races. 

Particularly well-suited to meeting ASIL-D—the most demanding safety level in ISO 26262—SPARK gives automotive developers a practical way to meet their compliance goals while reducing the cost and complexity of certification.

As automotive systems continue to evolve, integrating formal verification will be essential to delivering the safety, security, and trust that consumers and regulators demand.

AdaCore is your trusted partner for high-integrity automotive software.

For over 30 years, AdaCore has equipped developers with the tools to build safe, reliable, and secure systems. We provide open-source toolchains for Ada, SPARK, and Rust—languages chosen for their relevance and rigor in the safety-critical space.

AdaCore offers a unified development and verification environment across multiple languages and platforms, providing a consistent and reliable toolset. We support high-integrity industries by offering compiler-toolchain and analysis-tool qualification, along with run-time library certification evidence for compliance with industry standards. With a commitment to long-term support, AdaCore ensures the continuity and reliability of its toolchains for decades. Additionally, our open-source toolchains include a software bill of materials (SBOM) and timely vulnerability reports, helping developers maintain secure supply chains and build on a trusted foundation.