Description
Date depot: 1 janvier 1900
Titre: Méthodes formelles et langages de haut niveau pour logiciels embarqués
Encadrant :
Frédéric PESCHANSKI (LIP6)
Directeur de thèse:
Emmanuel CHAILLOUX (LIP6)
Domaine scientifique: Sciences et technologies de l'information et de la communication
Thématique CNRS : Non defini
Resumé:
{{Contexte}}
Le développement de logiciel critique repose sur deux piliers fondamentaux : (1) un effort notable est consacré à l'élaboration de spécifications précises, et (2) des contraintes fortes sont imposées sur l'activité de programmation. Dans le monde de l'embarqué, les besoins en terme de spécifications sont souvent très importants, notamment en raison d'aspects liés à la sûreté de fonctionnement. Pour les mêmes raisons, les contraintes de programmation sont très fortes et la plupart des traits de haut niveau sont écartés: structures de données complexes (listes, arbres, graphes, etc.) ainsi que les structures de contrôles comme les exception, le dispatch dynamique, les fermetures, etc. Il existe donc une tension entre le haut niveau d'abstraction généralement requis par la spécification fonctionnelle, et le bas niveau imposé sur la programmation du logiciel. La démarche de développement par raffinement, au coeur des méthodes formelles comme B [1] (mais également Z ou VDM), permet d'offrir une certaine latitude concernant la spécification. Mais dans la plupart des cas, la machine concrète ciblés par la méthode est fixée à l'avance, et correspond à une machine assez bas niveau. Le principal avantage concerne la décharge des obligations preuves (PO) qui est souvent 'automatique'. La contrepartie est claire: la relativement faible expressivité du formalisme de spécification.
{{Projet}}
L'objectif du projet est de s'appuyer sur la démarche de développement par raffinement de logiciel embarqué, mais en introduisant des traits de haut niveau caractéristiques de la programmation fonctionnelle : structures de données inductives (listes, arbres, graphes fonctionnels, etc.) et algorithmes récursifs. L'intérêt est bien sûr de faciliter et d'accélérer le développement du logiciel. Les spécifications peuvent être élaborées à un plus haut niveau d'abstraction. Le processus de raffinement est raccourci puisque une machine concrète de plus haut niveau est disponible. En contrepartie, la validation des obligations de preuve est potentiellement plus difficile: en particulier se pose la question de l'automatisation. De plus, certains traits de haut niveau - notamment les structures de données immutables - imposent un support à l'exécution (ex.: un ramasse-miettes) qui lui-même induit des questions liées à la sûreté de fonctionnement (et, dans une moindre mesure, des questions d'efficacité).
Doctorant.e: Sall Boubacar Demba