Qualification of source code generators in the avionics domain : automated testing of model transformation chains

Résumé : Dans l’industrie de l’avionique, les Générateurs Automatiques de Code (GAC) sont de plus en plus utilisés pour produire des parties du logiciel embarqué. Puisque le code généré fait partie d’un logiciel critique, les standards de sûreté exigent une vérification approfondie du GAC: la qualification. Dans cette thèse en collaboration avec AdaCore, nous cherchons à réduire le coût des activités de test par des méthodes automatiques et efficaces.La première partie de la thèse aborde le sujet du test unitaire qui assure une exhaustivité élevée mais qui est difficile à réaliser pour les GACs. Nous proposons alors une méthode qui garantit le même niveau d’exhaustivité en n’utilisant que des tests d’intégration de mise en œuvre plus facile. Nous proposons tout d’abord une formalisation du langage ATL de définition du GAC dans la théorie des Transformations Algébriques de Graphes. Nous définissons ensuite une traduction de postconditions exprimant l’exhaustivité du test unitaire en des préconditions équivalentes qui permettent à terme de produire des tests d’intégration assurant le même niveau d’exhaustivité. Enfin, nous proposons d’optimiser l’algorithme complexe de notre analyse à l’aide de stratégies de simplification dont nous mesurons expérimentalement l’efficacité.La seconde partie du travail concerne les oracles de tests du GAC, c’est à dire le moyen de valider le code généré par le GAC lors d’un test. Nous proposons un langage de spécification de contraintes textuelles capables d’attester automatiquement de la validité du code généré. Cette approche est déployée expérimentalement à AdaCore pour le projet QGen, un générateur de code Ada/C à partir de Simulink®.
Type de document :
Thèse
Computational Engineering, Finance, and Science [cs.CE]. Télécom ParisTech, 2015. English. 〈NNT : 2015ENST0082〉
Liste complète des métadonnées

Littérature citée [79 références]  Voir  Masquer  Télécharger

https://pastel.archives-ouvertes.fr/tel-01331877
Contributeur : Abes Star <>
Soumis le : mardi 14 juin 2016 - 16:52:26
Dernière modification le : jeudi 11 janvier 2018 - 06:23:39
Document(s) archivé(s) le : jeudi 15 septembre 2016 - 10:49:24

Fichier

TheseRicha.pdf
Version validée par le jury (STAR)

Identifiants

  • HAL Id : tel-01331877, version 1

Citation

Elie Richa. Qualification of source code generators in the avionics domain : automated testing of model transformation chains. Computational Engineering, Finance, and Science [cs.CE]. Télécom ParisTech, 2015. English. 〈NNT : 2015ENST0082〉. 〈tel-01331877〉

Partager

Métriques

Consultations de la notice

747

Téléchargements de fichiers

239