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.
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.
Three of AdaCore's signature software development/verification tools for Ada, SPARK and C have been qualified under the ISO 26262 and IEC 61508 functional safety standards.
AdaCore's GNAT Pro compiler and CCG have received TCL3 qualification under ISO 26262, and T3 qualification under IEC 61508. The SPARK Pro verification tool received TCL3 and T2 qualification. All three products have been certified by TÜV SÜD, an independent, globally recognized organization which confirms that products meet national and international standards. The TÜV SÜD certification mark is widely acknowledged and respected as a trusted symbol of quality, safety, and sustainability.
AdaCore has over two decades of certification experience in safety-critical domains such as avionics, space, and rail. By completing the qualification process for automotive and industrial standards, the company has shown that its high integrity technologies can meet the demanding assurance requirements of the software-intensive automotive industry.
Customer Projects: Automotive
Power Steering Control Software
JTEKT demonstrated how to leverage the SPARK Ada language subset and formal methods to facilitate unit testing and verification of the system’s C code to ensure that it was correct.
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.
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)