Sources LaTeX du document de thèse de Jean-Christophe Bach

Jean-Christophe Bach 595a508cf3 * add a README with FR+EN abstracts and keywords il y a 10 ans
code f56da2b462 push thesis sources il y a 10 ans
cover f56da2b462 push thesis sources il y a 10 ans
figures f56da2b462 push thesis sources il y a 10 ans
publications f56da2b462 push thesis sources il y a 10 ans
tables f56da2b462 push thesis sources il y a 10 ans
Makefile f56da2b462 push thesis sources il y a 10 ans
README.md 595a508cf3 * add a README with FR+EN abstracts and keywords il y a 10 ans
abstract.tex f56da2b462 push thesis sources il y a 10 ans
appendices.tex f56da2b462 push thesis sources il y a 10 ans
arydshln.sty f56da2b462 push thesis sources il y a 10 ans
bach.bib f56da2b462 push thesis sources il y a 10 ans
ch-approach.tex f56da2b462 push thesis sources il y a 10 ans
ch-conclusion.tex f56da2b462 push thesis sources il y a 10 ans
ch-evaluation.tex f56da2b462 push thesis sources il y a 10 ans
ch-introduction.tex f56da2b462 push thesis sources il y a 10 ans
ch-notions.tex f56da2b462 push thesis sources il y a 10 ans
ch-outils.tex f56da2b462 push thesis sources il y a 10 ans
ch-tom.tex f56da2b462 push thesis sources il y a 10 ans
ch-traceability.tex f56da2b462 push thesis sources il y a 10 ans
ch-usecase.tex f56da2b462 push thesis sources il y a 10 ans
ch-verification.tex f56da2b462 push thesis sources il y a 10 ans
custom_pgf-umlcd.sty f56da2b462 push thesis sources il y a 10 ans
glossaire.tex f56da2b462 push thesis sources il y a 10 ans
macros.tex f56da2b462 push thesis sources il y a 10 ans
publisjcb.tex f56da2b462 push thesis sources il y a 10 ans
ref.bib f56da2b462 push thesis sources il y a 10 ans
remerciements.tex f56da2b462 push thesis sources il y a 10 ans
slashbox.sty f56da2b462 push thesis sources il y a 10 ans
test.tex f56da2b462 push thesis sources il y a 10 ans
these.brf f56da2b462 push thesis sources il y a 10 ans
these.tex f56da2b462 push thesis sources il y a 10 ans
thesul.cls f56da2b462 push thesis sources il y a 10 ans
thloria.cls f56da2b462 push thesis sources il y a 10 ans
tlfloat.sty f56da2b462 push thesis sources il y a 10 ans
tlhypref.sty f56da2b462 push thesis sources il y a 10 ans
tlnatbib.sty f56da2b462 push thesis sources il y a 10 ans
tulfloat.sty f56da2b462 push thesis sources il y a 10 ans
tulhypref.sty f56da2b462 push thesis sources il y a 10 ans

README.md

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