• Langue : Français
• Discipline : Sciences mathématiques. Informatique
• Identifiant : Inconnu
• Type de mémoire : Habilitation à diriger des recherches
• Date de soutenance : 01/01/2006

Résumé en langue originale

Les différentes évolutions du génie logiciel ont introduit de plus en plus de souplesse pour les utilisateurs et de plus en plus de contraintes pour les plates-formes techniques. Les modèles objet puis les modèles à composants ont fait évoluer les applications d'entités monolithiques à des objets actifs, distribués, communicants, à des composants assemblables, réutilisables, facilement maintenables. Ces nouvelles manières de concevoir les applications ont créé de nouveaux besoins technologiques en matière de supports d'applications, mais également renforcé le besoin de maitrise du comportement de ces entités logicielles. La vue du logiciel en tant qu'assemblage de briques élémentaires nécessite une grande confiance en la qualité des briques : La durée de vie des éléments s'allonge, ils sont sujets à intégration, composition, au chargement dynamique, une partie du code peut être mobile et produite par un fournisseur externe. Nous abordons dans ce travail, à travers divers problèmes et applications, la sürété de fonctionnement en contexte objet, distribué, ouvert, pour des systèmes extensibles, supportant l'adaptabilité ou la mobilité. En particulier, nous nous intéressons aux apports des constructions orientées objet dans ce domaine et à la manière dont on peut assurer la sùreté de fonctionnement et dans certains cas des propriétés de sécurité en restant le plus proche possible des préoccupations et des habitudes des programmeurs. Nous nous efforçons au cours des sujets abordés d'imposer le moins de contraintes possible et de proposer des solutions faciles d'utilisation, de restreindre au minimum l'usage des mécanismes objet, au prix de l'expressivité si nécessaire. Pour traiter l'aspect ouvert des systèmes. nous proposons d'utiliser exclusivement un raisonnement local qui ne repose pas sur un état du contexte à un instant donné. Enfin, pour ne pas pénaliser les performances des systèmes, les solutions que nous proposons restent dans le cadre de vérifications ou d'analyses statiques même si nous raisonnons sur des comportements intrinsèquement dynamiques. Dans la première partie, nous nous intéressons aux systèmes orientés objet. Nous proposons une spécification à base de traces de communication qui permet le raisonnement formel et en particulier prend en compte les aspects liés au modèle objet ainsi que l'ouverture et l'extensibilité de ces systèmes. La deuxième partie aborde la spécification de composants logiciels en s'attachant, à proposer un modèle formel, théoriquement fondé et proche des solutions technologiques industrielles ou proposées par les grands consortia. Ces travaux peuvent étre vus comme une adaptation des réflexions menées dans le cadre des systèmes orientés objet aux systèmes à base de composants logiciels. Ils s'attachent en particulier à la compositionnalilé du modèle. Enfin. la troisième partie s'intéresse plus particulièrement aux propriétés de sécurité des systèmes embarqués ouverts. basés sur des modèles objet. permettant le chargement dynamique de composants applicatifs ou système et propose un algorithme de vérification pour les petlls systèmes embarqués dans le cadre du chargement de code mobile. Ces travaux ont été menés au sein de l'équipe STC du LlFL. La première partie dans le cadre d'un projet de l'université d'Oslo. la seconde dans le Cadre d'un partenariat avec la société NORSYS, enfin, la dernière, en collaboration, avec le projet POPS de l'INRIA Futurs.