This content is not included in
your SAE MOBILUS subscription, or you are not logged in.
Automatic Sound Static Analysis for Integration Verification of AUTOSAR Software
Technical Paper
2023-01-0591
ISSN: 0148-7191, e-ISSN: 2688-3627
Annotation ability available
Sector:
Language:
English
Abstract
Preventing systematic software failures is of paramount importance for any highly automatic vehicle control system, in particular for safety-critical AUTOSAR software. Among the most critical software defects are runtime errors like buffer overflows or data races. They may cause erroneous or erratic behavior, induce system failures, and constitute security vulnerabilities. Sound static analysis can be used to report all such defects in the code, or to prove their absence. It can also determine dependencies between software components and show freedom of interference without missing any data and control flow through data or function pointers. In the past, AUTOSAR projects often had to be decomposed or simplified to achieve satisfactory analysis time or memory consumption. Creating the analysis model, i.e., determining the tasks and ISRs to analyze, their priorities, synchronization, etc., required significant manual effort. In this article we present novel analysis concepts, developed in the Astrée analyzer, to support fully automatic integration analysis of AUTOSAR projects. The execution model is automatically derived from the ARXML specification. No changes to the software under analysis are required. All specified tasks and ISRs are analyzed assuming fully concurrent execution; runtime errors, data races and deadlocks are reported. Task priorities, core assignment, resources, spinlocks, and critical sections enclosed by primitives to disable/enable interrupts are automatically handled. To minimize false alarms, Astrée supports tuning the analyzer to the software under analysis by locally boosting analysis precision. We report on practical experience with real-life industry projects, giving an overview of alarm rates, analysis time and memory consumption, as well as reduction of false alarms by fine-tuning the analysis precision to the software under analysis.
Authors
- Daniel Kaestner - Absint Angewandte Informatik GmbH
- Stephan Wilhelm - Absint Angewandte Informatik GmbH
- Christoph Mallon - Absint Angewandte Informatik GmbH
- Stefana Schank - Absint Angewandte Informatik GmbH
- Christian Ferdinand - Absint Angewandte Informatik GmbH
- Laurent Mauborgne - Absint Angewandte Informatik GmbH
Topic
Citation
Kaestner, D., Wilhelm, S., Mallon, C., Schank, S. et al., "Automatic Sound Static Analysis for Integration Verification of AUTOSAR Software," SAE Technical Paper 2023-01-0591, 2023, https://doi.org/10.4271/2023-01-0591.Also In
References
- ISO/SAE 21434 2021
- ISO 26262 2018
- Kästner , D. , Schmidt , B. , Schlund , M. , Mauborgne , L. et al. SAE Technical Paper 2019-01-1246 2019 https://doi.org/10.4271/2019-01-1246
- MISRA (Motor Industry Software Reliability Association) Working Group MISRA-C:2012 Guidelines for the Use of the C Language in Critical Systems MISRA Limited Mar. 2013
- M. Limited June 2008
- Software Engineering Institute SEI – CERT Division SEI CERT C Coding Standard – Rules for Developing Safe, Reliable, and Secure Systems Carnegie Mellon University 2016
- 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 ACM Press 1977 238 252
- Souyris , J. , Le Pavec , E. , Himbert , G. , Jégu , V. et al. 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
- Kästner , D. , Miné , A. , Mauborgne , L. , Rival , X. et al. Finding all Potential Runtime Errors and Data Races in Automotive Software SAE Technical Paper 2017-01-0054 2017 https://doi.org/10.4271/2017-01-0054
- Kästner , D. Applying Abstract Interpretation to Demonstrate Functional Safety Boulanger , J.-L. Formal Methods Applied to Industrial Complex Systems London, UK ISTE/Wiley 2014
- Kästner , D. , Mauborgne , L. , and Ferdinand , C. Detecting Safety- and Security-Relevant Programming Defects by Sound Static Analysis The Second International Conference on Cyber-Technologies and Cyber-Systems (CYBER 2017) IARIA Conferences 26 31 2017
- Kästner , D. , Leroy , X. , Blazy , S. , Schommer , B. et al. Closing the gap – the formally verified optimizing compiler CompCert SSS’17: Developments in System Safety Engineering: Proceedings of the Twenty-fifth Safety-critical Systems Symposium 163 180 2017
- Kästner , D. , Barrho , J. , Wünsche , U. , Schlickling , M. et al. ERTS2 2018 - Embedded Real Time Software and Systems Jan. 2018 https://hal.inria.fr/hal-01643290/file/ERTS_2018_paper_59.pdf
- Miné , A. Static Analysis of Run-Time Errors in Embedded Real-Time Parallel C Programs Logical Methods in Computer Science (LMCS) 8 Mar. 2012 63
- Kästner D. , Mauborgne L. , Wilhelm S. , Mallon C. , and Ferdinand C. Static Data and Control Coupling Analysis 11th Embedded Real Time Systems European Congress (ERTS2022) Toulouse, France June 2022
- Sreeram , U. Electronic Theses and Dissertations, University of Windsor 2019
- AUTOSAR https://www.autosar.org/fileadmin/ABOUT/AUTOSAR_Introduction.pdf Nov. 2019
- AUTOSAR Aug. 2018
- OSEK/VDX 2005
- AUTOSAR http://www.autosar.org
- 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) IEEE CS Press Oct. 2015 65 74
- AUTOSAR Apr. 2007
- dev.toppers.jp https://dev.toppers.jp/trac_user/contrib/browser/autosar_os_training/trunk/program/sample/sample1.arxml?rev=258 2022
- Rival , X. and Mauborgne , L. The Trace Partitioning Abstract Domain ACM Trans. Program. Lang. Syst. 29 5 2007 26
- Kästner , D. and Pohland , J. Program Analysis on Evolving Software Roy , M. CARS 2015 - Critical Automotive Applications: Robustness & Safety (Paris, France) Sept. 2015
- Cousot , P. Proving Program Invariance and Termination by Parametric Abstraction, Lagrangian Relaxation and Semidefinite Programming Verification, Model Checking, and Abstract Interpretation, 6th International Conference, VMCAI 2005, Paris, France, January 17-19, 2005, Proceedings Cousot R. 3385 Lecture Notes in Computer Science 1 24 Springer 2005
- Giet , J. , Mauborgne , L. , Kästner , D. , and Ferdinand , C. Towards Zero Alarms in Sound Static Analysis of Finite State Machines Romanovsky , A. , Troubitsyna , E. and Bitsch , F. Computer Safety, Reliability, and Security Cham Springer International Publishing 2019 3 18