Contrôle de systèmes distribués.

Paul Gastin
LSV Cachan (France)
Friday, 15 April, 2005 (All day)
NO

Dans la panoplie des méthodes formelles utilisées pour assurer la sécurité des systèmes informatiques, la synthèse de contrôleurs constitue une approche particulièrement intéressante. Dans ce cadre, on suppose donnés d'une part un modèle de système ouvert (atelier de production, ...) dont les actions peuvent être soit contrôlables par programme soit incontrôlables (environnement) et d'autre part une spécification décrivant l'ensemble des comportements souhaitables. L'objectif est de synthétiser, si cela est possible, un contrôleur agissant uniquement sur les actions contrôlables de telle sorte qu'indépendamment des actions de l'environnement, les comportements du système restent corrects. Ce problème a été largement étudié dans le cadre séquentiel des systèmes à événements discrets depuis les travaux fondateurs de Ramadge et Wonham. Dans tous les cas raisonnables, on peut décider si le système est contrôlable et, si oui, synthétiser un contrôleur. L'intérêt principal de la synthèse de contrôleur est que l'on obtient des systèmes sûrs par construction, il est donc inutile de les vérifier ensuite.

La plupart des systèmes complexes aujourd'hui présentent des aspects distribués. Les processeurs exécutent plusieurs tâches simultanément, ils coopèrent et communiquent par échange de messages au travers de réseaux, ils doivent réagir aux stimuli d'un environnement, etc. De tels systèmes informatiques contrôlent des éléments critiques (centrales nucléaires, réseau ferré, ...) ou sont embarqués pour rendre des services cruciaux dans des véhicules, des cartes à puces, des téléphones, etc. Le problème du contrôle se pose donc très naturellement dans le cadre des systèmes distribués. La difficulté supplémentaire est liée au fait que les contrôleurs doivent être locaux aux composants du système et n'ont qu'une connaissance partielle des comportements puisqu'ils ne peuvent observer que localement ce qui se passe sur leur composant.

Les premiers travaux de Pnueli et Rosner sur le contrôle distribué étaient motivés par la synthèse de programmes pour les circuits. Ils ont naturellement considéré des systèmes totalement synchrones et ont montré que même pour des spécifications simples (LTL) le problème du contrôle est indécidable pour presque toutes les architectures de circuits. Les architectures décidables sont essentiellement de type "pipeline". Ces résultats ont été généralisés par Kupferman et Vardi pour des spécifications CTL^* et pour le mu-calcul et par Madhusudan et Thiagarajan pour des spécifications locales.

Les problèmes de contrôle sont souvent décrits et résolus en utilisant des jeux dans lesquels un joueur représente le contrôleur et son adversaire est l'environnement. Dans le cadre distribué, on considère plusieurs joueurs (les contrôleurs locaux) et un environnement. Il s'agit de jeux à information partielle puisqu'à nouveau la stratégie d'un joueur ne doit dépendre que de ce qu'il a pu observer localement. Mohalik et Walukiewicz ont utilisé cette approche dans le cadre du contrôle distribué, obtenant grâce à deux techniques de réduction tous les cas décidables précédents.

Avec Lerman et Zeitoun, j'ai reconsidéré le problème du contrôle distribué en changeant quelques hypothèses. D'une part, nous nous plaçons dans un cadre asynchrone et nous considérons des spécifications correspondant à des reconnaissables de traces de Mazurkiewicz. D'autre part, nous autorisons les contrôleurs à utiliser une mémoire causale plutôt qu'une mémoire purement locale. Cette mémoire causale, qui permet à un joueur de baser sa stratégie sur tout son passé causal, peut être implantée sur l'architecture considérée simplement en surchargeant les messages échangés dans l'exécution normale du système. Nous avons montré que sous ces hypothèses, le problème du contrôle distribué est décidable pour toutes les architectures série-parallèles et toutes les spécifications reconnaissables. Ce résultat positif contraste fortement avec les résultats essentiellement négatifs précédents.