Proving Properties of Reactive Programs From C to Lustre

In critical embedded software, proving functional properties of programs is a major area where formal methods are applied with an increasing success. Anyway, the more a property is complex, the more a high-level formal model of the software and its environment is required. However, in an industrial setting, such a model is not always available, or cannot be used for independent verification. We propose here a new route, where a high-level Lustre model is extracted from a C source program. Thus, high-level functional properties can be specified in Lustre and proved on this extracted model, hence on the real code, without requiring any additional formal documentation.