This content is not included in
your SAE MOBILUS subscription, or you are not logged in.
Analyze This! Sound Static Analysis for Integration Verification of Large-Scale Automotive Software
Technical Paper
2019-01-1246
ISSN: 0148-7191, e-ISSN: 2688-3627
This content contains downloadable datasets
Annotation ability available
Sector:
Language:
English
Abstract
Safety-critical embedded software has to satisfy stringent quality requirements. One such requirement, imposed by all contemporary safety standards, is that no critical run-time errors must occur. Runtime errors can be caused by undefined or unspecified behavior of the programming language; examples are buffer overflows or data races. They may cause erroneous or erratic behavior, induce system failures, and constitute security vulnerabilities. A sound static analyzer reports all such defects in the code, or proves their absence. Sound static program analysis is a verification technique recommended by ISO/FDIS 26262 for software unit verification and for the verification of software integration. In this article we propose an analysis methodology that has been implemented with the static analyzer Astrée. It supports quick turn-around times and gives highly precise whole-program results. We give an overview of the key concepts of Astrée that enable it to efficiently handle large-scale code, and describe a pre-analysis which transforms the source code to make it better amenable to static analysis. The experimental results confirm that sound static analysis can be successfully applied for integration verification of large-scale automotive software.
Recommended Content
Authors
Topic
Citation
Kaestner, D., Schmidt, B., Schlund, M., Mauborgne, L. et al., "Analyze This! Sound Static Analysis for Integration Verification of Large-Scale Automotive Software," SAE Technical Paper 2019-01-1246, 2019, https://doi.org/10.4271/2019-01-1246.Data Sets - Support Documents
| Title | Description | Download |
|---|---|---|
| Unnamed Dataset 1 |
Also In
References
- Kästner , D. , Mauborgne , L. , and Ferdinand , C. 2017
- 2011
- IEC 61508 2010
- ISO 26262 2011
- CENELEC EN 50128 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 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) 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 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
- Cousot , P. Semantic Foundations of Program Analysis, Ch. 10 Muchnick S. , 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 26-28 Aug. 1992 1992 269 295
- Cousot , P. and Cousot , R. Temporal Abstract Interpretation 27th POPL Boston ACM Press 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 Run-Time Errors and Data Races with Astrée Embedded Real Time Software and Systems Congress ERTS 2 2016
- AbsInt 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 31 100 2006
- 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 63 2012
- OSEK/VDX 2005
- OSEK/VDX Operating System 2005
- AUTOSAR 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. 2018