Sound Static Analysis for Integration Verification of Large-Scale Automotive Software 2019-01-1246
Safety-critical embedded software has to satisfy stringent quality requirements. Safety standards require evidence that no critical run-time errors occur. One important class of runtime errors is caused by undefined or unspecified behavior of the programming language, including 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. ISO/FDIS 26262 (2018) recommends sound static analysis for software unit verification and for the verification of software integration.
In the past there were concerns about the complexity of sound static program analysis. In this article we demonstrate that large-scale automotive control software of more than 10 million lines of code can be efficiently analyzed with low false alarm rates.
Splitting the application into components reduces analysis time. However, cross-component dependencies may lead to undiscovered defects on the one hand, and to false alarms on the other hand. Hence, it is preferable to do a whole-program analysis. Key requirements for such an integration analysis are a flexibly configurable analysis engine that achieves high analysis precision, minimizes unreached code, and scales to code sizes of millions of lines of code.
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. We briefly summarize the characteristics of the target application and report on practical experiments. The experimental results confirm that sound static analysis can be successfully applied for integration verification of large-scale automotive software.
Daniel Kaestner, Bernard Schmidt, Maximilian Schlund, Laurent Mauborgne, Stephan Wilhelm, Christian Ferdinand
Absint Angewandte Informatik Gmbh, Robert Bosch GmbH