Ensuring the safety of critical embedded software is important as a single “bug” can have catastrophic consequences. Previous work has demonstrated that static analysis by Abstract Interpretation could help, when specializing an analyzer to a class of programs (synchronous control/command avionics C software) and properties (run-time errors).
In this paper, we describe ongoing work to achieve similar results for parallel embedded programs. We wish to match the current trend in critical embedded systems to switch from large numbers of single-program processors communicating through a common bus to single-processor multi-threaded applications communicating through a shared memory (for instance, in the context of Integrated Modular Avionics).
We focus on detecting run-time errors (arithmetic and memory errors) and take data-races into account (as they may cause such errors), but we ignore other concurrency errors (such as dead-locks, live-locks, or priority inversions), which are orthogonal.
Our method is based on Abstract Interpretation, a general theory of the approximation of semantics, which allows designing static analyzers that are sound by construction, i.e., consider a superset of all program behaviors and thus cannot miss any bug, but can cause spurious alarms due to over-approximations.
At its core, our method performs an analysis of each thread considering an abstraction of the effects of the other threads (called interferences). Each analysis generates a new set of interferences, and threads are re-analyzed until a xpoint is reached.
Thus, few modifications are required for a non-parallel analyzer to analyze parallel programs. Moreover, we show that few thread re-analyses are required in practice, resulting in a scalable analysis.
As we target embedded software, we can safely assume that there is no recursion nor dynamic allocation of memory, threads, or locks, which makes the analysis easier.
To read this external content in full, download the paper from the author archives at INRIA.