Supervision : Emmanuel CHAILLOUX

Applicative Languages and Abstract Machines for Structural Code Coverage

This thesis presents a study on structural code coverage for a language of the ML family, in response to an industrial need in safety-critical software domain to develop tools. In this context, ML appears as a particularly rich and high-level language with a high degree of expressiveness. Its use is a progress but also raises issues when trying to use classical safety-critical software engineering processes. Notably, the two notions of conditions and decisions as well as coverage criteria associated with them rapidly become very complex. So the first contribution of this thesis is to give several formal semantics to the question of what conditions and decisions are when using a language of the ML family, which is formally specified. Then, we present a formalised technique for structural code coverage which rewrite the source code to produce traces at run-time. We name it the intrusive instrumentation. We also formalise another technique which does not rewrite the source code, which allows to use the same binary for both testing activities and distribution. This second technique is called non intrusive and consists in generating at compile-time the information needed to match the machine code back to the source code, but also other information for the execution environment to record the traces that we need to generate a coverage report. Finally, we compare these two techniques both formally and practically, but also in terms of implementation.

2007-2015 Publications