Automotive Safety Integrity Levels (ASIL)

ISO 26262 is the standard that covers the entire lifecycle of automotive systems, from concept and design to production, operation, and decommissioning. Central to ISO 26262 are its Automotive Safety Integrity Levels (ASIL), which categorize risk into four levels, ranging from A to D, based on the severity, exposure, and controllability of potential hazards. These ASIL levels guide the safety measures required for different components, with higher levels demanding more stringent verification and validation processes.

The determination of ASIL is the result of hazard analysis and risk assessment.In the context of ISO 26262, a hazard is assessed based on the relative impact of hazardous effects related to a system, as adjusted for the likelihood of the hazard manifesting those effects. Each hazard is evaluated in terms of the severity of possible injuries within the context of how often a vehicle is exposed to the possibility of the hazard happening, as well as the relative likelihood that a typical driver can act to prevent the injury.

ASIL D refers to the highest classification of initial hazard (injury risk) defined within ISO 26262 and to that standard’s most stringent safety measures to apply for avoiding an unreasonable residual risk.In particular, ASIL D represents a likely potential for severely life-threatening or fatal injury in the event of a malfunction and requires the highest level of assurance that the dependent safety goals are sufficient and have been achieved.An example of a hazardous condition that warrants an ASIL D level is loss of braking on all wheels.Any product compliant with ASIL D requirements would also comply with any lower level of safety integrity. ASIL C is associated with moderate to high risk, ASIL B is for moderate risk, such as headlights and brake lights, ASIL A is associated with low risk, such as rear lights, and QM relates to non-safety components, such as GPS.

About Formal Methods

Formal methods apply mathematical proofs to software development, offering guarantees that go beyond conventional testing. Instead of extrapolating correctness from a limited number of test cases, formal verification demonstrates that critical properties hold true for all possible inputs.

This capability is especially relevant for higher Automotive Safety Integrity Levels (ASIL C and D), where the consequences of failure are unacceptable. Formal methods can prove:

  • Absence of run-time errors

  • Conformance to functional requirements

  • Secure information flows within the system

In practice, this means that software underpinning emergency braking, steering assistance, or battery management can be developed with mathematical certainty around its safety properties. Something conventional approaches cannot deliver on their own.

What is SPARK

SPARK is a programming language derived from Ada, designed to eliminate undefined behavior and enable formal verification. It restricts certain language features to guarantee determinism and analyzability, while enriching Ada with precise semantics and annotations that allow developers to prove the absence of defects and verify functional correctness. Writing in SPARK means working in a full-featured imperative language that compiles directly to the hardware, delivering formally proven, high-performance code you can trust.

Adopting SPARK

In 2018, Zenseact investigated various formal verification methods, including SPARK, TLA+, Alloy, and Supremica. Following this exploration, SPARK was chosen as the best fit for the certification requirements.

Tamatea McGlinn describes the decision process,

“We needed a way of working that satisfies ISO-26262’s recommendations for components with ASIL C and D requirements. Previously, we had thought this could be done from C++, but the complexity of the language makes this impractical. I realised that high-criticality software in the automotive field faces the same challenges as that in other fields, such as military, aviation, spaceflight, and train-control, which already use Ada and/or SPARK. So why not use it in our cars, too?”

As automotive systems take on ever greater responsibility for human safety, the need for assurance at ASIL C and D cannot be addressed through testing alone. Zenseact’s adoption of SPARK demonstrates how formal methods can play a pivotal role in reducing human error, strengthening evidence for compliance, and achieving the highest levels of software assurance under ISO 26262. By applying mathematically rigorous verification to safety-critical components, Zenseact is not only meeting today’s certification demands but also setting a precedent for how the automotive industry can build trustable, high-integrity software at scale. In a world moving rapidly towards autonomy, formal methods are no longer a theoretical ideal, they are becoming a practical necessity.

For over 30 years, SPARK has been at the forefront of practical, industrial-strength formal methods. SPARK Pro is the culmination of relentless improvements that span coverage of Ada-language features, user experience, and best-in-class automation. There’s never been a better time to get started with deductive formal verification. Explore SPARK and formal methods with AdaCore: https://www.adacore.com/sparkpro