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.


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Analyze This! Sound Static Analysis for Integration Verification of Large-Scale Automotive Software


    Additional title:

    Sae Technical Papers



    Conference:

    WCX SAE World Congress Experience ; 2019



    Publication date :

    2019-04-02




    Type of media :

    Conference paper


    Type of material :

    Print


    Language :

    English




    Analyze This! Sound Static Analysis for Integration Verification of Large-Scale Automotive Software

    Kaestner, Daniel / Schmidt, Bernard / Schlund, Maximilian et al. | British Library Conference Proceedings | 2019


    Automatic Sound Static Analysis for Integration Verification of AUTOSAR Software

    Ferdinand, Christian / Mallon, Christoph / Kaestner, Daniel et al. | SAE Technical Papers | 2023


    Static Code Analysis for Automotive Software

    Kengo Oka, Dennis | Wiley | 2021


    Reducing defects in automotive software using static analysis

    Ranadive,P.R. / Vaidya,V. / Rajguru,C. et al. | Automotive engineering | 2015


    Reducing Defects in Automotive Software Using Static Analysis

    Rajguru, Chaitanya / Ranadive, Priti R. / Vaidya, Vinay | SAE Technical Papers | 2015