Zoom
Static verification of the good properties of a program did not look like a line of research that would be rich in applications. The assessment of the Ariane 501 flight failure using the tool developed by Alain Deutsch (project Para) has invalidated this statement.
The static analyzer automatically computes the properties of the program to be verified by abstract interpretation. Formally, all the properties of the program are solutions of a system of equations, the resolution of which requires an infinite amount of time. This system is replaced by an approximate system which only gives part of the properties of the program. Such methods were applied to two on-board software packages of the Ariane 5 launcher, the flight program and the inertial guidance system, in collaboration with Aérospatiale.
After this analyzer was successfully used for flight 502, it became necessary to bring it up to industrial standards. This entailed rewriting part of the code using public software. It also required validation by the DO-198B standard of aeronautics and aerospace users. The prototype was tested on diverse space projects. Daniel Pilaud and Alain Deutsch then founded the Polyspace Technologies company with active support from INRIA-Transfert. The company specializes in the development and marketing of software testing and validation environments. Such environments will be designed to improve the productivity of companies during the verification stages. The market targeted is that of on-board systems for which the control of validation costs is becoming a major issues, due to the ever growing complexity of embedded software.
