Direction de recherche : Emmanuel CHAILLOUX

Langages Applicatifs et Machines Abstraites pour la Couverture de Code Structurelle

Cette thèse présente une étude qui répond à un besoin industriel d’avoir des outils pour aider à la qualité et au respect des processus de développement de logiciels critiques comme ceux du domaine de l’avionique civile. Il s’agit de l’étude de la couverture de code structurelle pour un langage de la famille ML. Dans ce contexte, ML apparaît comme un langage particulièrement riche en constructions de haut-niveau d’abstraction et expressif. Son utilisation est un élément de progrès mais soulève des problèmes d’adaptation des pratiques du génie logiciel classique pour les systèmes critiques. Notamment, la notion de couverture des conditions et des décisions ainsi que les critères de couverture dérivés se complexifient rapidement. Nous donnons alors en première contribution plusieurs sémantiques pour l’interprétation des définitions des conditions et des décisions pour un langage d’expressions de haut-niveau que nous avons complètement formellement défini. Ensuite, nous donnons la sémantique formelle pour une implantation pour la mesure de couverture par réécriture du code source, ce que nous appelons l’instrumentation intrusive. Puis, nous étudions une technique qui ne réécrit pas le code, ce qui permet d’avoir la possibilité d’utiliser le même binaire pour les tests et pour la production. Cette technique, que nous appelons non intrusive, consiste à générer les informations de correspondance entre le code source et le code machine, et éventuellement d’autres informations, pour que l’environnement d’exécution incluant une machine virtuelle puisse enregistrer les traces nécessaires à l’élaboration des rapports de couverture. Enfin, nous comparons ces deux approches, en terme de sémantique, d’utilisation et d’implantation.

Publications 2007-2015

• 2015
  • B. Vaugon, Ph. Wang, E. Chailloux : “Programming Microcontrollers in Ocaml: the OCaPIC Project”, International Symposium on Practical Aspects of Declarative Languages (PADL 2015), vol. 9131, Lecture Notes in Computer Science, Portland, OR, United States, pp. 132-148, (Springer Verlag) (2015)
• 2014
  • P. Manoury, Ph. Baufreton, J.‑L. Dufour, E. Prun, E. Chailloux, G. Henry, F. Thibord, Ph. Wang, E. Millon : “Certification de l’assemblage de composants dans le développement de logiciels critiques”, Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL'14), Paris, France, pp. 109-114 (2014)
  • Ph. Baufreton, E. Chailloux, J.‑L. Dufour, G. Henry, P. Manoury, E. Prun, F. Thibord, Ph. Wang : “Compositional certification: the CERCLES2 project”, Embedded Real Time Software and Systems (ERTS2), Toulouse, France, pp. 582-591 (2014)
• 2012
  • Ph. Wang : “Langages Applicatifs et Machines Abstraites pour la Couverture de Code Structurelle”, soutenance de thèse, soutenance 04/10/2012, direction de recherche Chailloux, Emmanuel (2012)
• 2011
  • Ph. Wang, A. Jonquet, E. Chailloux : “Non-Intrusive Structural Coverage for Objective Caml”, 5^th Workshop on Bytecode Semantics, Verification, Analysis and Transformation, vol. 264 (4), Electronic Notes in Theoretical Computer Science, Paphos, Cyprus, pp. 59-73, (Elsevier) (2011)
  • B. Vaugon, Ph. Wang, E. Chailloux : “Les microcontrôleurs PIC programmés en Objective Caml”, Actes des vingt-deuxièmes Journées Francophones des Langages Applicatifs, Studia Informatica Universalis, La Bresse, France, pp. 177-207, (Hermann) (2011)
• 2009
  • M. Bourgoin, B. Canou, E. Chailloux, A. Jonquet, Ph. Wang : “OC4MC: Objective Caml for Multicore Architectures”, 21^st Symposium on Implementation and Application of Functional Languages, vol. SHU-TR-CS-2009-09-1, South Orange, United States, pp. 24-41 (2009)
  • B. Pagano, O. Andrieu, Th. Moniot, B. Canou, E. Chailloux, Ph. Wang, P. Manoury, J.‑L. Colaço : “Experience Report: Using Objective Caml to develop safety-critical embedded tool in a certification framework”, The 14^th ACM SIGPLAN International Conference on Functional Programming (ICFP 2009), Edinburgh, United Kingdom, pp. 215-220, (ACM) (2009)
• 2007
  • B. Pagano, B. Canou, E. Chailloux, J.‑L. Colaço, Ph. Wang : “Couverture de code Caml pour la réalisation d’outils de développement certifiés”, Journées Francophones des Langages Applicatifs (JFLA 2007), Aix-les-Bains, France, pp. 71-86 (2007)