WP5: Trusting Formal Methods

Static analysis techniques give strong theoretical assurance that some properties hold on critical embedded software. Implementing these techniques is very difficult and error-prone. This work package aims at increasing the level of trust in concrete static analyzers. More generally, it will investigate how the use of formal methods for developing the tools may impact validation and verification activities.

On a methodological point of view, a first task will focus on the qualifiability of tools in the sense of safety norms like DO-178B and the forthcoming DO-178C.

The other items in this work package will examine the formalization of the most important building blocks of the Frama-C framework into a proof assistant such as Coq. Properties to be proved on these formal models will be given as a result of the first item.

A first area of interest is to establish an explicit formal link between the model built by the analyzers (from the source code) and the model used by the compilation tool chain during the translation from source to object code. Second, a certified relational lattice similar to the ones used in task 3.4 will be implemented. Last, we will investigate the feasibility of building a formal model of Scade programs so as to be able to validate the C code generated from Scade (i.e. to prove that the semantics of the program is preserved through code generation).

As a summary, this work package depends on the models developed in WP3 (Combining Static Analysis Techniques) and, for the Scade models, on the ability to reason about temporal properties, as investigated in WP2 (Temporal Properties). On the other hand, these elements of formalization will foster the usage of the Frama-C platform, the main objective of WP6 (Spreading Static Analysis Techniques) in particular in contexts where a very high level of confidence is required.