Zenseact Chooses SPARK for Automotive Safety
Zenseact Chooses SPARK for Automotive Safety
Customer success: real results with AdaCore technologies
Customer
Zenseact develops world-leading safety software for passenger cars. As an AI and software company dedicated to revolutionizing car safety, Zenseact designs the complete software stack for autonomous driving and advanced driver-assistance systems. Zenseact strives to end car accidents altogether and create safe roads for everyone.
Challenge
As a company focused on safety, Zenseact recognized the value of using formal verification to increase confidence in the correctness of its software. Unit testing can demonstrate the presence of errors, but not their absence.
Solution
The SPARK tool set comes with the highest level of ISO 26262 certification. SPARK proofs indicate whether any possibility of error exists across all potential execution paths within the code.
Results and Benefits
Zenseact set up a system that runs SPARK tools in CI on every commit, so that proofs are run automatically. For ASIL-D level components, they have automated checks that ensure each requirement is checked by a contract, giving complete assurance that functional requirements are met. This makes it completely unnecessary to create or run unit tests. Removing the need to maintain a large set of unit tests and to verify that these cover the requirements is the main benefit of transitioning to formal verification.
Ready to achieve the same results?
Discover how AdaCore can help you build safe, secure, and high-integrity software tailored to your project’s needs. Speak with our team to explore solutions, pricing, and long-term support options.