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

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

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