Static Analysis of Embedded Asynchronous Real-Time Software – AstréeA

The focus of the AstréeA project is on the development of static analysis by abstract interpretation to check the safety of large scale asynchronous embedded software.

The safety of critical embedded software, such as found in aeronautical, railway, automotive or medical industries, is of paramount importance as any error may have catastrophic economical or human consequences.

The cost of testing, the main validation method in use, is unfortunately becoming prohibitive when faced with the continually increasing complexity in embedded systems. Thus, tests only cover a small fraction of all possible executions, and can fail to discover some errors during validation. The situation is critical in the case of asynchronous software, i.e., software composed of several processes executed in parallel, as tests can only cover a tiny part of the huge number of process interleavings, while some errors may appear only for some specific, hard to reproduce interleaving.

Formal methods, however, enable validation with mathematical guarantees. Static analysis by abstract interpretation seems ideally suited to an industrial context as it is automatic (without user intervention), works directly on the source code (and not a simplified model), is sound (full coverage of the formal semantics of the language, hence without false negative) and efficient. However, it can suffer from false alarms (false positives), which is the case of most commercial static analyzers.

Our experience with Astrée (http://www.astree.ens.fr/) has shown that it is possible to build a static analyser with zero false alarm (giving thus a proof of safety) if it is specialized for a class of properties and programs: in the case of Astrée, run-time errors in synchronous embedded control/command avionic software. Astrée is now a commercial product used in an industrial context.

In the AstréeA project, we focus on the, much harder, issue of run-time errors in asynchronous software, by developing the AstréeA prototype analyzer, based on Astrée. Following the development method used successfully for Astrée, AstréeA is also specialized, in this case for run-time errors in large scale asynchronous avionic software running under a real-time operating system. Airbus France provides a large typical example of such software (1.6 M lines).

During the first phase of AstréeA, funded by ANR, we developed a concrete and abstract models of the ARINC 653 operating system and its scheduler, and a first analyzer prototype. After 4 years, it was able to analyze the full software, albeit with many alarms.

The gist of the AstréeA proposition is the continuation of this effort, following the recipe that made the success of Astrée: an incremental refinement of the analyzer until reaching the zero false alarm goal. For AstréeA, the refinement concerns: (1) the abstraction of process interactions (relational and history-sensitive abstractions), (2) the scheduler model (supporting more synchronisation primitives and taking priorities into account), (3) the memory model (supporting volatile variables), and (4) the abstraction of dynamical data-structures (linked lists). These improvements should enable AstréeA to achieve a high level of precision, and even the zero false alarm goal, thus making its industrial use possible.