Improved Run Time Error Analysis using Formal Methods for Automotive Software – Improvement of Quality, Cost Effectiveness and Efforts to Proactive Defects Check

Quality is what determines success or failure. If products are not error-free, reliable and robust, customers will be put off. Criticism is inevitable. Bosch is focusing on this theme and taking appropriate action to improve the quality of automotive software developed for Combustion Engines. Runtime errors most often refer to issues that appear during the execution of a program like array out of bounds and illegally dereferenced pointer. They are important to detect as they may cause critical safety, security or business operation concerns. They can potentially cause the critical systems of high-integrity applications to fail, leading to disastrous results and they have been blamed as the root cause of system failure in high-profile examples in automotive software. This has resulted in identifying run-time error detection as critical field of interest where safety-critical embedded software has to satisfy stringent quality requirements by all contemporary safety standards where no run-time errors must occur. So, formal verification tools such as Polyspace Code Prover and Astrée helps to find all the run-time errors in the tested software. Formal verification is a technique recommended by ISO26262 for software unit verification and for the verification of software integration. In this paper we propose a methodology for integration analysis using formal verification tools to detect the run-time errors proactively. We show how the methodology was automated and implemented in software development flow. The methodology allows the identification of critical run-time defects and code fixes needed on developer side to deliver run-time free software resulting in better software quality. The results from the last year confirm that formal verification can successfully applied for integration verification. This has led to huge reduction in cost and effort by proactively identifying critical defects in software before it reaches final delivery.