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

Paper #:
  • 2017-01-0054

Published:
  • 2017-03-28
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. In the past stablished semantics-based static analysis tools could not handle concurrent programs with the same level of soundness, coverage, and automation as sequential programs. Typically they didn't cover all potential process interleavings, required extensive user interaction, had limited support for concurrency primitives and failed to detect all potential concurrency-specific hazards such as data races. We present an extension of the static analyzer Astrée to soundly and automatically analyze concurrent software. Our extension covers all possible thread interleavings, and reports all run-time errors, data races and lock/unlock problems. When the analyzer does not report any alarm, the program is proven free from those classes of errors. The extension applies to OSEK/AUTOSAR, but can be also be used for the analysis of POSIX threads or ARINC 653. For OSEK systems Astrée reads the OIL configuration, and automatically creates an analysis wrapper capturing the OS configuration and the execution model, including the set of tasks with their priorities, the interrupt service routines, alarms, etc. The concurrency-related OSEK operating system primitives like GetResource, ActivateTask, etc. are automatically taken into account. In this talk 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. We will briefly summarize the investigated OSEK and AUTOSAR applications, and discuss the analysis results.
Access
Now
SAE MOBILUS Subscriber? You may already have access.
Buy
Attention: This item is not yet published. Pre-Order to be notified, via email, when it becomes available.
Select
Price
List
Download
$22.00
Mail
$22.00
Members save up to 36% off list price.
Share
HTML for Linking to Page
Page URL

Related Items

Technical Paper / Journal Article
2004-11-16
Article
2016-03-04
Article
2016-03-04
Training / Education
2016-04-30
Training / Education
2017-01-20
Standard
2001-04-26
Technical Paper / Journal Article
2004-11-16
Training / Education
2015-07-13