|
|
@@ -0,0 +1,60 @@
|
|
|
+Sources du document de thèse de Jean-Christophe Bach, soutenue publiquement le
|
|
|
+12/09/2014
|
|
|
+
|
|
|
+Jean-Christophe Bach's thesis sources, publicly defended the September 12th
|
|
|
+
|
|
|
+==============================================================================
|
|
|
+
|
|
|
+FRANÇAIS
|
|
|
+--------
|
|
|
+
|
|
|
+Titre : Un îlot formel pour les transformations de modèles qualifiables
|
|
|
+
|
|
|
+Résumé :
|
|
|
+
|
|
|
+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.
|
|
|
+
|
|
|
+
|
|
|
+Mots-clefs : réécriture, termes, transformation, modèles, traçabilité, qualification
|
|
|
+
|
|
|
+======================================================================
|
|
|
+
|
|
|
+ENGLISH
|
|
|
+-------
|
|
|
+
|
|
|
+Title: A formal island for qualifiable model transformations
|
|
|
+
|
|
|
+Abstract:
|
|
|
+
|
|
|
+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 purpose.
|
|
|
+
|
|
|
+
|
|
|
+Keywords: rewriting, terms, transformation, models, traceability, qualification
|
|
|
+
|
Jean-Christophe Bach