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

• 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”, thesis, phd defence 10/04/2012, supervision 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)