This content is not included in
your SAE MOBILUS subscription, or you are not logged in.
Improved Run Time Error Analysis Using Formal Methods for Automotive Software - Improvement of Quality, Cost Effectiveness and Efforts to Proactive Defects Check
Technical Paper
2021-26-0459
ISSN: 0148-7191, e-ISSN: 2688-3627
This content contains downloadable datasets
Annotation ability available
Sector:
Language:
English
Abstract
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.
Topic
Citation
Anandapadmanabhan, I., "Improved Run Time Error Analysis Using Formal Methods for Automotive Software - Improvement of Quality, Cost Effectiveness and Efforts to Proactive Defects Check," SAE Technical Paper 2021-26-0459, 2021, https://doi.org/10.4271/2021-26-0459.Data Sets - Support Documents
Title | Description | Download |
---|---|---|
Unnamed Dataset 1 | ||
Unnamed Dataset 2 | ||
Unnamed Dataset 3 |
Also In
References
- Kästner , D. , Mauborgne , L. , and Ferdinand , C. Detecting Safety- and Security-Relevant Programming Defects by Sound Static Analysis The Second International Conference on Cyber-Technologies and Cyber-Systems (CYBER 2017) Falk , J.-C.B. Rainer , Chan , Steve 2 2017
- Radio Technical Commission for Aeronautics RTCA DO178C. Software Considerations in Airborne Systems and Equipment Certification 2011
- IEC 61508 Functional Safety of Electrical/Electronic/ Programmable Electronic Safety-Related Systems 2010
- ISO 26262 Road Vehicles - Functional Safety 2011
- CENELEC EN 50128 Railway Applications - Communication, Signaling and Processing Systems - Software for Railway Control and Protection Systems 2011
- Cousot , P. , and Cousot , R. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints Proc. of POPL’77 238 252 ACM Press 1977
- Kästner , D. Applying Abstract Interpretation to Demonstrate Functional Safety Boulanger , J.-L. Formal Methods Applied to Industrial Complex Systems London ISTE/Wiley 2014
- Kästner , D. , Rustemeier , C. , Kiffmeier , U. , Fleischer , D. , et al. Model-Driven Code Generation and Analysis SAE World Congress 2014 SAE International 2014
- Souyris , J. , Le Pavec , E. , Himbert , G. , Jégu , V. , Borios , G. , and Heckmann , R. Computing the Worst Case Execution Time of an Avionics Program by Abstract Interpretation Proceedings of the 5th Intl Workshop on Worst-Case Execution Time (WCET) Analysis 2005 21 24
- Delmas , D. , and Souyris , J. ASTRÉE: From Research to Industry Proc. 14th International Static Analysis Symposium (SAS2007), no. 4634 in LNCS 2007 437 451
- Kästner , D. , Miné , A. , Mauborgne , L. , Rival , X. , Feret , J. , Cousot , P. , Schmidt , A. , Hille , H. , Wilhelm , S. , and Ferdinand , C. Finding All Potential Runtime Errors and Data Races in Automotive Software SAE World Congress 2017, SAE International 2017
- ISO/FDIS 26262 Road Vehicles - Functional Safety 2018
- MISRA (Motor Industry Software Reliability Association) Working Group MISRA-C:2012 Guidelines for the Use of the C Language in Critical Systems MISRA Limited 2013
- Software Engineering Institute SEI - CERT Division SEI CERT C Coding Standard - Rules for Developing Safe, Reliable, and Secure Systems Carnegie Mellon University 2016
- The MITRE Corporation CWE - Common Weakness Enumeration
- Cousot , P. Semantic Foundations of Program Analysis, Ch. 10 Muchnick , S. and Jones , N. Program Flow Analysis: Theory and Applications Prentice-Hall 1981 303 342
- Cousot , P. , and Cousot , R. Comparing the Galois Connection and Widening/Narrowing Approaches to Abstract Interpretation, Invited Paper Bruynooghe , M. , Wirsing , M. Proc. 4th Int. Symp. PLILP’92, LNCS 631 Leuven, Springer 1992 269 295
- Cousot , P. and Cousot , R. Temporal Abstract Interpretation 27th POPL Boston ACM Press Jan. 2000 12 25
- Miné , A. , Mauborgne , L. , Rival , X. , Feret , J. , Cousot , P. , Kästner , D. , Wilhelm , S. , and Ferdinand , C. Taking Static Analysis to the Next Level: Proving the Absence of RunTime Errors and Data Races with Astrée Embedded Real Time Software and Systems Congress ERTS2 2016
- AbsInt The Static Analyzer - User Documentation for AAL Annotations 2015
- Kästner , D. , and Pohland , J. Program Analysis on Evolving Software Roy , M. CARS 2015 - Critical Automotive Applications: Robustness & Safety Paris, France 2015
- Miné , A. The Octagon Abstract Domain Higher-Order and Symbolic Computation 19 1 2006 31 100
- Feret , J. Static Analysis of Digital Filters Proc. of ESOP’04, vol. 2986 of LNCS Springer, 2004 33 48
- Miné , A. Static Analysis of Run-Time Errors in Embedded Real-Time Parallel C Programs Logical Methods in Computer Science (LMCS) 8 Mar. 2012 63
- OSEK/VDX OSEK/VDX Operating System 2005
- OSEK/VDX Operating System, Version 2.2.3 2005
- AUTOSAR (AUTomotive Open System ARchitecture) http://www.autosar.org
- Miné , A. , and Delmas , D. Towards an Industrial Use of Sound Static Analysis for the Verification of Concurrent Embedded Avionics Software Proc. of the 15th International Conference on Embedded Software (EMSOFT’15) IEEE CS Press Oct. 2015 65 74
- Burkacky , O. , Deichmann , J. , Doll , G. , and Knochenhauer , C. Rethinking Car Software and Electronics Architecture McKinsey Center for Future Mobility 2018