TY - JOUR
T1 - Finding All Potential Run-Time Errors and Data Races in Automotive Software
AU - Kaestner, Daniel
AU - Miné, Antoine
AU - Schmidt, André
AU - Hille, Heinz
AU - Mauborgne, Laurent
AU - Wilhelm, Stephan
AU - Rival, Xavier
AU - Feret, Jérôme
AU - Cousot, Patrick
AU - Ferdinand, Christian
N1 - Publisher Copyright:
Copyright © 2017 SAE International.
PY - 2017/3/28
Y1 - 2017/3/28
N2 - Safety-critical embedded software has to satisfy stringent quality requirements. All contemporary safety standards require evidence that no data races and no critical run-time errors occur, such as invalid pointer accesses, buffer overflows, or arithmetic overflows. Such errors can cause software crashes, invalidate separation mechanisms in mixed-criticality software, and are a frequent cause of errors in concurrent and multi-core applications. The static analyzer Astrée has been extended to soundly and automatically analyze concurrent software. This novel extension employs a scalable abstraction which covers all possible thread interleavings, and reports all potential run-time errors, data races, deadlocks, and lock/unlock problems. When the analyzer does not report any alarm, the program is proven free from those classes of errors. Dedicated support for ARINC 653 and OSEK/AUTOSAR enables a fully automatic OS-aware analysis. In this article we give an overview of the key concepts of the concurrency analysis and report on experimental results obtained on concurrent automotive software. The experiments confirm that the novel analysis can be successfully applied to real automotive software projects.
AB - Safety-critical embedded software has to satisfy stringent quality requirements. All contemporary safety standards require evidence that no data races and no critical run-time errors occur, such as invalid pointer accesses, buffer overflows, or arithmetic overflows. Such errors can cause software crashes, invalidate separation mechanisms in mixed-criticality software, and are a frequent cause of errors in concurrent and multi-core applications. The static analyzer Astrée has been extended to soundly and automatically analyze concurrent software. This novel extension employs a scalable abstraction which covers all possible thread interleavings, and reports all potential run-time errors, data races, deadlocks, and lock/unlock problems. When the analyzer does not report any alarm, the program is proven free from those classes of errors. Dedicated support for ARINC 653 and OSEK/AUTOSAR enables a fully automatic OS-aware analysis. In this article we give an overview of the key concepts of the concurrency analysis and report on experimental results obtained on concurrent automotive software. The experiments confirm that the novel analysis can be successfully applied to real automotive software projects.
UR - http://www.scopus.com/inward/record.url?scp=85018383096&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85018383096&partnerID=8YFLogxK
U2 - 10.4271/2017-01-0054
DO - 10.4271/2017-01-0054
M3 - Conference article
AN - SCOPUS:85018383096
SN - 0148-7191
VL - 2017-March
JO - SAE Technical Papers
JF - SAE Technical Papers
IS - March
T2 - SAE World Congress Experience, WCX 2017
Y2 - 4 April 2017 through 6 April 2017
ER -