Technologie d'empaquetage pour la sûreté de fonctionnement des systèmes temps-réel

Les travaux présentés dans ce mémoire proposent un ensemble de techniques, ou " technologie ", pour le développement et la mise en œuvre efficaces de mécanismes d'empaquetage destinés à la tolérance aux fautes et à la caractérisation de la sûreté de fonctionnement des systèmes temps-réel. Les formalismes, les méthodes et les outils définis par cette technologie sont réunis dans un même environnement. Celui-ci constitue la base des " empaquetâches ", programmes produits automatiquement par compilation de spécifications formelles et exécutés de façon concomitante par une machine virtuelle. En raison de leur rôle majeur dans les systèmes temps-réel, nous avons appliqué cette technologie aux logiciels exécutifs du commerce de type micronoyau. Les empaquetâches pour la tolérance aux fautes sont alors déduits d'une spécification en logique temporelle des services fondamentaux des micronoyaux (ordonnancement, temporisation et synchronisation). Cette spécification sert de base à la détection et au recouvrement d'erreur, tout en s'appuyant sur le concept original d'action de recouvrement (variante d'une fonction élémentaire du système). En ce qui concerne les empaquetâches de caractérisation, la spécification formelle définit des injecteurs de fautes traditionnels, mais aussi novateurs (basés sur la notion de saboteur), ainsi que des sondes logicielles destinées à la mesure de propriétés temporelles et à l'observation de modes de défaillance. Nous avons introduit deux techniques fondamentales à la mise en œuvre effective des empaquetâches : la réflexivité du micronoyau, à des fins pratiques d'observation et de commande, et l'émulation de l'environnement, en vue de l'élimination de l'intrusion temporelle. La technologie d'empaquetage a été intégrée dans un outil d'évaluation (MAFALDA-RT) que nous avons appliqué à l'analyse par injection de fautes d'un système temps-réel bâti sur le micronoyau du commerce Chorus/ClassiX. Enfin, en s'appuyant sur les résultats d'évaluation et en enrichissant convenablement le test d'ordonnançabilité du système, nous avons déduit une méthode expérimentale permettant de déterminer les ensembles d'empaquetâches de tolérance aux fautes compatibles avec les échéances strictes des tâches temps-réel.TOULOUSE-ENSEEIHT (315552331) / SudocSudocFranceF