Abstract FR:

L'utilisation de micronoyaux du commerce s'impose aujourd'hui dans le cadre de la conception de systemes, meme soumis a de fortes contraintes de surete de fonctionnement, comme une approche de plus en plus attractive. Les travaux presentes dans ce memoire ont pour objectif de proposer des reponses aux interrogations soulevees par cette nouvelle tendance. Nous developpons une methode d'evaluation et d'amelioration des proprietes de surete de fonctionnement d'un micronoyau du commerce. Tout d'abord, nous justifions la pertinence de l'injection de fautes pour la caracterisation des modes de defaillance d'un micronoyau. Nous presentons les lignes directrices qui ont conduit au developpement d'un outil d'evaluation par injection de fautes, pour l'aide a la conception de micronoyaux : mafalda. Par la suite, nous utilisons mafalda pour l'analyse du micronoyau commercial chorus/classix. A partir des lecons tirees de cette etude, nous proposons des recommandations pour ameliorer les proprietes de surete de fonctionnement du micronoyau, selon le point de vue du fournisseur et des developpeurs de systemes. Ensuite, nous developpons une approche novatrice de confinement des erreurs, d'origines externe et interne, pouvant affecter un micronoyau. La solution proposee s'appuie sur une modelisation du comportement attendu des classes fonctionnelles en absence de faute, a partir de laquelle il est possible de definir un ensemble de predicats. Nous appliquons cette approche aux classes de synchronisation et d'ordonnancement de taches. Pour mettre en uvre ces predicats, nous introduisons un mecanisme d'encapsulation original, base sur la notion de reflexivite. Ce concept est illustre sur le micronoyau chorus/classix. Enfin, nous utilisons mafalda pour evaluer de facon objective les benefices procures par les mecanismes d'encapsulation.