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