Use of static analysis in the V&V process for critical embedded software

This paper describes the new roles and goals assigned to Static Analysis in the CNES Verification & Validation process of embedded software. One of the main advantages of the static analysis approach is that it is easy to use: only the source code availability is required, not the full development environment. Moreover, static analysis techniques (and associated tools) in dedicated to embedded critical software are being developed and tested on the field, and the first experiments results seem very promising. The tools which implement these techniques deal with two major points that software teams cannot address thoroughly today: - exhaustive identification of run time errors, - verification of functional and safety properties. However, the use of these techniques also raises questions that must be addressed, such as. - Is it possible to measure its effectiveness - What is the ratio between the effort spent in results exploitation and the software safety requirements - What is the impact on the V&V process ? Based on several experiments carried out by the CNES on Spacecraft on board software, this paper introduces the main results obtained with a static analysis tool called PolySpace Verifier, and some typical defects that have been found at the occasion in the analysed software. As a conclusion, we will give some elements on the efficiency of this technique, the constraints for its implementation and some perspectives on the V&V process evolution.