thesis

Langages applicatifs et machines abstraites pour la couverture de code structurelle

Defense date:

Jan. 1, 2012

Edit

Institution:

Paris 6

Disciplines:

Authors:

Abstract EN:

Cette thèse présente une étude qui répond à un besoinindustriel d'avoir des outils pour aider à la qualité et au respectdes processus de développement de logiciels critiques comme ceux dudomaine de l'avionique civile. Il s'agit de l'étude de la couverturede code structurelle pour un langage de la famille ML. Dans cecontexte, ML apparaît comme un langage particulièrement riche enconstructions de haut-niveau d'abstraction et expressif. Sonutilisation est un élément de progrès mais soulève des problèmesd'adaptation des pratiques du génie logiciel classique pour lessystèmes critiques. Notamment, la notion de couverture des conditionset des décisions ainsi que les critères de couverture dérivés secomplexifient rapidement. Nous donnons alors en première contributionplusieurs sémantiques pour l'interprétation des définitions desconditions et des décisions pour un langage d'expressions dehaut-niveau que nous avons complètement formellement défini. Ensuite,nous donnons la sémantique formelle pour une implantation pour lamesure de couverture par réécriture du code source, ce que nousappelons l'instrumentation intrusive. Puis, nous étudions unetechnique qui ne réécrit pas le code, ce qui permet d'avoir lapossibilité d'utiliser le même binaire pour les tests et pour laproduction. Cette technique, que nous appelons non intrusive,consiste à générer les informations de correspondance entre le codesource et le code machine, et éventuellement d'autres informations,pour que l'environnement d'exécution incluant une machine virtuellepuisse enregistrer les traces nécessaires à l'élaboration des rapportsde couverture. Enfin, nous comparons ces deux approches, en terme desémantique, d'utilisation et d'implantation

Abstract FR:

This thesis presents a study on structural code coverage fora language of the ML family, in response to an industrial need insafety-critical software domain to develop tools. In this context, MLappears as a particularly rich and high-level language with a highdegree of expressiveness. Its use is a progress but also raises issueswhen trying to apply classical safety-critical software engineeringprocesses. In particular, the two notions of condition and decision,as well as coverage criteria associated with them, rapidly become verycomplex. The first contribution of this thesis answers the question ofwhat conditions and decisions mean for a language of the ML family, bygiving several formal definitions. Then, we present a formalisedtechnique for structural code coverage which rewrites the source codeto produce traces at run-time. We name it the intrusiveinstrumentation. We also formalise another technique which does notrewrite the source code, which allows to use the same binary for bothtesting activities and production. This second technique is called nonintrusive and consists in generating at compile-time the informationneeded to match the machine code back to the source code. Otherinformation are also generated for the execution environment to recordspecific traces that we need to generate a coverage report involvingBoolean measures. Finally, we compare these two techniques bothformally and practically, but also in terms of implementation.