• Langue : Anglais, Français
• Discipline : Automatique, Génie Informatique et Traitement du Signal
• Identifiant : 2009LIL10077
• Type de thèse : Doctorat
• Date de soutenance : 17/12/2009

Résumé en langue originale

Ces travaux de recherche présentent un nouveau cadre formel pour intégrer le diagnostic de fautes multiples et la reconfiguration. L'idée principale est d'utiliser STRIPS (Stanford Research Institute Problem Solver), un langage formel pour la planification automatisée qui peut intégrer les relations cause_effect et le mécanisme de raisonnement automatique dans un modèle. Le processus de diagnostic de fautes multiples et son module de vérification de cohérence sont basés sur le langage STRIPS. En outre, le modèle de faute est introduit dans le module de vérification de cohérence pour empêcher les diagnostics impossibles. Le langage STRIPS peut définir qualitativement le modèle de faute, sans nécessiter une connaissance précise et détaillée des composants défaillants. A partir des résultats du diagnostic, la reconfiguration met à jour le modèle du système. Elle vérifie que le modèle permet de réaliser les objectifs à partir d’une approche basée sur la vérification de modèle. Les objectifs sont pour ceci, exprimés à l’aide une logique temporelle.

Résumé traduit

This research presents a new formal framework for integrating multi-fault diagnosis and reconfiguration. The main idea is to use the STRIPS (STanford Research Institute Problem Solver), a formal language for automated planning which can integrate the cause_effect knowledge and the automated reasoning mechanism into one model. The multi-fault diagnostic process and its consistency-checking module are all based on the models defined by STRIPS actions. Moreover, the fault models are introduced into the consistency-checking module for preventing the impossible diagnoses. The STRIPS can qualitatively define the fault models without requiring detail and precise knowledge of faulty components. According to the results of diagnosis, the reconfiguration updates the system’s model. It uses the model checking to verify whether the updated model satisfies the desired objectives. These objectives are described by a temporal language.