Français Anglais
Accueil Annuaire Plan du site
Accueil > Production scientifique > Thèses et habilitations
Production scientifique
Doctorat de IBRAHIM Hassan
IBRAHIM Hassan
Doctorat
Equipe : Données et Connaissances Massives et Hétérogènes

Analyse à base de SAT de la diagnosticabilité et de la prédictibilité des systèmes à événements discrets centralisés et distribués

Début le 07/01/2013
Direction : SIMON, Laurent
[DAGUE Philippe]

Financement : ETR
Etablissement d'inscription : Université Paris-Sud
Lieu de déroulement : LRI-IASI

Soutenue le 16/12/2016 devant le jury composé de :
Directeur de thèse :
M. Philippe Dague, Professeur, Université Paris-Sud

Co-directeur de thèse :
M. Laurent Simon, Professeur, Université de Bordeaux

Rapporteurs :
- M. Stéphane Lafortune, Professeur, University of Michigan
- M. Lakhdar Saïs, Professeur, Université d'Artois

Examinateurs :
- M. Stefan Haar, Directeur de recherche, Inria & ENS Cachan
- M. Hervé Marchand, Chargé de recherche, Inria & Université de Rennes 1

Activités de recherche :

Résumé :
Les systèmes complexes sont omniprésents dans nos vies, mais sujets à des pannes qu’il est important de détecter ou de prédire. Leur modélisation comme des systèmes à événements discrets (SED) est un moyen naturel de les représenter pour les étudier formellement. Ainsi, un système peut être décrit par un ensemble d'états tels que son état actuel est obtenu après avoir déclenché une séquence d'événements. Ces événements sont prédéfinis dans un ensemble fini et peuvent être déclenchés spontanément dans le système. Tous ces événements ne sont pas observables / mesurables et certains d'entre eux sont considérés comme fautifs, donc ils modélisent un changement anormal entre deux états du système.

Le processus de diagnostic de SED a pour but de déterminer avec certitude si le système est actuellement dans un état défectueux ou dans un état normal, c'est-à-dire si un changement anormal d'un état du système s'est produit ou non. À cette fin, un observateur du système ne dispose que de la séquence d'événements observables pour décider le diagnostic de l'état actuel du système. Cependant, cet état peut être ambigu (normal ou défectueux) en fonction des observations disponibles. En outre, il peut être définitivement ambigu ! La possibilité de le désambiguïser en utilisant un nombre fini d'observations est appelée la diagnosticabilité d'une occurrence d'événement fautif. La faute est diagnosticable si toutes ses occurrences le sont et le système est diagnosticable si toutes ses fautes le sont. De même, la possibilité de prédire une occurrence future d'une faute en utilisant les événements observables la précédant est appelée la prédictibilité d'un événement fautif. Les deux problèmes de la diagnosticabilité et de la prédictibilité d'un événement peuvent être généralisés pour étudier celles d'un motif d’événements, soit un langage clos par extension représenté par une machine à états finis.

Cette thèse considère dans sa première partie les problèmes de vérification de la diagnosticabilité et de la prédictibilité d'un événement fautif et de la diagnosticabilité d'un motif d'événements dans les systèmes à événements discrets centralisés et distribués (avec des événements de communication synchrone observables ou non), à l'aide de solveurs SAT. Ainsi, nous les avons encodés comme des problèmes SAT, avons étudié des variantes incrémentales et fourni des résultats expérimentaux qui prouvent le passage à l’échelle et la flexibilité de cette approche. Dans la deuxième partie, nous avons introduit le problème de la planification de la diagnosticabilité. Ce problème consiste à trouver un plan d'actions (une séquence d'événements intentionnels prédéfinis à la conception) qui garantit, lorsqu'il est appliqué à un ensemble donné d'états potentiels du système actuel appelé état courant de croyances, de conduire le système dans un état de croyances diagnosticable d’où on peut le laisser s'exécuter librement (sans les actions de contrôle). Ce problème peut survenir après une intervention externe sur le système, comme par exemple l'application d'un plan de réparation après la détection d'une faute. Ainsi, cette approche peut garantir la possibilité de détecter d'autres futures fautes du système. Nous avons analysé ce problème et prouvé qu’il est PSpace-complet puis nous avons proposé trois méthodes pour engendrer un plan diagnosticable, que nous avons comparées sur un banc d’essais créé à cette fin.