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. Runtime errors most often refer to issues that appear during the execution of a program like buffer overflow issues and pointer access out of bounds. 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 Static RunTime Analyzer and Advanced Static RunTime Analyzer helps to find all the run-time errors in the tested software. Formal verification along with Abstract interpretation technology 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. The current tools in the market when used without any modifications, results in very high number of false positives e.g. in the order 3000+, these warnings cannot be analyzed by the development team. We have come with tools and methodology to reduce the false positives and give only those few warning in the range 1 to 10 which are real potential defects. The above methodology was automated and implemented in software development flow. This 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 be successfully applied for integration verification. This helps to reduce cost for the development team and focus on the real defects. This has led to huge reduction in costs and efforts by proactively identifying critical defects in software before it reaches final delivery.