Finding All Potential Run-Time Errors and Data Races in Automotive Software
| Autor: | Daniel Kaestner, Heinz Hille, Xavier Rival, Patrick Cousot, Antoine Miné, Jérôme Feret, Laurent Mauborgne, Christian Ferdinand, Stephan Wilhelm, André Schmidt |
|---|---|
| Přispěvatelé: | AbsInt GmbH (Angewandte Informatik), AbsInt, Algorithmes, Programmes et Résolution (APR), Laboratoire d'Informatique de Paris 6 (LIP6), Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS), Daimler Chrysler AG (Daimler), Analyse Statique par Interprétation Abstraite (ANTIQUE), Département d'informatique - ENS Paris (DI-ENS), Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Paris (ENS Paris), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Paris (ENS Paris), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria), New York University [New York] (NYU), NYU System (NYU), École normale supérieure - Paris (ENS-PSL), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Paris (ENS-PSL), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Inria de Paris, Département d'informatique de l'École normale supérieure (DI-ENS), École normale supérieure - Paris (ENS Paris), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Paris (ENS Paris) |
| Jazyk: | angličtina |
| Rok vydání: | 2017 |
| Předmět: |
[INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL]
Computer science business.industry 020209 energy OSEK Concurrency 02 engineering and technology computer.software_genre ARINC 653 020303 mechanical engineering & transports Embedded software AUTOSAR Software 0203 mechanical engineering Embedded system Pointer (computer programming) 0202 electrical engineering electronic engineering information engineering Operating system business computer Automotive software |
| Zdroj: | SAE Technical Paper WCX™ 2017-SAE World Congress Experience WCX™ 2017-SAE World Congress Experience, Apr 2017, Detroit United States. pp.1-9, ⟨10.4271/2017-01-0054⟩ |
| DOI: | 10.4271/2017-01-0054⟩ |
| Popis: | International audience; 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|