Finding All Potential Run-Time Errors and Data Races in Automotive Software

Daniel Kaestner, Antoine Miné, André Schmidt, Heinz Hille, Laurent Mauborgne, Stephan Wilhelm, Xavier Rival, Jérôme Feret, Patrick Cousot, Christian Ferdinand

Research output: Contribution to journalArticle

Abstract

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.

Original languageEnglish (US)
JournalSAE Technical Papers
Volume2017-March
Issue numberMarch
DOIs
StatePublished - Mar 28 2017

Fingerprint

Embedded software
Experiments

ASJC Scopus subject areas

  • Automotive Engineering
  • Safety, Risk, Reliability and Quality
  • Pollution
  • Industrial and Manufacturing Engineering

Cite this

Kaestner, D., Miné, A., Schmidt, A., Hille, H., Mauborgne, L., Wilhelm, S., ... Ferdinand, C. (2017). Finding All Potential Run-Time Errors and Data Races in Automotive Software. SAE Technical Papers, 2017-March(March). https://doi.org/10.4271/2017-01-0054

Finding All Potential Run-Time Errors and Data Races in Automotive Software. / Kaestner, Daniel; Miné, Antoine; Schmidt, André; Hille, Heinz; Mauborgne, Laurent; Wilhelm, Stephan; Rival, Xavier; Feret, Jérôme; Cousot, Patrick; Ferdinand, Christian.

In: SAE Technical Papers, Vol. 2017-March, No. March, 28.03.2017.

Research output: Contribution to journalArticle

Kaestner, D, Miné, A, Schmidt, A, Hille, H, Mauborgne, L, Wilhelm, S, Rival, X, Feret, J, Cousot, P & Ferdinand, C 2017, 'Finding All Potential Run-Time Errors and Data Races in Automotive Software', SAE Technical Papers, vol. 2017-March, no. March. https://doi.org/10.4271/2017-01-0054
Kaestner D, Miné A, Schmidt A, Hille H, Mauborgne L, Wilhelm S et al. Finding All Potential Run-Time Errors and Data Races in Automotive Software. SAE Technical Papers. 2017 Mar 28;2017-March(March). https://doi.org/10.4271/2017-01-0054
Kaestner, Daniel ; Miné, Antoine ; Schmidt, André ; Hille, Heinz ; Mauborgne, Laurent ; Wilhelm, Stephan ; Rival, Xavier ; Feret, Jérôme ; Cousot, Patrick ; Ferdinand, Christian. / Finding All Potential Run-Time Errors and Data Races in Automotive Software. In: SAE Technical Papers. 2017 ; Vol. 2017-March, No. March.
@article{375486ee5bf340f8bcda76c880db1400,
title = "Finding All Potential Run-Time Errors and Data Races in Automotive Software",
abstract = "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}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.",
author = "Daniel Kaestner and Antoine Min{\'e} and Andr{\'e} Schmidt and Heinz Hille and Laurent Mauborgne and Stephan Wilhelm and Xavier Rival and J{\'e}r{\^o}me Feret and Patrick Cousot and Christian Ferdinand",
year = "2017",
month = "3",
day = "28",
doi = "10.4271/2017-01-0054",
language = "English (US)",
volume = "2017-March",
journal = "SAE Technical Papers",
issn = "0148-7191",
publisher = "SAE International",
number = "March",

}

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

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 - Article

AN - SCOPUS:85018383096

VL - 2017-March

JO - SAE Technical Papers

JF - SAE Technical Papers

SN - 0148-7191

IS - March

ER -