This content is not included in
your SAE MOBILUS subscription, or you are not logged in.
Finding All Potential Run-Time Errors and Data Races in Automotive Software
Technical Paper
2017-01-0054
ISSN: 0148-7191, e-ISSN: 2688-3627
This content contains downloadable datasets
Annotation ability available
Sector:
Language:
English
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.
Recommended Content
Authors
- Daniel Kaestner - Absint Angewandte Informatik GmbH
- Antoine Miné - University Pierre and Marie Curie
- André Schmidt - Daimler AG
- Heinz Hille - Daimler AG
- Laurent Mauborgne - Absint Angewandte Informatik GmbH
- Stephan Wilhelm - Absint Angewandte Informatik GmbH
- Xavier Rival - INRIA/ENS
- Jérôme Feret - INRIA/ENS
- Patrick Cousot - New York University
- Christian Ferdinand - Absint Angewandte Informatik GmbH
Citation
Kaestner, D., Miné, A., Schmidt, A., Hille, H. et al., "Finding All Potential Run-Time Errors and Data Races in Automotive Software," SAE Technical Paper 2017-01-0054, 2017, https://doi.org/10.4271/2017-01-0054.Data Sets - Support Documents
Title | Description | Download |
---|---|---|
Unnamed Dataset 1 | ||
Unnamed Dataset 2 | ||
Unnamed Dataset 3 | ||
Unnamed Dataset 4 |
Also In
References
- AbsInt GmbH Safety Manual for aiT, Astrée, StackAnalyzer 2015
- Cousot P. and Cousot R. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints Proc. of POPL’77 238 252 ACM Press 1977
- Kästner D. Applying Abstract Interpretation to Demonstrate Functional Safety Boulanger J.-L. Formal Methods Applied to Industrial Complex Systems ISTE/Wiley London, UK 2014
- Souyris Jean , Pavec Erwan Le , Himbert Guillaume , Jégu Victor , Borios Guillaume , and Heckmann Reinhold Computing the worst case execution time of an avionics program by abstract interpretation Proceedings of the 5th Intl Workshop on Worst-Case Execution Time (WCET) Analysis 21 24 2005
- Delmas D. and Souyris J. ASTRÉE: from Research to Industry Proc. 14th International Static Analysis Symposium (SAS2007) 437 451 2007
- Kaestner , D. , Rustemeier , C. , Kiffmeier , U. , Fleischer , D. et al. Model-Driven Code Generation and Analysis SAE Technical Paper 2014-01-0217 2014 10.4271/2014-01-0217
- Miné A. , Mauborgne L. , Rival X. , Feret J. , Cousot P. , Kästner D. , Wilhelm S. , and Ferdinand C. Taking Static Analysis to the Next Level: Proving the Absence of Run-Time Errors and Data Races with Astrée Embedded Real Time Software and Systems Congress ERTS 2
- OSEK/VDX Operating System 2005
- AUTOSAR (AUTomotive Open System ARchitecture) http://-www.autosar.org
- MISRA-C:2004 Guidelines for the use of the C language in critical systems Oct. 2004
- MISRA-C:2012 Guidelines for the use of the C language in critical systems Mar. 2013
- ISO 26262 Road vehicles - Functional safety 2011
- GI/SafeTRANS/VDA Automotive Roadmap Embedded Systems - Eingebettete Systeme in der Automobilindustrie. Roadmap 2015 - 2030 September 2015
- Debouk R. , Czerny B. , and d’Ambrosio J. Safety Strategy for Autonomous Systems International Systems Safety Society Conference August 2011
- Blanchet B. , Cousot P. , Cousot R. , Feret J. , Mauborgne L. , Miné A. , Monniaux D. , and Rival X. A Static Analyzer for Large Safety-Critical Software Proc. of PLDI’03 196 207 ACM Press June 7-14 2003
- Mine A. , Mauborgne L. , Rival X. , Feret J. , Cousot P. , Kästner D. , Wilhelm S. , and Ferdinand C. Taking Static Analysis to the Next Level: Proving the Absence of Run-Time Errors and Data Races with Astrée Embedded Real Time Software and Systems Congress ERTS 2
- JTC1/SC22 Programming languages - C 16 Dec. 1999
- Miné A. The Octagon Abstract Domain Higher-Order and Symbolic Computation 19 1 31 100 2006
- Cousot Patrick , Cousot Radhia , Feret Jérôme , Miné Antoine , Mauborgne Laurent , Monniaux David , and Rival Xavier Varieties of Static Analyzers: A Comparison with ASTRÉE First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, TASE 2007 3 20 IEEE Computer Society 2007
- Feret Jérôme Static analysis of digital filters Proc. of ESOP’04 2986 LNCS 33 48 Springer 2004
- Mauborgne L. and Rival X. Trace Partitioning in Abstract Interpretation Based Static Analyzers 14th European Symposium on Programming ESOP’05 5 20 2005
- AbsInt The Static Analyzer - User Documentation for AAL Annotations 2015
- Kästner Daniel and Pohland Jan Program Analysis on Evolving Software Roy Matthieu CARS 2015 - Critical Automotive applications: Robustness & Safety Paris, France September 2015
- Miné A. Static analysis of run-time errors in embedded real-time parallel C programs Logical Methods in Computer Science (LMCS) 8 26 63 Mar. 2012
- IEEE Computer Society and The Open Group Portable operating system interface (POSIX) - Application program interface (API) amendment 2: Threads extension (C language) Technical report, ANSI/IEEE Std. 1003.1c-1995 1995
- Miné A. and Delmas D. Towards an Industrial Use of Sound Static Analysis for the Verification of Concurrent Embedded Avionics Software Proc. of the 15th International Conference on Embedded Software (EMSOFT’15) 65 74 IEEE CS Press Oct. 2015