Thèmes d'intérêt

  • Ingénierie du logiciel
  • Langages
  • Transformations
    • de langages
    • qualifiables
    • de modèles
    • de programmes
  • Évolution du logicielle
  • Migration d'applications
  • Aide à la vérification
  • Traçabilité des transformations
  • Méthodes formelles

Thèse

Soutenance le vendredi 12 septembre 2014 à 13h30, au Loria, salle C005 (salle du conseil) ; ma thèse est accessible ici ou sur HAL.
Jury:

  • Rapporteurs :
    • Antoine Beugnard, Telecom Bretagne
    • Laurence Duchien, Université de Lille 1, LIFL (présidente du jury)
  • Examinateurs :
    • Mark van den Brand, Eindhoven University of Technology
    • Benoît Combemale, Université de Rennes 1, IRISA, Inria
    • Marc Pantel, Université de Toulouse, INPT, IRIT
  • Encadrant de thèse :
    • Pierre-Etienne Moreau, Université de Lorraine, École des Mines de Nancy, LORIA.
Mon sujet de thèse s'intitulait « Un îlot formel pour les transformations de modèles qualifiables » et s'inscrivait dans dans le cadre du projet Quarteft. Ce projet s'intéresse aux chaînes de développement de systèmes critiques qui reposent sur des langages de modélisation spécifiques au métier ciblé (Domain Specific Modeling Language) et sur des transformations qualifiées (assurance que la transformation préserve lis propriétés d'intérêt) entre languages. Le projet Quarteft vise à développer des technologies pour faciliter cette approche dans le contexte des sytèmes embarqués temps-réel. Le projet s'appuie d'une part sur la définition de langages pivots dédiés (DSML) et sur l'exploitation de techniques formelles pour spécifier et prouver la correction des transformations. L'étude proposée s'appuie sur le langage FIACRE, un des langages pivots pour la vérification formelle des aspects temps réel dans le projet TOPCASED ; il factorise et optimise la chaîne de traduction entre les langages métier tels que SDL, AADL, … et les outils de vérifications de modèles tels que TINA et CADP.

Je me suis donc intéressé à développer des techniques de spécification et d'implantation des transformations dont les cas d'applications étaient des extensions de FIACRE (dont RT-FIACRE pour des constructions plus abstraites spécifiques au temps réel), en ayant pour objectif de proposer des méthodes permettant de valider et de vérifier formellement ces transformations.

Pour implanter ces transformations, j'ai dans un premier temps proposé une méthode de transformation par réécriture en utilisant le langage Tom couplé à un langage hôte tel que Java, ainsi qu'un framework de modélisation comme EMF. J'ai ensuite étendu le langage Tom pour exprimer facilement ces transformations. J'ai créé un îlot formel dédié pour exprimer des transformations de modèles. J'ai aussi ajouté d'autres îlots formels au sein de Tom pour pour exprimer la traçabilité et pour résoudre le problème de l'ordre d'application des règles de réécriture.

Publications et exposés

Sur DBLP et HAL.

Liste des publications :

[9] Jean-Christophe Bach. Un îlot formel pour les transformations de modèles qualifiables Université de Lorraine, September 2014. PhD Thesis in French. [ bib | theses.fr| TEL | hal |  Local copy ]
[8] Martin Quinson and Jean-Christophe Bach. L'informatique nomade, c'est la liberté ! Interstices, February 2013. Popularization article in French. [ bib | hal | Interstices]
[7] Jean-Christophe Bach. Une approche hybride GPL-DSL pour transformer des modèles. pages 175-201, 3/33 2014. Technique et Science Informatiques, TSI. [ bib | hal |  Local copy ]
[6] Ali Afroozeh, Jean-Christophe Bach, Mark van den Brand, Adrian Johnstone, Maarten Manders, Pierre-Etienne Moreau, and Elizabeth Scott. Island Grammar-Based Parsing Using GLL and Tom. In Krzysztof Czarnecki and Görel Hedin, editors, Software Language Engineering, 5th International Conference, SLE 2012, volume 7745 of Lecture Notes in Computer Science, pages 224-243, Dresden, Germany, September 2012. Springer Berlin Heidelberg. [ bib | DOI   Local copy ]
[5] Jean-Christophe Bach, Pierre-Etienne Moreau, and Marc Pantel. Tom-Based Tools to Transform EMF Models in Avionics Context. In ITSLE, Dresden, Germany, September 2012. To appear. [ bib | DOI |  Local copy ]
[4] Jean-Christophe Bach, Pierre-Etienne Moreau, and Marc Pantel. EMF Models Transformations with Tom. In SLE, Dresden, Germany, September 2012. [ bib |  Local copy ]
[3] Jean-Christophe Bach, Xavier Crégut, Pierre-Etienne Moreau, and Marc Pantel. Model transformations with Tom. In Proceedings of the 12th Workshop on Language Descriptions, Tools, and Applications, LDTA '12, pages 4:1-4:9, Tallinn, Estonia, 2012. ACM. [ bib | DOI |  Local copy |  Slides ]
[2] Francisco Durán, Manuel Roldán, Jean-Christophe Bach, Emilie Balland, Mark Van Den Brand, James R. Cordy, Steven Eker, Luc Engelen, Maartje De Jonge, Karl Trygve Kalleberg, Lennart C. L. Kats, Pierre-Etienne Moreau, and Eelco Visser. The third rewrite engines competition. In Proceedings of the 8th international conference on Rewriting logic and its applications, WRLA'10, pages 243-261, Paphos, Cyprus, 2010. Springer-Verlag. [ bib | DOI| ACM | SpringerLink |  Local copy ]
[1] Jean-Christophe Bach, Emilie Balland, Paul Brauner, Radu Kopetz, Pierre-Etienne Moreau, and Antoine Reilles. Tom Manual. Rapport technique, PAREO - INRIA Lorraine - LORIA - INRIA - CNRS : UMR7503 - Université Henri Poincaré - Nancy I - Université Nancy II - Institut National Polytechnique de Lorraine, 2009. [ bib | hal | .pdf ]
EN Dernière modification : 2015-09-03