Mise en 
uvre de la tolérance aux fautes par des
transformations automatiques de programmes
Nous avons proposé une approche formelle pour rendre automatiquement
tolérant aux fautes un système initialement non tolérant aux
fautes. Le système initial est constitué d'un ensemble de tâches
périodiques indépendantes, ordonnancées sur un ensemble de processeurs
à silence sur défaillance connectés par un réseau de communication
parfaitement fiable. Notre but est que, en supposant la présence d'un
processeur supplémentaire, le système final tolère une faute à la fois
d'un processeur (permanente ou non). La détection des fautes est
réalisée grâce à du « heartbeating » périodique, et le masquage par
des points de reprise périodiques (« checkpointing & rollback »). Le
principe de notre méthode est de transformer le code exécuté par
chaque tâche pour qu'il mette en uvre ces techniques. Chaque
transformation est formellement représentée par des règles de
transformation. Cette approche formelle illustre l'intérêt de la
séparation des préoccupations et nous a permis de démontrer
formellement que le système final tolère une faute tout en continuant
à satisfaire des contraintes de temps d'exécution
maximal [3].
En prenant cette approche comme point de départ, nous travaillons actuellement à la définition d'un langage d'aspects permettant de tisser différentes techniques de tolérance aux fautes dans des programmes temps-réel.
Pascal Raymond 2006-11-16
