Responsable: Alain Girault
Titre: Synthèse de contrôleurs discrets pour la tolérance aux fautes Byzantines de capteurs
En raison de son aspect critique, la programmation des systèmes embarqués nécessite des méthodes de conception formelles . Parmi celles-ci, la synthèse de contrôleurs discrets a récemment connu des développements intéressants, avec notammen t la réalisation d’outils logiciels. Son principe consiste à spécifier, au sein d’un modèle unique (le plus souvent un s ystèmes de transitions étiquetées, appelé STE), tous les comportements possibles de l’application. Puis, à partir d’un objectif de comportements désirés, on synthétise automatiquement un contrôleur qui, mis en parallèle avec le STE de l’a pplication, empêche de se produire tous les comportements non désirés. Pour ce faire, le contrôleur coupe les transition s du STE qui mènent à des états non désirés. Pour que cela soit possible, l’ensemble des événements qui apparaissent dans les étiquettes des transitions du STE est partitionné en deux sous-ensembles : les événements contrôlables et les événements non contrôlables, le contrôleur n’ayant le droit de couper que les transitions étiquetées par des événeme nts contrôlables. Par conséquent, il se peut qu’un problème de synthèse de contrôleur n’ait pas de solution. La synthè se de contrôleurs discrets est une alternative à la vérification formelle, en ce sens qu’elle permet d’obtenir un systèm e qui vérifie un certains nombre de propriétés par construction, au lieu d’avoir à les vérifier après coup. Dans le ca dre de ce sujet de DEA, on s’intéresse plus particulièrement à la synthèse de contrôleurs discrets pour les systèmes t olérants aux fautes Byzantines. Les fautes Byzantines sont les plus générales qui soient. Les systèmes que l’on considè re ici sont équipés de capteurs Byzantins, qui peuvent produire des sorties fausses lorsqu’ils sont défaillants. Plus pr \uffffcisemment, ce travail va se baser sur une étude de cas, à savoir une cuve de liquide équipée de plusieurs capteurs de n iveau. Chaque capteur peut être mouillé ou sec, et l’objectif du contrôleur est de maintenir la cuve dans un état moyen ni à sec ni débordant. Dans le cas général des composants Byzantin, Lamport, Shostak et Pease ont démontré un résulta t fondamental : il faut qu’au minimum plus de deux tiers des composants soient corrects pour que le système fonctionne corr ectement. Dans le cas particulier de notre cuve, il s’agira de mettre en évidence ce résultat analytique , voire mieux pui sque les capteurs sont ordonnés et que l’eau subit la gravité.
Soutenance - 22 Juin 2005 - UFR IMA F309