Model-based techniques for the future integration for formal verification of critical real-time software systems

Résumé

Les architectures avioniques modulaires intégrées combinées avec la norme SAE TTEthernet constituent une infrastructure solide pour le déploiement des applications avioniques a criticités mixtes ayant des exigences strictes en termes de sécurité, fiabilité et de performance. L’intégration de tels systèmes est une tâche d’ingénierie complexe et difficile. Par conséquent, l’approche basée sur les modèles qui offre aux ingénieurs systèmes une méthodologie et les outils de support pour maitriser cette complexité, est d’une grande importance. Dans cette thèse, nous présentons une extension pour le langage de modélisation AADL pour supporter la modélisation des applications avioniques à criticités mixtes déployées sur des architectures IMA basées sur TTEthernet. En particulier, nous présentons un méta-modèle qui étend le métamodèle de base de AADL avec les concepts et les contraintes de ce domaine. Nous définissons une syntaxe textuelle concrète pour cette extension ainsi que l’implémentation de cette extension en utilisant l’outil OSATE. Par la suite, on construit par-dessus notre extension du langage AADL et nous utilisons les transformations de modèles pour supporter la vérification des modèles de systèmes produits avec cette méthodologie. En particulier, nous proposons une transformation des modèles de systèmes en modèles convenables à la simulation avec DEVs. Finalement, nous illustrons l’approche proposée via une étude de cas fournies par Bombardier, notre partenaire industriel dans le projet. Nous utilisons cette étude de cas pour démontrer notre extension et procéder à la vérification de la contrainte contention-freedom d’un ordonnancement TTEthernet.

Date	19 oct. 2016
langue originale	Anglais américain
Établissement diplômant	École de technologie supérieure
Superviseur	Abdelouahed Gherbi (Directeur(-trice))