Qualification of source code generators in the avionics domain : automated testing of model transformation chains - PASTEL - Thèses en ligne de ParisTech Accéder directement au contenu
Thèse Année : 2015

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

Qualification des générateurs de code source dans le domaine de l'avionique : le test automatisé des chaines de transformation de modèles

Résumé

In the avionics industry, Automatic Code Generators (ACG) are increasingly used to produce parts of the embedded software. Since the generated code is part of critical software, safety standards require a thorough verification of the ACG called qualification. In this thesis in collaboration with AdaCore, we seek to reduce the cost of testing activities by automatic and effective methods.The first part of the thesis addresses the topic of unit testing which ensures exhaustiveness but is difficult to achieve for ACGs. We propose a method that guarantees the same level of exhaustiveness by using only integration tests which are easier to carry out. First, we propose a formalization of the ATL language in which the ACG is defined in the Algebraic Graph Transformation theory. We then define a translation of postconditions expressing the exhaustiveness of unit testing into equivalent preconditions that ultimately support the production of integration tests providing the same level of exhaustiveness. Finally, we propose to optimize the complex algorithm of our analysis using simplification strategies that we assess experimentally.The second part of the work addresses the oracles of ACG tests, i.e. the means of validating the code generated by the ACG during a test. We propose a language for the specification of textual constraints able to automatically check the validity of the generated code. This approach is experimentally deployed at AdaCore for a Simulink® to Ada/C ACG called QGen.
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®.
Fichier principal
Vignette du fichier
TheseRicha.pdf (3.91 Mo) Télécharger le fichier
Origine : Version validée par le jury (STAR)
Loading...

Dates et versions

tel-01331877 , version 1 (14-06-2016)

Identifiants

  • HAL Id : tel-01331877 , version 1

Citer

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⟩
320 Consultations
439 Téléchargements

Partager

Gmail Facebook X LinkedIn More