Description
Date depot: 1 janvier 1900
Titre: Bibliotheques de transformations de modeles d'architectures pour systemes avioniques
Directeur de thèse:
Laurent PAUTET (LTCI (EDMH))
Domaine scientifique: Sciences et technologies de l'information et de la communication
Thématique CNRS : Non defini
Resumé:
{{Contexte industriel}}
L’ingénierie dirigée par les modèles est aujourd’hui la méthode de choix pour le développement des systèmes avioniques. De la modélisation mathématique des lois physiques à la modélisation des systèmes de contrôle, en passant par celle des composants matériels, et celle des architectures des logiciels embarqués, les physiciens, automaticiens, et informaticiens tirent profit du pouvoir d’abstraction qu’apporte la modélisation. Les logiciels embarqués dérivés de cette approche contribuent de façon significative à la création de valeur du système final.
L’un des principaux intérêts de la modélisation dans le contexte industriel est la possibilité de génération automatique de l’application exécutable à partir des modèles décrivant le système. En effet, le concepteur ayant défini le système sous forme de modèles, est dispensé de l’écriture du code source correspondant grâce aux générateurs de code qui s’occupent de produire le code exécutable de l’application conformément aux modèles donnés en entrée.
Par ailleurs, les systèmes embarqués critiques sont soumis à des obligations de certification définies par des standards très stricts tels que le standard DO-178 pour l’avionique. Ainsi, pour qu’un système soit utilisable dans un contexte industriel, le concepteur doit valider la conformité de son application à des critères de certification très précis auprès des autorités adéquates. Entre autre, l’industriel est tenu de démontrer la conformité du code source et de l’exécutable final aux modèles et aux exigences de haut niveau en amont. La génération automatique de code y contribue dans la mesure où la transformation mise en œuvre peut garantir une préservation de propriétés entre le modèle et le code généré. Cette garantie, si existante, peut dispenser l’industriel de certaines tâches de vérification.
Cependant, cette dérogation est elle aussi réglementée par le standard, et n’est autorisée que lorsque le générateur de code est « qualifié » au sens du supplément pour la qualification d’outils du standard DO-178. Ainsi, pour que la génération de code soit réellement bénéfique dans le contexte de la certification, il faut que l’outil employé soit lui aussi conforme à des critères stricts permettant sa validation auprès des autorités de certification.
{{Problématique}}
La problématique de certification est aujourd’hui une préoccupation majeure des industriels ; cependant, malgré les apports de la génération automatique de code dans ce contexte, la mise en œuvre de cette méthode rencontre encore beaucoup de difficultés.
En pratique, la génération de code source est vue comme un cas particulier de la notion plus générale de « transformation de modèle ». Ainsi, en partant du modèle en entrée, la génération de code consiste en général en une série de transformations élémentaires, dont la dernière génère effectivement le code qui peut être lui aussi vu comme un modèle.
Pour qu’elles soient utiles dans le contexte de la certification, ces transformations doivent garantir une préservation de propriétés fonctionnelles et non-fonctionnelles de sorte que les vérifications faites au niveau des modèles soient toujours valables pour le code source et l’application exécutable. Or aujourd’hui, la préservation de ces propriétés n’est en général que partiellement vérifiée par des tests, mais sans aucune évidence formelle d’exactitude, ce qui limite la valeur ajoutée de la génération automatique de code dans le contexte de la certification.
Par ailleurs, les transformations de modèles sont classiquement définies à partir de besoins spécifiques à un utilisateur donné, un langage de modélisation et un processus industriel. Le développement bénéficie donc très rarement de la factorisation de besoins et de la réutilisation d’implémentations existantes. Par conséquent, le processus couteux de qualification d’un outil de génération automatique de code doit être toujours fait à partir de zéro.
Le manque de spécifications formelles accompagnant le processus de transformations de modèles ainsi que la faible réutilisation de celles-ci dans d’autres contextes applicatifs constituent deux facteurs fortement restrictifs pour le déploiement de l’ingénierie dirigée par les modèles dans le domaine embarqué critique.
{{Sujet de thèse}}
Cette thèse a pour objectif de pallier ce manque de spécifications formelles et cette faible réutilisation des transformations par la conception d’une architecture générique et extensible de transformateurs de modèles, et la définition d’une bibliothèque réutilisable de transformations pour les architectures de systèmes avioniques partitionnés temps-réel. Cette bibliothèque de transformations s’appuiera sur un formalisme pivot basé sur AADL et capable d’exprimer la structure et les comportements fonctionnels et non-fonctionnels de ces architectures. Des exemples typiques de cette bibliothèque seront des transformations horizontales à partir de et vers un form
Doctorant.e: Richa Elie