AdaCore + Automotive

AdaCore’s technology enables developers working on critical automotive applications to improve and streamline their development, verification, and certification processes.

Competition in the automotive industry is intense, and successful companies must constantly innovate by introducing new advances in software. The cars we drive today have large, growing amounts of sophisticated software aboard, controlling everything from the powertrain, to the suspension, braking, and entertainment systems. By some accounts, the number of lines of code in a luxury automobile is greater than the number of lines of code in a modern commercial jetliner.

Accompanying an increase in the complexity of automotive software, in particular when it comes to automated systems such as ADAS or autonomous driving which can have a strong impact on safety, the industry is raising the bar in terms of software quality and assurance. The evolution of the ISO-26262 safety standard is a good indication of this trend. This increase in system reliability requirements comes with an increased cost however. AdaCore solutions are positioned to mitigate this increase and offer alternatives and compliments traditional C development and heavy-testing based processes.

Reduce recalls with cost-effective software assurance.

AdaCore believes that the most cost-effective way to address safety and security needs is to address these requirements as early as possible in the development process, and has designed its toolset to allow software verification to take place as close as possible to the developper’s desk.

AdaCore’s tools and services for automotive are based around two components that can be used either independently or collaboratively:

SPARK is a programming language and toolsuite that allows specification, development and verification of the software in the same language. The introduction of defects is minimized thanks to the  the intrinsic properties of the language. Dedicated static analysis tools can then formally demonstrate the absence of certain categories of defects and compliance of the code to pre-defined specifications.

QGen auto-generates SPARK or MISRA C code from a safe subset of MATLAB Simulink ® and StateFlow ® models. The same code generator can generate consistent code across different versions of Simulink ® and StateFlow ® models, and enforces the use of a safe subset guaranteeing identical behavior between simulation and embedded code.

ISO 26262

ISO 26262 is an international safety standard that encourages the use of system and software development processes to improve the safety of automotive systems. It provides requirements at various levels, through the whole development cycle, articulated around 4 risk levels (or ASIL) depending on the contribution of a given component to the overall safety. A large emphasis is dedicated to the verification processes, which includes activities such as reviews, testing and static analysis at the software level.

Customer Projects: Automotive


    System-on-a-chip Product Lines

    NVIDIA plans to upgrade select security-critical firmware software, rewriting it from C to Ada and SPARK to increase verification efficiencies to achieve compliance with the functional safety standard ISO-26262.


    Automotive Research Project

    AdaCore and the University of Nagasaki successfully completed a joint research project for DENSO, Application of Formal Methods to Help Achieve Freedom from Interference, with the goal of simplifying the development of safety-critical automotive applications in an ISO 26262 context.


    High-Reliability Vehicle Component Research Project

    TOYOTA InfoTechnology Center (ITC) Japan selected the SPARK language and SPARK Pro toolset for a research project to develop a vehicle component implementation that can be proven to be free of run-time errors.

View all customer projects »

AdaCore offers a variety of tools that have been tested and proven across the most demanding industries, making our products the ideal solution for developers that need to build safe, secure and reliable automotive applications.


QGen is a model-based development toolsuite for Simulink® and Stateflow® reduces the development and verification costs for developers of safety- and security-critical applications, through qualifiable code generation, model verification, and tight integration with AdaCore’s qualifiable target emulation and structural coverage analysis tools. The QGen code generator can generate MISRA C, but can also generate the verifiable SPARK subset of Ada, from Simulink® and Stateflow®. By selecting SPARK for code generation, can formally prove important safety and security properties of their software, not only enhancing quality but also decreasing testing costs.


SPARK Pro is a language and toolset specifically designed for developing applications where correct operation is vital for safety or security. The SPARK Pro toolset offers static verification that is unrivalled in terms of its soundness, low false-alarm rate, depth and efficiency. The toolset generates evidence for correctness that can be used to meet the requirements of safety and security certification schemes.

GNAT Pro Assurance

GNAT Pro Assurance includes a specialized service known as sustained branches, which allows a project to continue its use of a specific version of the technology, including upgrades to repair critical issues. It supports all versions of the Ada language standard (from Ada 83 to Ada 2012), and C support is an optional add-on. A full toolsuite is supplied, as well as a configurable run-time library and several specific run-times that are especially suited to high-assurance systems.


CodePeer is an Ada source code analyzer that detects runtime and logic errors. It assesses potential bugs before program execution, serving as an automated peer reviewer, helping to find errors efficiently and early in the development life-cycle. It can also be used to perform impact analysis when introducing changes to the existing code, as well as helping vulnerability analysis. Using control-flow, data-flow, and other advanced static analysis techniques, CodePeer detects errors that would otherwise only be found through labor-intensive debugging.


GNATcoverage allows coverage analysis of both object code (instruction and branch coverage), and Ada or C language source code (Statement, Decision and Modified Condition/Decision Coverage - MC/DC)