A formal island for qualifiable model transformations

Le processus de développement logiciel est composé d'un grand nombre d'étapes qui intègrent de plus en plus d'outils. Les chaînes de développement de systèmes critiques (aéronautique, domaine médical) font appel à des outils de génération de code basés sur des modèles. Cette complexification a des conséquences sur la vérification des logiciels critiques. Les contraintes légales imposant qu'ils soient certifiés, la qualification des outils utilisés lors de leur développement est nécessaire. Dans cette thèse, nous nous proposons d'aider le processus de qualification en élaborant des méthodes et outils pour le développement fiable. Pour ce faire, nous présentons une méthode hybride de transformation de modèles par réécriture. Nous nous appuyons sur le langage Tom qui fournit de nouvelles fonctionnalités aux langages généralistes par l'ajout de constructions dédiées. Nous proposons aussi une traçabilité de ces transformations afin de répondre aux exigences de la qualification. La trace générée peut être utilisée a posteriori à des fins de vérification.Software development process is composed of steps which integrate an increasing number of tools. Development chains for critical systems (avionics, health field) have gradually adopted model-based code generation tools. This increase of complexity has consequences on critical software verification. As legal constraints require to certify them, tools used during the development have to be qualified. In this thesis, we propose to help the qualification process by providing methods and tools for liable development. To do so, we present an hybrid models transformation method based on rewriting. We rely upon Tom language which provides new features to general purposes languages by adding dedicated constructs. We also propose a traceability in order to respect qualification requirements. The generated trace can then be used for verification purpos