Diagnostic des systèmes dynamiques hybrides
Diagnostic des systèmes dynamiques hybrides
THESE EN COTUTELLE
par
Haithem DERBEL
le 18 Décembre 2009
Titre :
Directeurs de thèse :
JURY :
M. René DAVID DR Émérite CNRS Président du jury
M. Hervé GUEGUEN SUPELEC Rennes Rapporteur
M. Moncef TAJINA ENSI - Tunisie Rapporteur
M. Moez YEDDES ENSI - Tunisie Examinateur
M. Hassane ALLA UJF - Grenoble I Examinateur
M. Néjib BEN HADJ-ALOUANE ENSI - Tunisie Examinateur
A la mémoire de mon père,
à ma mère,
à ma chère Emna
et à tous ceux qui pensent à moi...
Remerciements
Ce mémoire marque une étape importante dans ma vie. Je voudrais remercier ici
toutes les personnes qui m’ont accompagné pour accomplir l’un des plus importants
projets professionnels de ma vie
Je tiens avant tout à exprimer ma profonde reconnaissance à Monsieur Hassane ALLA
et Monsieur Néjib BEN HADJ-ALOUANE, qui ont assuré la direction de cette thèse.
Je les remercie pour l’aide scientifique qu’ils m’ont toujours apporté, mais surtout pour
leur disponibilité, leur soutien et leurs encouragements. Des remerciements très spéciaux
pour Monsieur Moez YEDDES, pour toutes les discussions fructueuses, les critiques
constructives et l’aide considérable qui ont contribué au contenu de cette thèse.
Je tiens à remercier Monsieur Moncef TAJINA, Professeur à l’Ecole Nationale des
Sciences de l’Informatique de Tunis, d’avoir accepté avec Monsieur Hervé GUEGUEN,
Professeur à Supelec de Rennes, d’étudier mes travaux et d’en être les rapporteurs ainsi
que pour l’intérêt et l’attention qu’ils ont accordés à cette étude. Je remercie énormément
les membres du jury pour les conseils et remarques qui m’ont beaucoup aidé à la finalisa-
tion de ce document : René DAVID, président du jury, Directeur de Recherche au CNRS,
Moez YEDDES Maitre-Assistant à l’Ecole Nationale des Sciences de l’Informatique de
Tunis.
Je suis également reconnaissant au soutien financier apporté par le projet de coopéra-
tion Franco-Tunisien CMCU. Ce soutien, attribué par le Ministère des affaires étrangères
et européennes, a été géré par l’EGIDE, que je tiens également à les remercier respecti-
vement.
Mes remerciements vont à tout le personnel du laboratoire Gipsa-lab et de l’unité de
recherche OASIS qui m’ont accueilli durant ces trois années. L’ambiance chaleureuse est
propice à un travail efficace.
Je tiens tout particulièrement à remercier tous les doctorants du laboratoire (Amine,
Cedric, Andra, Van, Hala, Mohamed, Irfan, Lizeth, Adib, Oumayma, Joumana, Simona,
Hu, et les autres . . .), pour l’ambiance sympathique qu’ils ont réussi à instaurer.
Je tiens à exprimer mon éternelle gratitude à ma chère mère qui m’a toujours soutenu
tout au long de mon cursus. Parce qu’elle trouve dans l’achèvement de ce travail l’abou-
tissement de ses efforts et ses sacrifices. J’exprime ma gratitude à ma chère Emna qui a
toujours été ma motivation la plus importante et qui a été disponible pour m’encourager
à achever ce travail. Je remercie tous les membres de ma famille (Wided, Mohamed,
Mourad, mon cousin Sami, Cyrine et mon petit choux Slim) pour tous leurs encourage-
ments.
Je ne pourrais pas terminer sans exprimer un remerciement venant du plus profond
du coeur à tous mes amis qui m’ont toujours soutenu pendant mes années d’étude (Adel,
Hédi, Amine, Imène, Mehdi, Wissem, Youssef, Dilouma, Yamen, Iyed, Khabeb, Ghassen,
Rayène et les autres . . .).
Table des matières
1 Introduction générale 17
7
3.5.1 Contributions fondées sur des approches continues . . . . . . . . . 59
3.5.2 Contributions fondées sur des approches SED . . . . . . . . . . . 61
3.6 Etude de la diagnosticabilité . . . . . . . . . . . . . . . . . . . . . . . . . 63
3.6.1 Diagnosticabilité des SED selon l’approche de Sampath . . . . . . 63
3.6.2 Diagnosticabilité des SED à aspect temporel . . . . . . . . . . . . 65
3.7 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67
B Preuves 165
B.1 Preuves du chapitre 4 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 165
B.2 Preuves du chapitre 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 169
Bibliographie 173
Table des figures
11
Table des figures
12
Table des figures
5.5 Futur d’un polyhèdre hx ∈ [1, 3] ∧ y ∈ [0, 2]i sur une fonction de flux
hẋ = 1 ∧ ẏ ∈ [1, 3]i . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 130
5.6 Schéma du diagnostic en-ligne à base d’automates hybrides rectangulaires 132
5.7 Modèle automate hybride rectangulaire d’un système de chauffage de liquides133
5.8 Sommets accessibles par des exécutions correspondant à de différents
modes de fonctionnement . . . . . . . . . . . . . . . . . . . . . . . . . . . 136
5.9 Modèle obtenu après la l’application de la transformation . . . . . . . . . 136
5.10 Restriction du comportement normal H0 . . . . . . . . . . . . . . . . . . 137
5.11 Diagramme d’exécution de la procédure de diagnostic. . . . . . . . . . . . 139
5.12 Etude de la diagnosticabilité à HTL d’un AHR. . . . . . . . . . . . . . . 148
5.13 L’AHR T B θ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 151
5.14 Les AHRs H1 et H1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 153
5.15 L’AHR H1,1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 154
5.16 Les AHRs H2 et H2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 154
5.17 L’AHR H2,2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 155
θ
5.18 Exemple de l’accessibilité d’un sommet marqué dans l’AHR H1,1 . . . . . . 156
13
Table des figures
14
Liste des Algorithmes
1 Pseudo-code du diagnostiqueur . . . . . . . . . . . . . . . . . . . . . . . 52
2 Fonction d’accessibilité non-observable UR . . . . . . . . . . . . . . . . . 96
3 Procédure de synthèse du diagnostiqueur . . . . . . . . . . . . . . . . . . 104
4 Fonction d’analyse d’accessibilité : Accessible . . . . . . . . . . . . . . . 130
5 Fonction d’accessibilité non-observable à temps-borné T R . . . . . . . . 141
6 Procédure de diagnostic . . . . . . . . . . . . . . . . . . . . . . . . . . . 142
7 Procédure diagnosticable . . . . . . . . . . . . . . . . . . . . . . . . . . . 149
8 Fonction d’accessibilité non-observable UR enrichie . . . . . . . . . . . . 163
9 Procédure de synthèse du diagnostiqueur enrichi . . . . . . . . . . . . . . 164
15
Liste des Algorithmes
16
Chapitre 1
Introduction générale
17
Chapitre 1. Introduction générale
18
Chapitre 1. Introduction générale
Contributions de la thèse
19
Chapitre 1. Introduction générale
contribution par rapport aux travaux existants dans la littérature. Dans un premier vo-
let, nous rappelons le cadre de modélisation des SED et des SDH. Nous présentons les
caractéristiques de chacun de ces systèmes ainsi que quelques outils permettant leur mo-
délisation. Dans un deuxième volet, nous présentons un survol des principales méthodes
de diagnostic des SED et de SDH évoquées dans la littérature.
Le troisième chapitre présente notre démarche de diagnostic pour les systèmes tem-
porisés. Il expose, autour d’un exemple, les différentes étapes nécessaires pour la synthèse
en-ligne du diagnostiqueur à partir d’un modèle automate temporisé du système (Der-
bel et al., 2009c). Nous commençons par présenter formellement le modèle automate
temporisé, ses outils d’analyse ainsi que les différentes hypothèses retenues pour per-
mettre la construction du diagnostiqueur. Ensuite, nous détaillons l’algorithme employé
pour la synthèse hors-ligne du diagnostiqueur à partir du modèle considéré. Enfin, nous
présentons une notion de diagnosticabilité pour le modèle considéré. Une méthode sys-
tématique de vérification de cette notion, reposant sur la détection de cycles spéciaux
dans le modèle diagnostiqueur, est proposée.
Le dernier chapitre est consacré à la présentation de notre approche de diagnos-
tic d’une sous-classe de systèmes dynamiques hybrides (Derbel et al., 2009b,d). D’abord,
nous rappelons le cadre de modélisation considéré dans notre contribution : les automates
hybrides rectangulaires, ainsi les méthodes permettant l’analyse comportementale de ce
modèle. Nous détaillons par la suite notre démarche de diagnostic de ces systèmes. Cette
démarche commence par caractériser les différentes hypothèses de modélisation permet-
tant l’application de notre méthode de diagnostic et la vérification de diagnosticabilité.
Ensuite, nous exposons intuitivement puis formellement notre procédure de diagnostic
en-ligne. Une notion de diagnosticabilité pour la sous-classe de modèles considérée est
définie. Nous proposons enfin une méthode permettant la vérification systématique de
cette diagnosticabilité.
20
Chapitre 2
2.1 Introduction
Durant ces dernières décennies, l’automatisation des systèmes industriels vise à aug-
menter les performances de production ainsi que la qualité du produit à travers sa tra-
çabilité et la diminution des coûts de sa fabrication. Dans ce contexte, les systèmes
de surveillance des équipements industriels jouent un rôle important pour maintenir la
disponibilité des machines et les lignes de production.
Un système de surveillance observe en continu l’évolution des équipements à tra-
vers des données quantifiables et/ou qualifiables collectées à partir du système surveillé.
Ces données permettent de signaler au bon moment à l’opérateur les écarts détectés
par rapport au comportement nominal prévu. Ceci permettra de mettre en oeuvre les
actions préventives et correctives. Plusieurs chercheurs ont abordé la thématique de la
surveillance industrielle mettant ainsi en évidence l’intérêt manifesté par la communauté
scientifique ainsi que les industriels par rapport à cette problématique. Les approches de
surveillance sont généralement divisées en deux catégories : les approches de surveillance
avec modèles et les approches de surveillance sans modèles. Les premières se basent sur
l’existence d’un modèle formel de l’équipement et utilisent généralement les techniques
de l’automatique (Combacau, 1991). Dans la deuxième catégorie de méthodologies, le
modèle du procédé est inexistant ou difficile à obtenir, et elles se basent ainsi sur des
techniques statistiques ou issues du domaine de l’Intelligence Artificielle (IA).
L’objectif de ce chapitre est de présenter les concepts fondamentaux liés au diagnostic
et à la surveillance des systèmes automatisés. Dans un premier temps, nous présentons le
contexte de notre étude à savoir, les systèmes automatisés de production. Dans la littéra-
ture de la surveillance et du diagnostic, on peut trouver plusieurs définitions quelquefois
21
Chapitre 2. Diagnostic des défauts dans les systèmes automatisés
divergentes. C’est la raison pour laquelle nous donnons les définitions des mots clés né-
cessaires pour la compréhension de ce rapport. Enfin, nous présentons une classification
non exhaustive des méthodes de diagnostic des défauts rencontrées dans la littérature.
22
Chapitre 2. Diagnostic des défauts dans les systèmes automatisés
Les SAP peuvent être caractérisés à travers la dynamique exprimant leur fonctionne-
ment. Selon l’objectif considéré, il y a trois abstractions possibles pour modéliser cette
dynamique : les systèmes continus, les systèmes à événements discrets et les systèmes
dynamiques hybrides (Dousson, 2007).
23
Chapitre 2. Diagnostic des défauts dans les systèmes automatisés
continu et discret. Ces systèmes évoluent dans le temps et combinent des variables conti-
nues et des variables discrètes (Ben Hadj-Alouane et al., 2006). Un état discret du sys-
tème peut être vu comme un système continu avec des variables continues reliées par des
contraintes. Cependant, la portée de ces contraintes est restreinte à l’état en question.
La transition du système d’un état à un autre fait changer son mode de fonctionnement
en lui faisant subir d’autres lois continues propres au nouvel état.
L’utilisation des SAP dans le milieu industriel doit répondre à des objectifs prédé-
finis. Malheureusement, cette utilisation peut être confrontée à des dysfonctionnements
non prévus dont les conséquences sont désastreuses pour la sécurité des hommes et des
équipements. Les dysfonctionnements peuvent être de deux types : externes ou in-
ternes (Combacau et al., 2002; Deschamps, 2007).
Les dysfonctionnements externes peuvent venir :
• d’un problème dans la matière première. Par exemple, la rupture du stock d’une
matière première, ou la non conformité de la qualité par rapport aux exigences de
fabrication, . . . ;
• des aléas de l’environnement du système. Par exemple, un court circuit causant
une coupure de l’alimentation électrique d’un SAP, . . . ;
• d’une modification de la commande par le client. Par exemple, un changement dans
la spécification du produit, . . ..
Les dysfonctionnements internes peuvent être dus :
• à un problème physique dans la PC. Par exemple, une mauvaise communication,
une panne du calculateur, . . . ;
• à un problème logiciel dans la PC. Par exemple, un bogue de programmation, le
plantage du système d’exploitation, . . . ;
• à un problème dans la PO. Par exemple, la détérioration d’un composant physique,
d’un capteur ou d’un actionneur, . . ..
24
Chapitre 2. Diagnostic des défauts dans les systèmes automatisés
La diversité des terminologies trouvées dans différents travaux fait que nous avons
jugé important d’établir un lexique sur les termes qui seront utiles pour la compréhension
du présent rapport. Nous présentons dans la suite quelques définitions extraites des
références suivantes : (Villemeur, 1988; Combacau, 1991; Toguyeni, 1992; Lefebvre, 2000;
Zemouri, 2003; Philippot, 2006; Deschamps, 2007)
Définition 1. Défaut : c’est une déviation du système par rapport à son comportement
normal, qui ne l’empêche pas de remplir sa fonction. Un défaut est donc une anomalie
qui concerne une ou plusieurs propriétés du système, pouvant aboutir à une défaillance
et parfois même à une panne.
25
Chapitre 2. Diagnostic des défauts dans les systèmes automatisés
Définition 2. Dégradation : tout état qui se caractérise par une évolution irréversible
des caractéristiques d’un système est une dégradation. La dégradation peut être liée à
des facteurs directs, tels que l’usage, le temps. . ., ou à des facteurs indirects, tels que
l’humidité, la température. . .. La dégradation peut aboutir à une défaillance, quand les
performances du système sont en dessous d’un seuil d’arrêt défini par les spécifications
fonctionnelles.
Une défaillance implique l’existence d’un défaut, puisqu’elle aboutit à un écart entre
la caractéristique mesurée et la caractéristique de référence. Inversement, un défaut ne
conduit pas nécessairement à une défaillance. En effet, le système peut très bien conser-
ver son aptitude à assurer une fonction requise, si les défauts qui l’affectent n’ont pas
d’impacts significatifs sur la mission. Si une défaillance peut conduire à une cessation de
l’exécution de la mission principale du système, ce dernier est déclaré en état de panne.
Ainsi, la panne est toujours le résultat d’une défaillance.
26
Chapitre 2. Diagnostic des défauts dans les systèmes automatisés
Les SAP sont généralement caractérisés par la complexité de leurs structures, puis-
qu’ils imbriquent de nombreux éléments complexes de la PO. Le taux d’apparition de
pannes dans un système augmente en fonction de la complexité de sa structure, ce qui
rend la tâche d’analyse de ces pannes difficile. Cette difficulté justifie la nécessité de
disposer d’un système de surveillance permettant d’alerter l’opérateur en cas de pannes,
afin de pouvoir décider à temps des actions correctives.
[Link] Surveillance
[Link] Détection
La fonction de détection permet de discerner tout écart du système par rapport à son
état de fonctionnement normal. Autrement dit, elle permet de déterminer la présence
de défauts dans un système. Pour assurer cette fonction, il est indispensable de pouvoir
distinguer entre les situations normale et anormale. Cette fonction représente très souvent
un sujet de débat concernant sa place. Dans certains travaux (Combacau et al., 2000;
Boufaied, 2003), cette fonction est considérée comme un élément distinct de la fonction
de diagnostic et plutôt une entité de la surveillance. D’autres travaux (Chow et Wilsky,
1984; Isermann, 1984) considèrent cette fonction comme une information primordiale
et indissociable du diagnostic. Ainsi, ils définissent le diagnostic comme la détection, la
localisation et l’identification de défauts.
27
Chapitre 2. Diagnostic des défauts dans les systèmes automatisés
[Link] Diagnostic
Exemple 2.3.1
Afin de mieux clarifier les différentes notions de surveillance, détection, diag-
nostic, localisation et identification, nous considérons l’exemple d’une panne
d’huile dans une voiture. Nous pouvons constater que la dégradation des
performances de cette voiture apparaît suite à une surconsommation d’huile,
tout en restant au dessous d’un seuil de consommation. A un certain moment,
cette dégradation peut être accompagnée, quelquefois, par l’observation de
symptômes de défaillances, comme le dégagement d’une fumée blanche. La
détection correspond au dépassement d’un certain seuil de consommation,
qui provoque le déclenchement d’une alarme indiquant l’occurrence d’une
défaillance.
28
Chapitre 2. Diagnostic des défauts dans les systèmes automatisés
Les méthodes de diagnostic des défauts utilisées dans le milieu industriel sont très
variées. Leur principe général repose sur une comparaison entre les données observées au
cours du fonctionnement du système et les connaissances acquises sur son comportement
normal et ses comportements de défaillance (Combacau, 1991). Dans cette section, nous
présentons une classification des principales méthodes de diagnostic rencontrées dans la
littérature. Cette classification, représentée dans la figure 2.3, peut être réalisée selon
plusieurs critères tels que la nature de l’information disponible (quantitative ou qua-
litative), la dynamique du système (continu, discret ou hybride), la structure de prise
de décision (centralisée, décentralisée ou distribuée). Dans la suite, nous proposons une
classification non exhaustive des méthodes de diagnostic selon deux axes : les approches
sans modèles et les approches à base de modèles (Zwingelstein, 1995). Nous référons le
lecteur aux travaux suivants pour avoir plus de détails : (Willsky, 1976; Isermann, 1984;
Basseville, 1988; Combacau, 1991; Zemouri, 2003).
29
Chapitre 2. Diagnostic des défauts dans les systèmes automatisés
30
Chapitre 2. Diagnostic des défauts dans les systèmes automatisés
Les méthodes statistiques : les méthodes statistiques supposent que les signaux
fournis par les capteurs possèdent certaines propriétés statistiques, sur lesquelles des tests
de seuil sont établis (Basseville, 1988; Zemouri, 2003). En effet, l’étude de l’évolution de la
moyenne ou de la variance d’un signal peut favoriser la mise en évidence d’une anomalie.
La reconnaissance des formes : ces méthodes reposent sur l’utilisation des algo-
rithmes de classification des formes et des mesures (continues ou discrètes). Le fonction-
nement d’un système de diagnostic par reconnaissance des formes se déroule en trois
phases (Dubuisson, 1990; Ondel, 2006) :
• une phase d’analyse qui consiste à déterminer et à réduire l’espace de représentation
des données et à définir l’espace de décision permettant de spécifier l’ensemble des
classes possibles ;
• une phase de choix d’une méthode de décision permettant de définir une règle de
décision qui a pour fonction de classer les nouvelles observations dans les différentes
classes de l’ensemble d’apprentissage ;
• une phase d’exploitation qui détermine, en appliquant la règle de décision, le mode
de fonctionnement du système en fonction de chaque nouvelle observation recueillie
sur le processus.
Les systèmes experts : les systèmes experts utilisent une information heuristique
pour lier les symptômes aux défauts (Zwingelstein, 1995). Ce sont des systèmes à base de
règles qui établissent des associations empiriques entre effets et causes (Farreny, 1989).
Ces associations sont généralement fondées sur l’expérience de l’expert plutôt que sur une
connaissance de la structure et/ou du comportement du système. Leur fonctionnalité est
de trouver la cause de ce qui a été observé en parcourant les règles par un raisonnement
inductif par chaînage avant ou arrière.
31
Chapitre 2. Diagnostic des défauts dans les systèmes automatisés
32
Chapitre 2. Diagnostic des défauts dans les systèmes automatisés
système, il faut effectuer la comparaison entre les paramètres estimés et les paramètres
théoriques.
Les méthodes de diagnostic doivent tenir compte de certains critères qui varient en
fonction des besoins en termes de sûreté, des ressources humaines et matérielles dispo-
nibles, de l’aspect critique du système surveillé, . . .. Dans (Philippot, 2006), plusieurs
critères communs aux méthodes de diagnostic ont été dégagés. En effet, une méthode de
diagnostic doit :
• fournir un diagnostic fiable (pas de fausses alarmes ni d’alarmes manquantes),
• être algorithmiquement concevable,
• être réalisable en temps réel,
• avoir un temps de réponse raisonnable (faible complexité),
• permettre un diagnostic rapide des défauts,
33
Chapitre 2. Diagnostic des défauts dans les systèmes automatisés
La distribution des composants d’un système, des informations qu’il génère (com-
mandes et compte-rendus des capteurs) peuvent parfois imposer le choix de la structure
de prise de décision des méthodes de diagnostic. Ce choix peut être entre une structure
centralisée, décentralisée ou distribuée.
La structure centralisée consiste à associer un modèle global du procédé avec un seul
module de diagnostic. En conséquence, le module de diagnostic collecte les différentes
informations du système avant de prendre sa décision finale sur son état de fonction-
nement (Sampath et al., 1995). Cette structure se montre performante en terme de
diagnostic. Cependant, elle est exposée au problème de l’explosion combinatoire des mo-
dèles utilisés surtout lorsqu’il s’agit de systèmes complexes. En effet, plusieurs approches
de diagnostic, reposant sur des structures décentralisées et distribuées, ont été proposées
dans la littérature.
La structure décentralisée se base sur un modèle global du système à qui sont associés
plusieurs modules de diagnostic locaux. Chacun reçoit les informations observables qui
lui sont spécifiques et prend une décision locale en se basant sur ses observations locales.
Afin de lever le problème d’indécision et permettre aux modules de diagnostic locaux
de diagnostiquer l’ensemble de défauts, un coordinateur (Debouk et al., 2000) doit être
utilisé. Il traite les différentes décisions locales, communiquées par les modules locaux,
afin de prendre une décision finale.
Dans la structure distribuée, le système est modélisé à travers ses composants par plu-
sieurs modèles locaux. Chacun étant associé à un module de diagnostic local responsable
de son composant. Un protocole de communication permet la communication directe-
ment entre les différents modules afin de gérer les conflits décisionnels (Silveira, 2003).
Chaque module de diagnostic prend sa décision en se basant sur sa propre observation
locale et celle communiquée par les autres modules (Xue et al., 2005).
Dans notre travail, nous nous intéressons uniquement aux structures centralisés. Des
extensions aux autres structures peuvent être réalisées par la combinaison des démarches
de décentralisation de distributions.
34
Chapitre 2. Diagnostic des défauts dans les systèmes automatisés
n’impose pas des critère de réactivité de la réponse de diagnostic. En effet, aucune limi-
tation sur le temps de réponse n’est exigée.
Le diagnostic en-ligne (Grastien, 2005) consiste à calculer le diagnostic du système
pendant qu’il fonctionne, en s’appuyant sur les observations générées. Les approches de
diagnostic en-ligne présentent des exigences en terme de réactivité de la réponse. Cela
implique un temps de réponse rapide de la part du module de diagnostic. Le diagnostic
en-ligne conduit généralement à une difficulté qui concerne la complexité du calcul. En
effet, la réponse de diagnostic doit être livrée en temps-réel, le plus rapidement possible.
Si le module de diagnostic ne parvient pas à gérer le flux d’observations et inférer le
diagnostic suffisamment rapidement, alors le diagnostic en-ligne n’est plus possible. Vu
que le nombre d’observations augmente régulièrement, il est nécessaire de disposer d’un
diagnostic incrémental, où seul le diagnostic de la date ti−1 est pris en compte pour
le calcul du diagnostic de la date ti . En effet, la complexité de traitement ne doit pas
dépendre du nombre d’observations reçus avant la date ti−1 , puisque ce nombre augmente
d’une manière non bornée.
2.5 Conclusion
35
Chapitre 2. Diagnostic des défauts dans les systèmes automatisés
36
Chapitre 3
3.1 Introduction
37
Chapitre 3. Diagnostic a base de modèles des SED et des SDH
linéaires
3.2 Cadre général du diagnostic des SED
Nous présentons dans cette section le cadre général du diagnostic des SED. Nous
introduisons d’abord la classe des SED ainsi que les outils permettant sa modélisation.
Ensuite, nous présentons le contexte général du diagnostic pour cette classe de systèmes.
D’une manière informelle, un SED est un système dynamique à espace d’états discrets
dont les transitions entre les états sont effectuées suite à l’occurrence d’événements.
L’occurrence d’un événement est instantanée dans le sens où elle n’a pas de durée. Un
SED demeure dans le même état en l’absence d’événements.
La classe des SED a été largement étudiée dans la littérature (Ramadge et Wonham,
1987; Lin et Wonham, 1988; Sampath et al., 1995). Cet intérêt est justifié par l’existence
d’un grand nombre de systèmes réels évoluant d’une manière discrète.
Cassendras et Lafortune ont défini un SED dans (Cassandras et Lafortune, 1999)
comme suit :
Exemple 3.2.1
A son état initial (instant t0 ), le système est supposé être à l’état éteint.
L’occurrence de l’événement a à l’instant t1 fait évoluer le système vers l’état
orangé. De la même manière, le SED passe aux états éteint, orangé, rouge
puis vert, suites aux occurrences respectives des événements e, a, s et c. En
38
Chapitre 3. Diagnostic a base de modèles des SED et des SDH
linéaires
Etat
rouge
6 6
orangé
6 6 6 6
vert ? ?
éteint ?
-
t0 t1 t2 t3 t4 t5 t6 t7 t8 t9 Temps
6 6 6 6 6 6 6 6 6
a e a s c a s c a
Fig. 3.1 – Chronogramme d’une évolution de SED dans le temps.
effet, l’évolution d’un SED peut être décrite par un ensemble de couples :
(σ,t) où σ représente un événement (ou une action) et t représente l’instant
de l’occurrence de cet événement. Dans notre exemple, une évolution possible
du système peut être définie par la séquence suivante d’événements : (a,t1 ),
(e,t2 ), (a,t3 ), (s,t4 ), (c,t5 ),(a,t6 ), (s,t7 ). . .
Cet ensemble ordonné de couples constitue ce que l’on appelle une trace (mot ou tra-
jectoire) du système. Dans une telle description de l’évolution du système, l’information
temporelle est représentée d’une manière explicite, ainsi, cette trace est dite temporisée.
Il est possible de décrire l’évolution du système en faisant abstraction du temps, qui sera
représenté uniquement par l’ordre d’occurrence des événements. Une telle description du
SED est dite logique. Dans l’exemple précédent, la trajectoire a e a s c a s, décrit une
évolution logique du SED.
Nous présentons dans la suite quelques outils de modélisation des SED. Durant cette
présentation, nous distinguons deux catégories de modèles pour les SED : les modèles
logiques et les modèles temporisés.
39
Chapitre 3. Diagnostic a base de modèles des SED et des SDH
linéaires
modèles logiques sont utilisés pour l’étude des propriétés qualitatives des SED. Parmi
ces modèles, nous trouvons les automates à états finis et les réseaux de Petri.
[Link].1 Les automates à états finis Un automate à états finis est une machine
à états qui permet de décrire les évolutions possibles d’un système à événements dis-
crets (Cassandras et Lafortune, 1999). Ainsi, le comportement d’un SED est représenté
à travers un ensemble d’événements associé à un ensemble d’états. Formellement, un
automate à états finis est défini par un quintuplet
G = (Q, Σ, δ, q0 , Qm )
où :
• Q est un ensemble fini d’états ;
• Σ est un ensemble fini d’événements (ou de symboles) ;
• δ est une fonction de transition, δ : Q × Σ → Q ;
• q0 ∈ Q est un état initial ;
• Qm ⊆ Q est l’ensemble d’états finaux.
Un automate à états finis est dit déterministe si à partir d’un état donné, au plus,
une seule transition est possible sur l’occurrence d’un événement.
Exemple 3.2.2
Dans la figure 3.2.1, nous modélisons le comportement du SED introduit
dans l’exemple 3.2. Chaque sommet de l’automate correspond à un état du
SED. Les transitions entre ces états sont représentées par des arcs. Chaque
arc, reliant deux sommets, est étiqueté par un événement de transition entre
les états correspondants à ces sommets. L’état initial du système éteint est
marqué par une flèche.
a a vert
~ j
+ 6
éteint orangé c
Y
s j
e rouge
La théorie des automates à états finis a été conjointement développée avec la théorie
des langages. Nous présentons dans la suite quelques notions relatives à la théorie des
langages, qui seront utilisées plus loin dans ce mémoire.
Un mot défini sur un alphabet Σ est une suite finie d’éléments de Σ. L’opérateur ||s||
indique le nombre d’éléments de Σ dans le mot s.
40
Chapitre 3. Diagnostic a base de modèles des SED et des SDH
linéaires
Nous désignons par Σ∗ l’ensemble de mots de longueur quelconque que l’on peut
construire sur Σ. Un langage défini sur un alphabet Σ correspond à un sous-ensemble de
Σ∗ .
Soit s un mot défini sur un alphabet Σ. Un mot s1 est dit préfixe de s s’il existe
un mot s2 ∈ Σ∗ telle que s = s1 s2 . La préfixe-clôture L d’un langage L est le langage
constitué par tous les préfixes des mots de L. Un language L est dit préfixe-clos s’il est
égal à sa préfixe-clôture ; i.e., L = L.
Un mot est dit accepté par un automate si, partant de son état initial et recevant
successivement les symboles du mot d’entrée, l’automate évolue vers un état final. Un
langage L(G) accepté par un automate G est constitué par l’ensemble des mots acceptés
par l’automate ; i.e., L(G) = {σ ∈ Σ∗ | δ(q0 , σ) ∈ Qm }, où δ désigne la fonction de
transition sur l’occurrence d’un mot. Un automate G est dit générateur si tous ses états
sont finaux ; i.e., Q = Qm . Il est clair que le langage L(G) accepté par un générateur
G = (Q, Σ, δ, q0 ) est préfixe-clos.
[Link].2 Les Réseaux de Petri Le modèle Réseau de Petri (RdP) a été introduit
en 1964 par C. A. Petri (Petri, 1962). Il constitue un outil de modélisation de SED parti-
culièrement adapté pour spécifier le comportement des systèmes industriels. Il permet de
modéliser et de visualiser des primitives de comportement telles que la synchronisation,
le parallélisme, le partage de ressources ou le séquencement (David et Alla, 1989). Les
RdPs sont représentés autour d’un langage graphique et d’un langage mathématique. Un
RdP se présente sous la forme de places et de transitions, reliées par des arcs.
Cet outil possède de nombreuses extensions comme les RdPs colorés (David et Alla,
1989), ou les RdP temporels (Merlin, 1974; Berthomieu et Diaz, 1991). Cette richesse
d’extensions fait que les RdPs peuvent s’appliquer à la plupart des phases de développe-
ment d’un système, de la spécification de la commande à la supervision en passant par
le diagnostic et la validation (Philippot, 2006).
41
Chapitre 3. Diagnostic a base de modèles des SED et des SDH
linéaires
[Link].1 Les automates temporisés Les automates temporisés ont été introduits
par R. Alur et D. Dill dans les années 1990 (Alur et Dill, 1994). Il s’agit d’automates
classiques munis d’un ensemble de variables réelles, appelées horloges, qui évoluent de ma-
nière continue et synchrone avec le temps. A chaque transition est associée une condition
sur la valeur des horloges, dite garde, décrivant quand une transition peut être exécutée,
et un ensemble d’horloges remises à zéro lors du franchissement de la transition. Chaque
état discret contient un invariant (une contrainte sur les horloges) qui restreint le temps
d’attente dans l’état et donc force l’exécution d’une transition. Dans ce qui suit, nous
présentons l’exemple d’un automate temporisé.
L’automate temporisé présenté dans la figure 3.3 décrit le comportement temporel
du SED considéré dans l’exemple 3.2.1. Ce modèle augmente le modèle automate à
états finis dans la figure 3.2, par une horloge, notée x, permettant de mesurer le temps
écoulé dans chaque état discret du système. Cette horloge est mise à zéro après chaque
transition entre deux sommets. La contrainte d’invariance restreint le temps de séjour
possible dans chaque état discret du système. En effet, la contrainte x ≤ 20 implique
que le système ne peut pas séjourner dans l’état discret vert plus que 20 unité de temps
(u.t.). Lorsque l’horloge x atteint 20 u.t., une transition vers l’état orangé sera franchie,
sur l’occurrence de l’événement a. La garde de cette transition (x = 20) est évidement
satisfaite par la valeur de x.
L’état d’un automate temporisé est l’association d’un sommet de l’automate (état
discret) avec l’ensemble de valeurs réelles des horloges à un instant donné (état continu).
La transition du sommet vert vers le sommet orangé peut être franchie uniquement à
partir de l’état (vert, hx = 20i).
x ≤ 20
a, x = 20, x := 0 vert
x≤3 a, x = 3, x := 0 x ≤ 3
~ z 9
6
éteint orangé c, x = 30, x := 0
Y
e, x = 3, x := 0 s, x = 3, x := 0 z rouge
x ≤ 30
42
Chapitre 3. Diagnostic a base de modèles des SED et des SDH
linéaires
[Link].2 Les réseaux de Petri temporels Le modèle réseau de Petri tempo-
rel (Merlin, 1974) est une extension du modèle réseau de Petri qui associe deux dates
min et max à chaque transition. En effet, si une transition t a été sensibilisée pour la
dernière fois à une date θ, alors t ne peut pas être franchie avant la date θ + min ou après
la date θ + max, sauf si une autre transition a désensibilisé t avant que celle-ci ne soit
franchie. Les RdPs temporels expriment des spécifications "en délais" qui sont largement
utilisées dans la description de l’évolution temporelle des processus industriels. Plusieurs
travaux se sont intéressés à la traduction du modèle RdP temporel vers le modèle au-
tomate temporisé (Sava et Alla, 2001; Cassez et Roux, 2006) afin d’exploiter la grande
capacité d’analyse que représente le modèle automate temporisé.
43
Chapitre 3. Diagnostic a base de modèles des SED et des SDH
linéaires
3.2.4 Notion d’observabilité
La notion d’observabilité dans le cadre des SED a été introduite dans les travaux de
Lin et Wonham (Lin et Wonham, 1988). En effet, les événements qui décrivent l’évolu-
tion d’un SED ont été classés en événements observables et événements non obser-
vervables.
L’ensemble des événements observables, noté Σo , correspond aux événements issus
des capteurs physiques et des actionneurs d’un procédé. Ces événements peuvent être
observés par l’environnement du système, notamment par le module de surveillance.
L’ensemble des événements non observables, noté Σuo , correspond aux événements
internes du système (des informations échangées entre les composants élémentaires de
la PO) et aux événements de défauts dont les occurrences ne peuvent pas être directe-
ment observées. Aucune information directe sur l’occurrence d’un événement observable
ne peut remonter à la PC, ou à l’environnement du système (Sampath et al., 1995).
Néanmoins, il est possible d’inférer, indirectement, l’occurrence de ces événements en
s’appuyant sur le comportement observable qui suit l’occurrence de tels événements.
Dans le cadre de notre étude, nous traitons les défauts correspondant à des évé-
nements non observables. Ainsi, nous écartons la surveillance des défauts qui peuvent
être directement observés par des capteurs de défaut. En effet, nous considérons que le
problème de surveillance devient dans ce cas trivial, puisqu’il suffit de transmettre le
signal fourni par le capteur de défaut au module de surveillance pour qu’il déclenche une
alarme. Cependant, il faut noter que le déploiement de tels capteurs n’est pas toujours
possible. En effet, certains défauts n’admettent pas de capteurs physiques permettant de
détecter leurs occurrences. Cela peut être dû à des limitations de nature technologique ou
conceptuelle. En plus, ces capteurs ont souvent un coût très élevé et impliquent parfois
des efforts supplémentaires en terme de maintenance.
La notion de diagnostic des SED a été introduite au milieu des années 1990 dans les
travaux de sampath (Sampath et al., 1995, 1996). Plusieurs extensions de ces travaux
ont été proposées dans le cadre des modèles SED temporisés (Tripakis, 2002; Zad et al.,
2005; Lunze, 2006), des modèles hybrides (Fourlas et al., 2002; Bhowal et al., 2007),
des architectures décentralisées (Debouk et al., 2000) et distribuées (Silveira, 2003; Xue
et al., 2005), des modèles stochastiques (Thorsley et Teneketzis, 2005), . . ..
Dans la suite, nous présentons les méthodes de diagnostic de SED les plus pertinentes
pour la compréhension de notre travail. Nous considérons une classification des méthodes
de diagnostic de SED basée sur la nature du modèle. En effet, nous pouvons distinguer
44
Chapitre 3. Diagnostic a base de modèles des SED et des SDH
linéaires
deux catégories de méthodes :
• les méthodes basées sur des modèles logiques ;
• les méthodes basées sur des modèles temporisés.
Les méthodes à base de modèles logiques consistent à élaborer le diagnostic du sys-
tème à partir d’un modèle logique du SED. Ainsi, le temps sera considéré uniquement
d’une manière qualitative à travers l’ordre d’occurrence des événements. Le diagnostic
résultant considérera le temps, de même, d’un point de vue qualitatif.
Les méthodes à base de modèles temporisés consistent à élaborer le diagnostic du
système à partir d’un modèle temporisé du SED. Ainsi, l’aspect temporel sera considéré
d’une manière explicite et quantitative, à travers l’utilisation d’horloges internes (Alur
et Dill, 1994) ou la discrétisation du temps (Zad et al., 2005).
Nous présentons dans la suite les approches de diagnostic des SED reposant sur un
modèle logique du système à diagnostiquer. Dans ce cadre, nous pouvons distinguer deux
principales approches. La première approche, issue des travaux de Sampath (Sampath
et al., 1995), se base sur une représentation événementielle des défauts. La seconde ap-
proche a été introduite par Zad (Zad et al., 2003) et repose sur modélisation à base
d’état des défauts. Nous présentons dans la suite un aperçu de ces deux approches, tout
en insistant sur l’approche de référence développée dans les travaux de Sampath.
Dans la littérature, les travaux de Sampath et al. (Sampath et al., 1995, 1996)
sont devenus une référence dans le domaine du diagnostic à base de modèles des SED.
Dans (Sampath et al., 1995), une approche de modélisation et de diagnostic des systèmes
complexes, basée sur une représentation logique des SED, a été proposée. Cette approche
consiste à inférer les occurrences des événements des défauts non observables en utilisant
les événements observables générés par le système.
Dans la figure 3.4, nous illustrons le principe de cette approche.
1. Dans une première étape, un modèle "complet", qui décrit le comportement nor-
mal et anormal du système, est construit. Ce modèle correspond à un automate à
états finis, construit à partir d’une composition des modèles élémentaires des com-
posants. Les défauts sont représentés par des événements non observables. A partir
de ce modèle global, un outil de diagnostic, appelé diagnostiqueur, est compilé
hors-ligne, sous la forme d’un automate à états finis déterministes.
45
Chapitre 3. Diagnostic a base de modèles des SED et des SDH
linéaires
Module de surveillence
MODELE COMPLET
DU SYSTEME
compilation du
diagnostiqueur HORS-LIGNE
EN-LIGNE
DIAGNOSTIQUEUR
-
annoncer la détection
de défaillances
6 6
événements observables
Système
- PO
compte-rendus
commandes
PC
46
Chapitre 3. Diagnostic a base de modèles des SED et des SDH
linéaires
ensemble de paires de la forme (état,étiquettes). Chaque paire contient un état estimé du
système, associé à un ensemble d’étiquettes éléments de {F1 , . . . , Fm , N }. L’étiquette N
indique que le système admet un fonctionnement normal s’il se trouve dans l’état estimé,
associé à cette étiquette. Si un état estimé est associé à une étiquette Fi alors un défaut
de l’ensemble Σfi s’est produit, avant d’atteindre cet état. Si l’étiquette Fi est associée
à tous les éléments d’un état du diagnostiqueur, alors cet état du diagnostiqueur est dit
Fi -certain. Un état du diagnostiqueur est dit normal, si les étiquettes appartenant à cet
état ne comportent que l’étiquette N et dit Fi -incertain s’il ne coïncide à aucun des deux
cas précédents.
Lorsque le diagnostiqueur évolue vers un état Fi -certain, suite à l’observation d’une
séquence d’événements, il annonce par le biais d’une fonction de décision, l’occurrence
d’un défaut de l’ensemble Σfi . Intuitivement, toute trajectoire du système, dont la pro-
jection observable est identique à la séquence d’événements observables générée par le
système, contient au moins un défaut de l’ensemble Σfi . Autrement dit, toutes les tra-
jectoires estimées du système, qui expliquent le comportement observé, contiennent un
défaut de Σfi . Si le diagnostiqueur évolue vers un état Fi -incertain, aucune décision
certaine sur l’occurrence d’un défaut ne pourra être prise. Ceci peut être expliqué par
l’existence d’au moins deux trajectoires qui expliquent le comportement observé, l’une
contient un défaut de l’ensemble Σfi et l’autre non.
Afin de décrire le fonctionnement du diagnostiqueur, nous considérons l’exemple sui-
vant.
Exemple 3.3.1
La figure 3.5 illustre l’exemple d’un modèle et son correspondant diagnos-
tiqueur. Dans le modèle considéré, les transitions sur les événements non
observables sont représentées par des arcs en pointillés. On suppose que
Σo = {a, b, c, d, e} et Σuo = Σf = {f1 , f2 }. On définit la partition de défauts
de la manière suivante : Πf = {Σf1 , Σf2 }, avec Σf1 = {f1 } et Σf2 = {f2 }.
L’état 1N correspond à l’état initial du diagnostiqueur. Ainsi, on suppose
que le système ne contient pas de défaut à son état initial. A partir de cet
état et suite à l’observation de l’événement a, le diagnostiqueur évolue vers
l’état F1 -incertain {3F1 7N }. Cet état indique que le modèle du système est
soit dans l’état 7 et aucun défaut ne s’est produit, soit dans l’état 3 avec
l’occurrence d’un défaut de l’ensemble Σf1 . Ensuite, le diagnostiqueur évolue
vers l’état {4F1 9F2 12N } suite à l’observation de l’événement b.
47
Chapitre 3. Diagnostic a base de modèles des SED et des SDH
linéaires
R
d 1N
a
c
3m b - 4m - 5m
+
?
a 3 3F1 7N }
f1 3 2m b
e ? d
~ m 4F1 9F2 12N
1 b c e R
8m - 9m - 10m - 11m c
a ~ 6f2 ?
5F1 10F2 13N
m b - m c- m
7 12 13
k e e
? W
d 11F2
Fig. 3.5 – Exemple d’un modèle automate à états finis G et son diagnostiqueur Gd
48
Chapitre 3. Diagnostic a base de modèles des SED et des SDH
linéaires
[Link] Approche issue de la contribution de Zad
Chaque état du modèle du système ainsi que de son diagnostiqueur est étiqueté par
la sortie observée. L’état initial du diagnostiqueur correspond au sommet (X, {N, F })
qui signifie que l’état courant du système est inconnu et qu’il peut être normal ou associé
à une défaillance. Supposons que la sortie d est observée, le diagnostiqueur évolue vers
le sommet ({5, 9}, {N, F }) qui correspond à un état incertain (normal ou défaillant). Si
49
Chapitre 3. Diagnostic a base de modèles des SED et des SDH
linéaires
par la suite, la sortie e est observée, le diagnostiqueur évolue vers le sommet ({6}, {F }),
un défaut est alors détecté.
Ces approches reposent sur des modèles représentant, d’une manière explicite, les
relations temporelles liant les occurrences des événements dans un SED. De nombreuses
méthodes se sont intéressées au diagnostic basé sur des modèles temporisés de SED. Ces
méthodes visent à exploiter au maximum les contraintes temporelles qui existent entre
les événements du SED, afin de permettre la discrimination des défauts.
La notion de signature temporelle est une notion intéressante pour la caractérisation
temporelle des trajectoires discrètes de comportement normal et de défaut au sein d’une
description événementielle (Philippot, 2006). En effet, il est possible que l’occurrence
d’un défaut n’affecte pas l’ordre des événements observables qui suivent le défaut, par
contre, elle affecte les dates d’occurrence de ces événements. Ainsi, l’exploitation du
temps devient nécessaire dans ce cas pour caractériser les trajectoires des comportements
défaillants.
L’intégration des contraintes temporelles dans le diagnostic des SED a été abordée
par plusieurs chercheurs utilisant des formalismes mathématiques différents, tels que les
automates temporisés (Alur et Dill, 1994), les RdP temporels (Merlin, 1974), les chro-
niques (Dousson, 1994), . . .. Nous proposons dans la suite, quelques méthodes de diag-
nostic de SED à base de modèles temporisés. Nous dégageons dans ce cadre deux types
de méthodes qui se distinguent par l’élaboration ou non d’un pré-calcul de diagnostic :
les méthodes en-ligne ou les méthodes hors-ligne.
Les approches hors-ligne sont caractérisées par l’élaboration d’un pré-calcul hors-
ligne, afin de minimiser le calcul à effectuer pendant la phase en-ligne (à ne pas confondre
avec le diagnostic hors-ligne qui est élaboré sur la base d’observations connues à l’avance).
L’approche de Sampath fait partie de cette sous-classe d’approches. En effet, le calcul
effectué hors-ligne consiste à estimer, pour chaque observation pouvant être générée par
le système, l’ensemble des états du système et des défauts produits. L’ensemble de ces
estimations est compilé sous la forme d’un automate à états finis, qui correspond au
diagnostiqueur. Ainsi, une fois exécuté, le diagnostiqueur évolue d’une manière détermi-
niste sur l’occurrence de chaque événement observable généré par le système, et fournit
l’ensemble des défauts pouvant affecter son fonctionnement. En effet, le calcul effectué
pendant la phase en-ligne se réduit au franchissement déterministe d’une transition as-
sociée à l’événement observé.
50
Chapitre 3. Diagnostic a base de modèles des SED et des SDH
linéaires
Nous présentons dans la suite quelques approches de diagnostic hors-ligne, basées sur
des modèles temporisés de SED.
[Link].2 Approches à base de RdP temporel Dans (Ghazel et al., 2005), les au-
teurs ont proposé la construction d’un diagnostiqueur à partir d’un modèle RdP temporel
du système. Cette approche exploite les contraintes temporelles sur les événements dans
le but d’affiner les résultats de l’estimation. La construction du diagnostiqueur repose sur
une approche d’analyse des états accessibles dans le RdP temporel du système. Le diag-
nostiqueur conséquent est un graphe d’états similaire au graphe des classes d’états, où
chaque transition entre deux nœuds du graphe est étiquetée par un événement observable
et un intervalle de franchissement. Une transition ne peut être franchie que si la date
d’occurrence de l’événement observé satisfait l’intervalle de franchissement. Ainsi, suite
à l’observation de chaque événement, une transition est franchie d’une manière détermi-
niste vers un autre nœud du graphe, qui détermine la classe d’états accessibles à cette
date, en tenant compte de l’occurrence de toute séquence d’événements non observables.
Dans le cadre des approches en-ligne, aucun calcul pré établi n’est effectué. En effet,
le diagnostiqueur élabore en-ligne le calcul nécessaire pour l’identification des défauts, à
partir de l’ensemble d’événements observables générés par le système. Nous présentons
dans la suite quelques travaux portant sur le diagnostic en-ligne qui sont basés sur des
modèles SED temporisés.
51
Chapitre 3. Diagnostic a base de modèles des SED et des SDH
linéaires
[Link].1 Estimateur d’état de Tripakis Dans (Tripakis, 2002), Tripakis propose
une extension temporisée de l’approche de diagnostic de Sampath reposant sur l’utilisa-
tion d’un estimateur d’état en-ligne (à ne pas confondre avec l’estimateur d’état défini
par les automaticiens). La démarche de diagnostic présentée dans ce travail commence
par l’élaboration d’un modèle automate temporisé du système à diagnostiquer. Par la
suite, une partition des sommets de l’automate en sommets de fonctionnement normal
et sommets de fonctionnement de défaut est établie. Le diagnostiqueur est donné sous
la forme d’un algorithme d’estimation d’état en-ligne. Cet algorithme estime l’état cou-
rant du système suite à chaque occurrence d’un événement observable et déclenche une
alarme quand un défaut est détecté.
Le fonctionnement du diagnostiqueur est décrit dans Algorithme 1.
52
Chapitre 3. Diagnostic a base de modèles des SED et des SDH
linéaires
• enfin, l’occurrence de l’événement σ, si cet événement a été observé.
La fonction de diagnostic fd évalue l’estimation de l’état courant du système et dé-
clenche une alarme si elle détecte un défaut ; i.e, lorsque tous les états estimés dans W
correspondent à des sommets de fonctionnement de défaut.
Un exemple d’application de l’algorithme du diagnostiqueur est illustré dans la fi-
gure 3.7. Nous supposons, dans cet exemple, une évolution du système décrite par la
séquence d’événements temporisés : (a, 9)(f, 3.5)(b, 1)(c, 4), où a, b et c représentent
les seuls événements observables et f désigne l’événement de défaut. Après l’observa-
tion de la projection observable de cette séquence d’événements, à savoir, la séquence
(a, 9)(b, 4.5)(c, 4), l’algorithme du diagnostiqueur évolue comme décrit dans la figure 3.7.
x≤5 x≤8 x≥0
u 3m - 4m - 5m
x≥0 x≤4 3 b, x ≤ 5 c, x ≤ 6
R 1m - 2m
a, x := 0 x≤8 x ≤ 10 x≥0
f s m
6 - 7m - 8m
b, x ≥ 4 c, x ≥ 8
? ? ? ?
pas de pas de pas de annoncer
défauts défauts défauts un défaut
53
Chapitre 3. Diagnostic a base de modèles des SED et des SDH
linéaires
simplicité et permet d’éviter le problème d’explosion combinatoire lié à la compilation
hors-ligne du diagnostiqueur, cependant, il présente plusieurs inconvenants.
D’abord, la complexité d’exécution de cet algorithme est doublement exponentielle
en fonction de la taille du modèle considéré et la taille de la séquence d’événements
observée (Bouyer et Chevalier, 2005). Cette grande complexité du calcul en-ligne im-
plique un phénomène de retard considérable, qui augmente au fur et à mesure du nombre
d’événements observé (puisque la taille des observations intervient dans la formule de
complexité). Ce retard n’est pas toléré lors du diagnostic des systèmes critiques, qui
nécessitent une identification rapide des défauts, et peut avoir dans certains cas des
conséquences néfastes. Nous remarquons que cette approche s’intéresse seulement à la
détection et non à l’identification des défauts puisqu’elle considère l’existence d’un
seul type de défaut. Enfin, cette approche est incapable de détecter au plus-tôt les
défauts, quand le système se bloque et ne génère plus d’événements. En effet, il faut at-
tendre l’écoulement d’une durée constante T O u.t. pour déclencher une alarme, même
s’il est possible de s’assurer, plus-tôt, de l’occurrence du défaut.
54
Chapitre 3. Diagnostic a base de modèles des SED et des SDH
linéaires
chaque mode de défaillance, que l’on désire identifier, une chronique (ou un scénario). En-
suite, elle utilise une technique de reconnaissance en-ligne de ces chroniques afin d’iden-
tifier les scénarios de défaillances. En effet, si des événements observés correspondent
aux motifs de la chronique et si leur occurrence a lieu selon le contexte et les contraintes
spécifiées, alors une instance de la chronique modélisée devra être reconnue.
Comme il est illustré dans la figure 3.8, introduite dans (Dousson, 1994), les modèles
de chroniques sont spécifiés hors-ligne alors que la phase de reconnaissance est établie en-
ligne. Cette dernière phase repose sur le maintien à jour de fenêtres temporelles précisant
les dates où un événement est attendu par la chronique compte-tenu de l’ensemble de
ses contraintes. Les chroniques peuvent être modélisées par un RdP temporel ou par un
graphe de contrainte (treillis) (Mokhtari, 2007).
La plupart des SAP réels évoluent selon des sous processus continus qui sont démar-
rés, arrêtés par des commandes à états discrets (dont les entrées dépendent des sous
processus continus). Par conséquent, les procédés ont rarement un comportement pure-
ment discret ou purement continus mais plutôt un mélange entre les deux. Ces systèmes
dynamiques à double composante comportementale (dynamique continue et événemen-
tielle) sont nommés : Systèmes Dynamiques Hybrides (SDH). Ces systèmes peuvent être
de natures très diverses. On peut rencontrer des systèmes continus auxquels sont associés
des commutations discrètes ou bien des systèmes à événements discrets auxquels sont
associés certaines évolutions continues. Plusieurs outils de modélisation des systèmes hy-
brides ont été proposés dans la littérature. Parmi ces outils, nous citons les automates
hybrides (Alur et al., 1993), les automates hybrides rectangulaires (Henzinger et al.,
55
Chapitre 3. Diagnostic a base de modèles des SED et des SDH
linéaires
1998), les automates hybrides linéaires (Müller et Stauner, 2000), les RdP hybrides (Alla
et David, 1998; David et Alla, 2004), les statecharts hybrides (Harel et Pnueli, 1987), les
bond graphs hybrides (Mosterman, 1997). . .. Dans la suite, nous insistons sur les outils
dans lesquels nous avons trouvé des réponses aux objectifs que nous nous sommes fixés.
D’une manière générale, un SHD est modélisé par un ensemble de systèmes à dyna-
mique continue interagissant avec un ou plusieurs systèmes à événements discrets (Ku-
rovszky, 2002). Le point commun entre ces formalismes est que l’évolution continue est
affectée par les événements discrets et les modèles nécessitent à la fois des variables d’état
continues et discrètes.
Nous pouvons classer les approches de modélisation des SDH selon trois classes(Chen
et Provan, 1997) :
• l’approche continue : cette approche consiste à définir une approximation des
dynamiques discrètes du système hybride par des équations différentielles pour
modéliser l’occurrence des événements discrets ;
• l’approche événementielle : avoir une approche purement discrète pour modéli-
ser les SDH consiste à supprimer les dynamiques continues ou à faire une approxi-
mation de l’évolution continue de façon à ce que le système hybride soit représenté
uniquement par les événements qui le caractérisent ;
• l’approche mixte : dans une approche mixte, chacune des deux composantes
(discrète et continue) est représentée de façon rigoureuse et explicite et leur colla-
boration est prise en compte dans l’interface qui les relie. La résolution du modèle
continu déclenche l’évolution des variables au cours du temps et valide certaines
transitions. L’évolution du modèle discret engendre alors la mise en place d’un nou-
vel état discret qui se traduit par l’élaboration d’un nouveau système d’équations.
Nous présentons dans la suite quelques modèles mixtes rencontrés dans la littérature.
Les automates hybrides (Alur et al., 1993) sont une extension des automates à états
finis. Ils représentent des systèmes qui intègrent deux composantes : celle ayant un com-
portement discret, modélisée naturellement par un automate à états finis et celle dont
le comportement varie de manière continue dans le temps, modélisée par un système
algébrodifférentiel. Un automate hybride évolue par une alternance de pas continus, où
les variables d’état et le temps évoluent de façon continue, et de pas discrets où plusieurs
transitions discrètes et instantanées peuvent être franchies. Notons qu’un automate tem-
56
Chapitre 3. Diagnostic a base de modèles des SED et des SDH
linéaires
porisé correspond à automate hybride particulier où toutes les variables admettent des
dérivées par rapport au temps égales à 1.
D’un point de vue informel et général, un automate hybride apparaît ainsi comme
un automate à états fini pilotant un ensemble d’équations différentielles modélisant la
dynamique continue du système. L’état de l’automate change instantanément lors de
l’occurrence d’un événement discret ou par l’écoulement du temps lors de la validation
d’une condition logique spécifiée sur la valeur de la variable continue (Henzinger, 1996).
allumer, x ∈ [2, 4], x := 0
x ∈ [5, 10] ∧ y = 0
R
)
Éteint Allumé
x≤4 x ≤ 10
ẋ = 1 ẋ = 1
ẏ = −4y ẏ = 3y + 2
1
57
Chapitre 3. Diagnostic a base de modèles des SED et des SDH
linéaires
L’analyse d’accessibilité consiste à déterminer l’espace d’état accessible par l’évolution
du système hybride étudié. Ce problème n’est pas décidable pour un automate hybride
sans hypothèses particulières (Henzinger et al., 1998). Il faut alors apporter des restric-
tions pour avoir des sous-classes pour lesquelles certaines propriétés sont décidables. Dans
la suite, nous nous intéressons à l’étude d’une de ces sous-classes d’automates hybrides
pour laquelle l’analyse d’accessibilité est décidable.
Plusieurs sous-classes du modèle automate hybride ont été explorées dans la littéra-
ture. Ces sous-classes ont été étudiées dans le but d’alléger la structure du modèle initial,
afin de simplifier son analyse et sa vérification. Parmi les modèles proposés, nous citons :
• les automates hybrides linéaires (Alur et al., 1993) : un automate hybride est dit
linéaire si les conditions de flux, des invariants, des gardes, sont définies par des
expressions linéaires sur l’ensemble des variables.
• les automates hybrides rectangulaires (Kopke, 1996; Henzinger et al., 1998) : c’est
une sous-classe des automates hybrides linéaires. La condition de flux dans ce
modèle est définie sous la forme de prédicats rectangulaires de la forme ẋ ∈ [a, b],
pour chaque variable x du modèle. De même, Les invariants, les gardes, la condition
initiale sont décrits par des prédicats rectangulaires.
• les automates hybrides rectangulaires initialisés (Henzinger et al., 1998) : c’est une
sous-classe des automates hybrides rectangulaires. Dans ce modèle, chaque variable
qui change de condition de flux, suite au franchissement d’une transition entre deux
sommets, doit être réinitialisée. Dans la figure 3.10, nous illustrons l’exemple d’un
automate hybride rectangulaire initialisé.
α, x ∈ [5, 10], y := 10
x = 0 ∧ y ∈ [0, 5]
R
A B
x≤4 x ≤ 20 ∧ y ≤ 60
ẋ = 1 ẋ = 1
ẏ = 0 ẏ = 3
1
La sous-classe des automates hybrides rectangulaires est une sous-classe très inté-
ressante d’automates hybrides. Elle a été largement étudiée dans la littérature (Spatho-
poulos, 2000; Henzinger et Majumdar, 2000). L’importance de cette sous-classe est due
au fait que plusieurs problèmes intéressants, tels que l’analyse d’accessbilité (Henzinger
58
Chapitre 3. Diagnostic a base de modèles des SED et des SDH
linéaires
et al., 1998), la synthèse de contrôleurs (Spathopoulos, 2000), le model-checking (Hen-
zinger et Majumdar, 2000) sont décidables pour les automates hybrides rectangulaires
initialisés. Ce modèle représente le modèle de base de notre travail de recherche. Une des-
cription plus détaillée et formelle de la sous-classe des automates hybrides rectangulaires
sera donnée dans les chapitres suivants.
Les réseaux de Petri (Petri, 1962) ont été très utilisés comme outils de modélisation,
analyse et synthèse pour les systèmes à événements discrets. Dans (Alla et David, 1998),
les auteurs présentent une extension des réseaux de Petri (RdP), les réseaux de Petri
hybrides. Le modèle RdP hybride hérite tous les avantages du modèle de réseaux de Petri
tel que la représentation du parallélisme, de la synchronization et des conflits (David et
Alla, 2004).
Un RdP hybride permet d’obtenir des modèles concis de systèmes réels. Il est ensuite
possible de construire de manière algorithmique l’automate hybride correspondant (Al-
lam et Alla, 1996) et d’appliquer tous les outils formels qui y sont développés.
59
Chapitre 3. Diagnostic a base de modèles des SED et des SDH
linéaires
2003; Domlan et al., 2004). L’exploitation de l’aspect discret des SDH est généralement
faible dans ces approches. Nous présentons dans la suite, d’une manière non exhaustive,
quelques approches rencontrées dans la littérature, dans ce cadre.
Plusieurs approches de diagnostic basées sur la génération de résidus ont été proposées
dans la littérature. Nous pouvons citer à titre d’exemple l’approche de (Koutsoukos et al.,
2001) . Dans cette approche, l’estimation en ligne du mode de fonctionnement des SDH
est réalisée grâce à l’emploi de RdP. L’occurrence d’un défaut est détectée en comparant
les grandeurs mesurées à celles attendues en tenant compte des commandes envoyées
au processus. Le diagnostic de l’état du processus est ensuite réalisé à l’aide d’un arbre
logique. Cette approche, adaptée aux SDH, présente l’avantage de détecter les anomalies
dues aux variables continues et à l’occurrence d’événements perturbateurs.
Une autre technique de diagnostic de SDH a été proposée (Cocquempot et al., 2004).
Cette technique repose sur les méthodes de diagnostic à base de redondance analytique.
Le système à diagnostiquer est modélisé par un automate hybride. La détection de dé-
fauts est réalisée grâce à la génération de résidus entre les variables d’entrée et de sortie
mesurées et les relations de redondance analytique déterminées à partir des entrées et
des sorties ainsi que de leurs dérivées, indépendamment du mode discret du système. Le
diagnostic des défaillances est réalisé à partir de résidus structurés spécifiques à chaque
défaut. Dans (Balluchi et al., 2002), une solution basée sur l’utilisation d’un observa-
teur hybride constitué d’un observateur continu et un observateur discret est proposée.
L’observateur discret permet d’identifier l’état discret courant du système tandis que
l’observateur continu estime l’évolution des variables continues.
Gomaa propose, dans (Gomaa et Gentil, 1996; Gomaa, 1997), une approche de diag-
nostic des SDH fondée sur une extension des RdP hybrides, dénommé les réseaux de Petri
continus causaux hybrides(RdP C 2 H). Ce modèle intègre trois type de RdPs : un RdP
continu temporisé qu’on a appelé Réseau de Petri Continu Causal hybride(RdP C 2 H) ;
c’est un modèle approximatif modélisant de façon causale la partie continue du SDH ; un
RdP classique modélisant le système de contrôle (SED) ; et un RdP classique modélisant
l’interaction entre la partie continue et le système de contrôle. Les liens causaux (tran-
sitions) entre les variables continues sont représentés à travers des fonctions de transfert
qualitatives basées sur les informations de gain, retard,. . .. L’auteur propose la concep-
tion d’un système de diagnostic de défauts basée sur un modèle RdP C 2 H. Le système de
détection de défauts, influençant les variables continues, est réalisé de façon asynchrone ;
60
Chapitre 3. Diagnostic a base de modèles des SED et des SDH
linéaires
la localisation de défauts est effectuée par le chaînage arrière/avant des liens causaux
entre les variables en utilisant leurs informations temporelles.
Une autre approche reposant sur un raisonnement causal a été proposé dans (Karsai
et al., 2003). Cette approche repose d’abord sur la modélisation du système par un modèle
bond graph hybride (Mosterman, 1997) puis la génération d’un graphe de propagation
des défauts, qui permet de décrire les relations causales et temporelles entre les différents
modes de défauts d’un coté, et les observations associées d’un autre.
Il existe peu de contributions de diagnostic pour les SDH, issues de méthodes SED.
En effet, l’élaboration de telles méthodes se trouve en confrontation avec les dynamiques
complexes et les indécidabilités liées aux SDH. Nous pouvons dégager deux grandes ap-
proches dans ce cadre, chacune détermine à sa manière, l’acquisition du modèle hybride.
La première approche est fondée sur l’abstraction des trajectoires continues et sa
représentation à travers des modèles discrets dynamiques. En effet, elle consiste à établir
des partitions qualitatives des grandeurs continues et de les représenter sous la forme
d’états ou d’étiquettes de transition d’état. Cette approche représente une solution al-
ternative aux approches fondées sur une représentation analytique précise. Parmi les
approches développées dans ce cadre, nous citons les travaux de Bhowal (Bhowal et al.,
2007) qui se base sur un modèle automate hybride à temps discret.
Une autre approche repose sur une acquisition expérimentale du modèle du système
à travers l’abstraction des équations de l’espace d’état et les méthodes d’identification à
base de réalisations expérimentales. Parmi les approches développées dans le cadre, nous
citons les travaux de Lunze (Lunze, 2000, 2006).
Lunze propose dans (Lunze, 2000, 2006), des algorithmes de diagnostic similaires au
concept du diagnostiqueur de Sampath. Ainsi, l’inférence et l’évaluation des hypothèses
sur les défauts sont effectuées à travers un algorithme de diagnostic, comme il est indiqué
dans la figure 3.11. Le problème de diagnostic est associé à un problème d’observation
d’état qualitatif. En effet, une abstraction qualitative des variables continues du système
est effectuée à travers l’utilisation de quantificateurs. L’identification de défaut consiste
alors à trouver le modèle fi dont la trajectoire prédite est cohérente avec celle observée. La
localisation est une conséquence de l’identification qui associe à chaque fi un composant
ou sous-système. Si la discrimination entre les défauts est faible alors une réévaluation
de l’abstraction qualitative faite ou bien une réévaluation du schéma d’instrumentation.
61
Chapitre 3. Diagnostic a base de modèles des SED et des SDH
linéaires
62
Chapitre 3. Diagnostic a base de modèles des SED et des SDH
linéaires
3.6 Etude de la diagnosticabilité
Comme nous avons vu dans l’étude précédente, l’application d’une méthode de diag-
nostic est soumise à la condition de vérification du critère de diagnosticabilité. Ce critère
stipule que le modèle du système dispose de suffisamment d’informations pour effectuer
le diagnostic. En d’autres termes, il permet de répondre à l’interrogation suivante : est-il
possible de déterminer toutes les occurrences des défauts affectant un système, étant
données les informations fournies par son modèle et les observations qu’il génère ?
La définition de la diagnosticabilité pour les SED a été initialement formalisée dans
les travaux de Lin et Wonham (Lin et Wonham, 1994). Plusieurs extensions de cette
définition ont été ensuite proposées, dans de différents contextes (Sampath et al., 1995;
Jiang et al., 2000; Tripakis, 2002; Fourlas et al., 2002; Thorsley et Teneketzis, 2005). Les
extensions proposées varient en fonction de l’abstraction du modèle utilisé (logique, tem-
porisé, hybride), de la structure de la méthode de diagnostic (centralisée,décentralisée,
distribuée), . . ..
Dans la suite, nous présentons la notion de diagnosticabilité dans le cadre des SED
logiques et temporisés. Nous nous intéressons aux travaux les plus importants pour la
compréhension de notre travail. Ensuite, nous survolons les techniques utilisées pour la
vérification de cette notion.
Pour une partition de défauts donnée, un SED est dit diagnosticable s’il est possible
de détecter, au bout d’un délai fini, l’occurrence de n’importe quel défaut non obser-
vable, appartenant à un ensemble de la partition, à travers les événements observés (Lin
et Wonham, 1994; Sampath et al., 1995). En effet, le critère de diagnosticabilité implique
que chaque événement de défaut conduit à des observations suffisamment discriminantes
pour permettre l’identification unique du mode de défaut au bout d’un délai fini. L’en-
semble des observations doit être suffisamment riche pour cette discrimination. Cela peut
être représenté formellement de la manière suivante :
Définition 7. Soient L un langage vivant préfixe-clos et Πf une partition de défauts,
Πf ={Σf1 , . . . , Σfm }. L est dit diagnosticable par rapport à une partition de défauts Πf ,
si :
63
Chapitre 3. Diagnostic a base de modèles des SED et des SDH
linéaires
ω ∈ PL−1 (P (st)) ⇒ Σf i ∈ ω
où :
• L/s désigne l’ensemble des suffixes de L qui commencent par s, L/s={t ∈ Σ∗ | st
∈ L}.
• PL−1 désigne la fonction de projection inverse sur L définie par PL−1 (y)={s ∈ L |
P (s) = y}.
• Ψ(Σf i ) désigne l’ensemble des séquences terminées par un défaut de l’ensemble Σfi .
Cette définition stipule qu’un langage L est diagnosticable si, pour toute séquence s
contenant un défaut appartenant à l’ensemble Σfi , le diagnostiqueur doit être capable
d’identifier ce défaut après l’occurrence d’un nombre fini d’événements ni = ||t||. En
effet, toute autre séquence ω ayant un comportement observable que la séquence st ; i.e.,
P (ω) = P (st), elle doit contenir un défaut appartenant à Σfi .
En effet, afin de pouvoir identifier un défaut de l’ensemble Σfi , toute trajectoire
observable qui suit l’occurrence du défaut, doit être distinguée, au bout d’un nombre
fini d’événements, des trajectoires observables des comportements ne contenant pas de
défauts de Σfi . Autrement dit, l’occurrence d’un défaut de l’ensemble Σfi , conduit à des
observations suffisamment discriminantes pour permettre l’identification unique du type
de défaut Σfi dans un délai fini. Cet ensemble d’observation définit alors la signature du
défaut.
Une approche systématique pour la vérification de la diagnosticabilité d’un language
L, généré par un automate à états finis G, a été proposée dans (Sampath et al., 1995).
Cette approche repose sur la construction du diagnostiqueur D, puis la vérification de
certains cycles, dit Fi -indéterminés. Un cycle Fi -indéterminé est constitué exclusivement
d’états Fi -incertain, à qui correspond deux cycles dans l’automate G, où tous les éléments
du premier cycle sont associés à l’étiquette Fi dans le cycle du diagnostiqueur, et tous
les éléments du deuxième cycle sont associés à des étiquettes différentes de Fi .
Un language L, généré par un automate G, est diagnosticable par rapport à une par-
tition de défauts Πf , si son diagnostiqueur D ne contient aucun cycle Fi -indéterminé,
pour tout i ∈ Πf . Considérons le diagnostiqueur construit dans l’exemple 3.3.1, ce diag-
nostiqueur ne vérifie pas la condition de diagnosticabilité, puisque le cycle constitué par
64
Chapitre 3. Diagnostic a base de modèles des SED et des SDH
linéaires
les états {3F1 7N }, {4F1 9F2 12N } et {5F1 10F2 13N }, est F1 -indéterminé. A ce cycle,
correspond deux cycles d’états dans l’automate G : chaque élément dans le cycle des états
{7, 12, 13}, est associé à l’étiquette F1 , et les éléments du cycle {3, 4, 5}, sont associés
à des étiquettes différentes de F1 . Si le système génère la séquence af1 bcdbcd(bcd) . . . ,
le diagnostiqueur va évoluer dans le cycle F1 -indéterminé, sans pouvoir identifier le dé-
faut. Autrement dit, la séquence observée par le diagnostiqueur abcdbcd(bcd) . . . , peut
provenir d’une évolution du système dans le cycle {3, 4, 5} avec l’occurrence d’un défaut
f1 ∈ Σf1 , soit d’une évolution du système dans le cycle {7, 12, 13}. L’auteur a proposé
plusieurs solutions permettant de rendre le système diagnosticable : la première solution
consiste à introduire des capteurs supplémentaires afin que l’ensemble des observations
soit suffisamment riche pour permettre la discrimination du comportement de défaut et
rendre ainsi le système diagnosticable. La deuxième solution, appelée diagnostic actif,
consiste à restreindre certains comportements du système afin de le rendre diagnosti-
cable. Cette méthode est basée sur la théorie de commande supervisée introduite par
Ramadge-Wonham (Ramadge et Wonham, 1987). Une autre solution consiste à redé-
finir la partition des défauts. En effet, si deux défauts, appartenant à deux différents
ensembles de défauts, ne peuvent pas être distingués selon leurs trajectoires observables,
alors on fusionne les deux ensembles de défauts en un même ensemble. Cependant, cette
solution rend la capacité de localisation du diagnostiqueur plus faible.
Cette définition stipule qu’un langage temporisé est ∆-diagnosticable, si toute paire
de traces dans L, la première contient un défaut et la seconde est dépourvue de défauts,
les projections observables de ces deux traces doivent être différentes au bout de ∆ u.t.
de l’occurrence du défaut.
65
Chapitre 3. Diagnostic a base de modèles des SED et des SDH
linéaires
L’intégration du temps dans la définition de ∆-diagnosticabilité introduit deux nou-
velles notions sur la définition classique de diagnosticabilité :
• dans l’approche classique, l’identification d’un défaut doit se faire au bout d’un
délai fini. Ce délai est représenté qualitativement à travers le nombre d’événements
qui suivent l’événement du défaut. Par contre, ce délai est défini quantitativement
dans l’extension temporisée de cette définition à travers le délai ∆.
• la discrimination des trajectoires de défauts prend en considération le temps d’une
manière explicite. En effet, la définition classique stipule qu’un language est diag-
nosticable s’il est possible de discriminer, d’un point de vue logique, les trajectoires
comportant des défauts. Cela nécessite l’observation d’un événement discrimi-
nant, au bout d’un délai fini, permettant de caractériser d’une manière unique
une trajectoire défaillante du système. Dans le contexte temporisé, la discrimi-
nation d’une trajectoire défaillante considère en plus, les dates d’occurrence des
événements observables. Ainsi, deux traces peuvent avoir la même projection ob-
servable d’un point de vue logique (séquence d’événements) mais pas d’un point de
vue temporisé (dates des événements). Ainsi, il est possible de discriminer un com-
portement défaillant en s’appuyant sur les dates d’occurrence des correspondants
événements observables. Dans ce cas, on parle de temps discriminant.
Exemple 3.6.1
Pour une meilleure compréhension de la notion de ∆-diagnosticabilité, nous
considérons l’exemple suivant, introduit dans (Tripakis, 2002). Nous sup-
posons que les événements a et b sont observables, les événements u et f
non observables et f l’événement de défaut. Il est clair que le langage tem-
porisé accepté par l’automate temporisé A illustré dans la figure 3.12 est
3-diagnosticable. D’abord, il faut noter que dans le comportement défaillant,
le délai entre l’événement b et l’événement de défaut est inférieur à 3 u.t.,
ce qui implique l’existence de l’événement b dans toute trace 3-défaillante.
L’observation de l’événement b nous permet de détecter le défaut dans tout
comportement défaillant. En effet, dans chaque comportement défaillant, le
délai entre les événements observés a et b est supérieur à 3 u.t.., tandis que
ce délai est inférieur à 3 u.t. dans chaque comportement normal.
Si nous considérons dans un second exemple l’automate temporisé A0 illus-
tré dans la figure 3.13. Le langage accepté par cet automate n’est pas diag-
nosticable. En effet, si nous considérons les deux traces (a, 0)(f, 2.5)(b, 0.1)
et (a, 0)(u, 2.5)(b, 0.1) acceptées par A0 , nous pouvons établir qu’elles ont la
même projection observable ; i.e., (a, 0)(b, 2.6), que la première trace contient
un défaut et que la seconde ne contient aucun défaut. En plus, pour toutes
continuations de ces deux traces obtenues par l’écoulement du temps, elles
admettent la même projection observable.
66
Chapitre 3. Diagnostic a base de modèles des SED et des SDH
linéaires
x
≤6
b
f, x > 3 : -
≤6
x
a, x := 0-
~
u, x ≤ 3 z b -
x≤3
x
≤6
b
f, x > 2 : -
≤6
x
~
a, x := 0-
u, x ≤ 3 z b -
x≤3
3.7 Conclusion
Dans ce chapitre, nous avons proposé un tour d’horizon sur les méthodes de sur-
veillance et diagnostic à base de modèles des systèmes à événements discrets et des
systèmes dynamiques hybrides. Nous avons classifié ces méthodes selon différents cri-
tères, parmi lesquels, le modèle utilisé pour représenter le comportement du système, la
représentation du temps : modèles logiques, denses, à temps discret. Nous énumérons
quelques remarques retenues à partir de notre étude :
1. une approche de référence a été proposée dans (Sampath et al., 1995), pour le
diagnostic des SED :
• cette méthode repose sur la conception d’un modèle complet du système décri-
vant le comportement normal et les comportements défaillants. Les événements
67
Chapitre 3. Diagnostic a base de modèles des SED et des SDH
linéaires
de défauts sont représentés par des événements non observables ;
• un diagnostiqueur, sous la forme d’un automate à états finis, est construit hors-
ligne, à partir du modèle du système. Ce diagnostiqueur est par la suite utilisé
en-ligne, pour inférer l’occurrence des événements de défaut en observant une
séquence d’événements observables générée par le système ;
• une notion de diagnosticabilité a été définie. Un modèle diagnosticable garantit
la discrimination de tout défaut au bout d’un nombre fini de transitions après
l’occurrence du défaut ;
• le diagnostic élaboré par cette approche considère une évolution complètement
discrète du système. En effet, le temps est considéré d’une manière qualitative à
travers l’ordre d’occurrence des événements ;
2. l’exploration des données temporelles relatives aux événements qui peuvent avoir
lieu dans un SED s’est avérée très fructueuse dans un processus de surveillance et
du diagnostic. En effet, elle augmente la capacité d’identification des défauts du
diagnostiqueur ;
3. une extension temporisée de l’approche de Sampath, reposant sur un modèle SED
à temps discret, a été proposée dans (Zad et al., 2003). Cette approche utilise un
événement spécial appelé tick d’horloge, pour représenter le passage du temps. La
discrétisation du temps entraîne une explosion combinatoire de la taille du modèle
du système ainsi que celui du diagnostiqueur. Ainsi, cette approche est inadéquate
pour le diagnostic des systèmes complexes ;
4. une extension inspirée des travaux de Sampath, dans le contexte des modèles tem-
porisés denses, a été proposée dans (Tripakis, 2002) :
• cette approche repose sur l’utilisation d’un algorithme d’estimation d’état du
système, exécuté en-ligne avec le système à diagnostiquer ;
• une extension de la définition de diagnosticabilité a été également proposée dans
le cadre des langages temporisés ;
• la complexité du diagnostic en-ligne est doublement exponentielle en fonction de
la taille de l’observation et du modèle du système ;
5. l’élaboration d’un complexe calcul en-ligne pénalise les performances du diagnostic
et le rend parfois l’approche inadéquate pour les systèmes temps réels critiques,
qui nécessitent une prise de décision rapide de la part du diagnostiqueur ;
6. conception hors-ligne d’un diagnostiqueur sous la forme d’un automate temporisé
est plus appropriée pour ces systèmes puisqu’elle nécessite peu d’effort en-ligne ;
7. la plupart des méthodes de diagnostic des SDH rencontrées dans la littérature sont
issues de contributions du domaine du diagnostic des systèmes continus ;
8. les méthodes de diagnostic issues de contributions SED, sont des méthodes quali-
tatives qui se basent sur une abstraction discrète de la dynamique continue et/ou
du temps ;
68
Chapitre 3. Diagnostic a base de modèles des SED et des SDH
linéaires
9. à notre connaissance, il existe peu de contributions de diagnostic pour les SDH,
reposant sur des modèles hybrides mixtes ;
10. à notre point de vue, l’indécidabilité du problème de vérification des modèles hy-
brides représente la principale difficulté empêchant le développement d’approches
de diagnostic à base de modèles hybrides denses.
11. le problème d’analyse d’accessibilité est décidable pour certaines sous-classes de
modèles hybrides, telles que les automates temporisés et les automates hybrides
rectangulaires initialisés.
69
Chapitre 3. Diagnostic a base de modèles des SED et des SDH
linéaires
70
Chapitre 4
4.1 Introduction
Les travaux de recherche menés dans le domaine du diagnostic des systèmes à événe-
ments discrets ont révélé l’importance du facteur temps. Plusieurs études ont montré que
ce facteur est souvent un porteur potentiel d’informations dans le cadre de la détection et
du diagnostic. L’exploration des données temporelles relatives aux événements occurrant
dans un SED s’est avérée très fructueuse dans un processus de diagnostic.
C’est à partir de ces faits que nous élaborons, dans ce chapitre, une approche de
diagnostic pour les Systèmes à Événements Discrets dont on connaît le comportement
temporel. La démarche de notre approche de diagnostic commence par la conception d’un
modèle temporisé du SED, décrivant son comportement normal ainsi que ses possibles
comportements défaillants. Ce modèle est donné sous la forme d’un automate tempo-
risé respectant certaines hypothèses. Le choix du modèle automate temporisé est justifié
par la généralité de ce modèle, sa capacité d’analyse et sa description intrinsèque des
contraintes temporelles existantes entre les différents événements du système (Bengtsson
et Yi., 2004). Nous considérons par ailleurs que les événements qui peuvent avoir lieu
sont de deux types : observables et non observables. Dans notre approche, nous visons
à maximiser l’exploitation des informations temporelles formulées par le modèle du sys-
tème en s’appuyant sur un ensemble d’outils, développés dans la littérature, permettant
l’analyse des automates temporisés.
La deuxième étape de notre démarche de diagnostic repose sur la construction, hors-
ligne, d’un automate temporisé, appelé diagnostiqueur, à partir du modèle du système.
Le diagnostiqueur est par la suite déployé, en-ligne, pour permettre l’identification des
défauts affectant le système. En effet, l’automate du diagnostiqueur reçoit les événements
observables générés par le système et évolue d’une manière déterministe d’un sommet à
un autre. Chaque sommet du diagnostiqueur fournit une estimation de l’état courant du
71
Chapitre 4. Diagnostic des systèmes temporisés
système ainsi que les possibles défaillances pouvant affecter son fonctionnement. En se
basant sur une analyse des données présentes dans le sommet courant du diagnostiqueur,
une fonction de décision émet une alarme lorsqu’un défaut est identifié.
Dans ce chapitre, nous commençons par définir le modèle automate temporisé qui
constitue le cadre formel de notre approche de diagnostic à base de modèles temporisés.
Ensuite, nous précisons le contexte général ainsi que les objectifs de la réalisation d’une
telle approche. En effet, nous illustrons, à travers des exemples, les différents scénarios
de discrimination de défaut qui doivent être pris en considération par notre approche.
Par la suite, nous présentons notre démarche de diagnostic à base de modèles tempo-
risés. D’abord, nous caractérisons les différentes hypothèses retenues sur le modèle du
système à diagnostiquer. Ensuite, nous détaillons l’algorithme de construction du diag-
nostiqueur à partir de la sous-classe de modèles considérée. Dans la section suivante,
nous présentons la notion de diagnosticabilité pour les langages temporisés ainsi qu’une
méthode systématique permettant de vérifier la diagnosticabilité du modèle considéré
dans notre travail. Enfin, nous exposons quelques éléments relatifs à l’implémentation et
la complexité de notre contribution.
Nous présentons dans cette section le modèle automate temporisé introduit par Alur
et Dill dans (Alur et Dill, 1994). Nous faisons un rappel de l’aspect syntaxique et sé-
mantique de ce formalisme de modélisation. Nous portons une attention particulière à
l’analyse symbolique de ce modèle.
Étant donnée une trace temporisée ω = (σ1 , d1 )(σ2 , d2 ) . . . (σk , dk ) . . . , on définit l’opé-
rateur k ω k qui permet de projeter les éléments d’une trace temporisée ω sur l’ensemble
des événements Σ : k ω k= σ1 σ2 . . .σk . . ..
72
Chapitre 4. Diagnostic des systèmes temporisés
Par exemple, étant donnée une trace temporisée ω = (a, 5)(b, 3)(c, 4)(d, 8)(e, 1), la
trace P{a,c,e} (ω) = (a, 5)(c, 7)(e, 9) correspond à la projection de ω sur l’ensemble des
événements Σ0 = {a, c, e}. Nous remarquons qu’après avoir éliminé l’événement b de la
trace ω, nous avons mis à jour le délai entre les événements a et c. En effet, le délai
calculé entre les événements a et c (égale à 7) correspond à la somme du délai entre a et
b (égale à 3) et celui entre b et c (égale à 4).
Définition 11. Un langage temporisé L est un ensemble de séquences temporisées ; i.e.,
L ⊆ (Σ × R+ )∞ . Étant donné un ensemble d’événements Σ0 , on définit la projection
du langage L sur l’ensemble Σ0 , notée par PΣ0 (L), comme l’ensemble constitué par les
projections sur Σ0 de toutes les traces de L.
Un automate temporisé est un automate à états finis muni d’un ensemble de variables
réelles positives appelées horloges. Les horloges sont incrémentées simultanément, avec
une dynamique égale à 1 et peuvent être remises à zéro. Les horloges sont des variables
fictives dans le sens où elles ne sont pas des variables du système, mais elles sont utilisées
pour mesurer le temps et définir les contraintes temporelles sur le franchissement des
transitions.
Une transition, entre deux sommets d’un automate temporisé, est franchie suite à
l’occurrence d’un événement en entrée et la satisfaction d’une contrainte de franchisse-
ment, appelée garde. Ce franchissement est instantané et peut déterminer la mise à zéro
d’un ensemble d’horloges.
Avant de définir formellement le modèle automate temporisé, nous introduisons, dans
ce qui suit, quelques notions préliminaires.
Définition 12. Étant donné un ensemble d’horloges X, l’ensemble des contraintes sur
X, noté C(X), est défini par la grammaire :
ψ ::= x ∼ c | x − y ∼ c | ψ ∧ ψ | ¬ψ | vrai
où x, y ∈ X, c ∈ Z, ∼∈ {<, ≤, =, ≥, >}.
73
Chapitre 4. Diagnostic des systèmes temporisés
Définition 13. L’ensemble des gardes sur X, noté G(X), est le sous-ensemble de C(X),
ne contenant pas des contraintes de la forme x − y ∼ c, dites contraintes diagonales. En
effet, l’ensemble G(X) est défini par la grammaire suivante :
g ::= x ∼ c | g ∧ g | ¬g | vrai
où x ∈ X, c ∈ Z, ∼∈ {<, ≤, =, ≥, >}.
Définition 15. Un automate temporisé est dit déterministe si pour chaque paire de
transitions (q, σ, g, Y, q 0 ) et (q, σ, g 0 , Y 0 , q 00 ) ayant le même événement de franchissement
σ et issues du même sommet q, les contraintes de garde g et g 0 sont disjointes ; i.e.,
l’ensemble des valuations d’horloges satisfaisant à la fois les deux gardes est vide.
Remarque 2. Pour des raisons de lisibilité, lorsque la garde d’une transition vaut vrai
ou que l’ensemble de réinitialisation est vide, le champ de la composante en question ne
sera pas représenté.
74
Chapitre 4. Diagnostic des systèmes temporisés
Exemple 4.2.1
Nous présentons dans la figure 4.1-a un simple système de chauffage de
liquides. Ce système comporte deux vannes V1 and V2 , un bac, un thermostat
et deux capteurs de niveau : le capteur S1 qui surveille le niveau maximal et
le capteur S2 qui surveille le niveau minimal. Le système commence par une
phase de remplissage, en utilisant la vanne V1 . Dès que le niveau du liquide
atteint le niveau maximal, après une intervalle de [40,50] u.t., un capteur
de niveau émet l’événement rempli, la vanne V1 passe en position fermée
et le système commence la phase de chauffage qui dure 60 u.t.. Ensuite, le
contrôleur commande l’évacuation du liquide présent dans un bac en ouvrant
la vanne V2 . La phase d’évacuation dure entre 20 et 25 u.t.. Elle s’achève
lorsque le capteur de niveau S2 détecte que bac est vide et alerte le contrôleur
par l’émission de l’événement vide. A l’interception de cet événement, le
contrôleur ferme la vanne V2 pour commencer un nouveau cycle du système.
L’automate temporisé décrit dans la figure 4.1-b présente le fonctionne-
ment de ce système. Il comporte trois sommets chacun correspond à une
phase de fonctionnement du système. Le passage d’une phase à une autre se
fait suite à l’occurrence d’un événement : rempli, évacuer ou vide. L’hor-
loge x permet de mesurer le temps écoulé après l’occurrence de chacun de
ces événements. En effet, cette horloge est remise à zéro après le franchisse-
ment d’une transition sur chacun de ces événements. Puisque les conditions
des invariants sont toutes bornées, le système ne peut séjourner dans l’un de
ces sommets que pendant une durée finie. Par exemple, pendant la phase du
remplissage, le système ne peut pas séjourner plus que 50 u.t. dans le sommet
remplissage. Ainsi, une transition sur l’événement rempli, vers le sommet
chauffage, doit être franchie lorsque la valeur de x se trouve dans l’intervalle
[40,50].
remplissage
- x ≤ 50
V1
rempli,x ≤ 50 ∧ x ≥ 40 vide, x ≤ 25 ∧ x ≥ 20
x := 0
I x := 0
S1
chauffage évacuation
a
-
S2 x ≤ 60 x ≤ 25
V2 évacuer,x = 60
x := 0
(a) (b)
75
Chapitre 4. Diagnostic des systèmes temporisés
4.2.3 Sémantique
Définition 16. Soit X un ensemble fini d’horloges. Une valuation des horloges est une
fonction v : X → R+ , qui associe un nombre réel positif à chaque horloge de X.
(v + d)(x) = v(x) + d, ∀x ∈ X
Définition 17. Un état d’un automate temporisé est un couple (q, v), où q est un
sommet et v une valuation d’horloges. La configuration initiale d’un automate temporisé
est (q0 , v0 ) où v0 (x) = 0 pour toute horloge x ∈ X. La notation v g, où v ∈ Rn+ et
g ∈ G(X), signifie que la valuation v vérifie la garde g.
Définition 18. Un chemin dans un automate temporisé A est une séquence finie ou
infinie de transitions de E de la forme
σ1 ,g1 ,Y1 σ2 ,g2 ,Y2 σ3 ,g3 ,Y3
p = q0 −−−−→ q1 −−−−→ q2 −−−−→ q3 . . .
D’une manière informelle, l’automate temporisé admet deux types d’évolution pos-
sibles :
• les transitions de temps : l’automate séjourne dans le même sommet en laissant
le temps s’écouler. En effet, les valeurs des variables progressent d’une manière
synchrone avec la même durée, en respectant la contrainte de l’invariant du
d
sommet. Formellement, (q, v) →− (q, v + d) pour d ∈ R+ , si ∀0 ≤ t ≤ d, v + t I(q).
• les transitions d’actions : Ces transitions font évoluer l’automate d’un sommet
à un autre. Une transition d’action est possible lorsque la valuation courante des
horloges satisfait la contrainte de garde et un événement est réalisé. Ces transitions
sont instantanées en plus. En plus, le franchissement d’une transition peut remettre
σ σ,g,Y
− (q 0 , v 0 ) s’il existe q −−−→
à zéro un sous-ensemble d’horloges. Formellement, (q, v) →
q 0 ∈ E tel que v g, v 0 = v[Y ← 0] et v 0 I(q 0 ).
76
Chapitre 4. Diagnostic des systèmes temporisés
Définition 19. Une exécution r sur le chemin p est une suite de transitions d’actions et
de transitions de temps définie de la manière suivante :
où chaque délai (di )i≥1 correspond à la durée de temps écoulée entre les événements
σi−1 et σi et (vi )i≥0 sont des valuations d’horloges définies comme suit :
• v0 (x) = 0, ∀x ∈ X,
• ∀i ≥ 1, vi−1 + d i gi ,
0, si x ∈ Yi
• ∀i ≥ 1, vi (x)=
vi−1 (x) + di , sinon.
Définition 20. Une séquence (ou une trace) temporisée ω = (σ1 , d1 )(σ2 , d2 )(σ3 , d3 ) . . .
est dite acceptée par un automate temporisé A, s’il existe une exécution de A qui évolue
sur les éléments de ω.
Définition 21. L’ensemble des séquences qui sont acceptées par l’automate A forment
le langage accepté (ou reconnu) par A, noté L(A). En cas d’absence d’ambiguïtés, nous
notons ce langage simplement par L.
Définition 22. Un état (q 0 , v 0 ) d’un automate temporisé est dit atteignable (ou ac-
cessible) depuis un état (q, v), qu’on note par (q, v) (q 0 , v 0 ), s’il existe une exécu-
tion qui commence à l’état (q, v) et qui progresse vers l’état (q 0 , v 0 ). Nous notons par
ω
(q0 , v0 ) (q, v), un état (q, v) atteignable depuis l’état initial (q0 , v0 ), à travers une exé-
cution sur la trace temporisée ω.
Exemple 4.2.2
Considérons l’automate temporisé introduit dans l’exemple 4.2.1. Nous illus-
trons une exécution possible de l’automate de la figure 4.1-b, sur la trace
temporisée (rempli, 47.4)(évacuer, 60)(vide, 23.1) . . . :
rempli,x≤50∧x≥40,x:=0 évacuer,x=60,x:=0
hremplissage, 0i −−−−−−−−−−−−−−→ hchauffage, 0i −−−−−−−−−−→
47.4 60
vide,x≤25∧x≥20,x:=0
hévacuation, 0i −−−−−−−−−−−−→ hremplissage, 0i . . .
23.1
77
Chapitre 4. Diagnostic des systèmes temporisés
La propriété de divergence du temps garantit l’absence des traces infinies qui s’exé-
cutent dans un temps fini, dites aussi exécutions zénon (Tripakis, 1999).
Définition 24. Un automate temporisé A est dit Fortement Non-Zénon (FNZ) (Tripa-
kis, 1999), s’il existe un entier naturel d > 0, tel que chaque exécution évoluant dans un
cycle de transitions de A, admet une durée supérieure à d. Nous pouvons facilement éta-
blir que les conditions suivantes garantissent qu’un automate temporisé A est fortement
non-zénon :
1 e 2 e ek−1 k e
Pour chaque cycle de transitions q1 −→ q2 −
→ . . . −−→ qk −
→ q1 dans A, il existe au
0
moins deux transitions e, e dans ce cycle, une horloge x et un entier naturel c ≤ 1, tels
que :
1. x est remise à zéro dans e ;
2. x admet la valeur c comme une borne inférieure dans la contrainte de garde g 0
associée à la transition e0 : g 0 ∧ (x < c) = ∅.
Nous rappelons dans la suite quelques résultats intéressants sur le modèle automate
temporisé.
• Le problème du vide : Ce problème consiste à vérifier si un automate temporisé
accepte au moins une trace temporisée ; i.e., décider si L(A) est vide, où A désigne
un automate temporisé.
Ce problème a été montré décidable et sa complexité est PSPACE-Complet (Alur
et Dill, 1994).
• Le problème d’atteignabilité (ou d’accessibilité) : ce problème consiste à
vérifier, pour un état donné (q, v) d’un automate temporisé, s’il existe une exécu-
tion de l’automate telle que (q, v) est accessible depuis l’état initial à travers cet
exécution.
Ce problème a été montré décidable et sa complexité est PSPACE-Complet (Alur
et Dill, 1994).
78
Chapitre 4. Diagnostic des systèmes temporisés
Dans la mesure où le temps est continu, il est impossible d’énumérer tous les états
d’un automate temporisé. En d’autres termes, l’espace d’état d’un automate temporisé
est infini et non dénombrable. Pour pouvoir vérifier un modèle automate temporisé, il
est nécessaire de disposer d’une représentation symbolique permettant de manipuler cet
espace d’état.
Alur et Dill proposent dans (Alur et Dill, 1994) une abstraction de l’espace d’état
basée sur la notion de région. Cette notion représente la base formelle qu’a permis de
prouver la décidabilité des problèmes du vide et d’atteignabilité. Le principe de cette
construction consiste à abstraire les comportements des automates temporisés en un
ensemble de classes d’équivalence, appelés régions. En effet, l’ensemble infini des états
est partitionné en des régions. Chaque région est constituée d’un ensemble d’états liés
par une relation d’équivalence comportementale appelée relation de bisimulation. Cette
relation est définie de la manière suivante. Deux états (l, v) et (l0 , v 0 ) sont équivalents,
si (1) l = l0 et (2) v ∼=K v 0 , où K désigne la constante maximale qui apparaît dans
l’automate. Deux valuations v et v 0 sont équivalentes, qu’on note v ∼
=K v 0 , si les conditions
suivantes sont vérifées :
79
Chapitre 4. Diagnostic des systèmes temporisés
Exemple 4.2.3
Dans l’exemple suivant, nous illustrons un exemple de partition en régions
d’un espace d’état.
région
(1 < x < 2) ∧ (0 < y < 1) ∧ (0 < x − y < 1)
y
6
1 9 régions ponctuelles
?
22 régions linéaires
-x 13 régions surfaciques
0 1 2
Fig. 4.2 – Un exemple d’une région définie par deux horloges x et y
Il est clair à travers cet exemple que la notion de région est trop fine pour être
utilisée par des algorithmes d’analyse d’automates temporisés. Une autre abstraction
plus efficace de l’espace d’état a été proposée dans la littérature (Alur, 1999). Cette
représentation symbolique se base sur la notion de zones. Une zone est un ensemble de
valuations défini par une contrainte de l’ensemble C(X).
Durant l’analyse en avant d’un automate temporisé, les objets qui seront manipulés
seront des paires (q,z), appelées états symboliques, où q est un sommet de l’automate
et z une zone. Un état symbolique peut être considéré comme une union de régions.
Dans la figure 4.3, nous illustrons l’exemple d’une zone définie par deux horloges x et
y. Cette zone peut être décrite par la contrainte h(y ≤ 4) ∧ (x ≤ 5) ∧ (1 ≤ x − y ≤
4)i. Nous notons que cette zone peut être représentée par des formules de contraintes
différentes. Cependant, il existe une représentation unique pour chaque zone d’horloges
(convexe ou non-convexe), appelée représentation canonique (Bengtsson et Yi., 2004).
80
Chapitre 4. Diagnostic des systèmes temporisés
81
Chapitre 4. Diagnostic des systèmes temporisés
σ,g,Y
Soient q −−−→ q 0 ∈ E une transition d’un automate temporisé et (q, z) un état symbo-
lique. L’état symbolique (q, z) peut évoluer selon deux manières :
• les transitions de temps : définies par l’opérateur P ostt ((q, z)) = (q, z 0 ) où z 0 =
{v 0 | ∃d ∈ R+ , v 0 = v + d, v 0 ∈ I(q), v ∈ z} = z ↑ ∧I(q).
σ,g,Y
• les transitions d’actions : définies par l’opérateur P ostd ((q, z), −−−→) = (q 0 , z 0 ), où
σ
z 0 = {v 0 | (q, v) →
− (q 0 , v 0 ), v ∈ z} = ((z ∧ g)[Y ← 0]) ∧ I(q 0 ).
σ,g,Y
On définit le successeur d’un état symbolique (q, z) sur une transition q −−−→ q 0 ∈ E
par :
σ,g,Y σ,g,Y
P ost((q, z), −−−→) = P ostt ◦ P ostd ((q, z), −−−→)
Généralement, l’étude d’un système modélisé par un automate temporisé est basée
sur l’analyse de l’atteignabilité des états de l’automate. Pour savoir si un ensemble d’états
d’arrivée, défini par un état symbolique (q 0 , z 0 ) est atteignable depuis un ensemble d’état
de départ (q, z), nous pouvons appliquer une analyse d’atteignabilité à partir de l’en-
semble des états de départ. Cette analyse permet de calculer tous les états qui peuvent
être accessibles depuis les états définis par le couple (q, z). Si l’espace calculé contient des
états qui appartiennent également à l’ensemble d’états d’arrivée (q 0 , z 0 ), alors on peut
dire que l’ensemble d’arrivée est atteignable depuis l’ensemble de départ. L’opérateur
P ost, défini ci-dessus, permet d’établir l’analyse d’atteignabilité en avant. En effet, il
82
Chapitre 4. Diagnostic des systèmes temporisés
Dans ce travail, nous nous basons sur les travaux de Sampath (Sampath et al., 1995,
1996), qui propose la compilation d’un diagnostiqueur à partir d’un modèle automate
à états finis du système. Notre objectif consiste à développer une nouvelle approche
de diagnostic dans le cadre des modèles temporisés à temps continu (par opposition
aux modèles à temps discret). Dans la figure 4.7, nous illustrons le schéma global de
l’approche de diagnostic que nous allons développer.
Modèle
temporisé du système
procédure de synthèse
du diagnostiqueur Construction hors-ligne
Déploiement en-ligne
Système
- PO
compte-rendus
commandes
PC
Fig. 4.7 – Schéma global de notre approche de diagnostic à base d’automates temporisés
Comme une hypothèse de départ, nous supposons que nous disposons d’une part, du
modèle du système à diagnostiquer décrivant les comportements événementiel et tem-
porel du système et d’une autre part, d’une observation partielle des événements de
83
Chapitre 4. Diagnostic des systèmes temporisés
ce système. Le modèle du système est supposé être "complet" dans le sens où il présente
tous les comportements normaux et anormaux (défaillants) du système. Nous désirons
construire le diagnostiqueur de ce système, sous la forme d’un modèle temporisé. Le
diagnostiqueur observe, en-ligne, le système pour estimer son état et les défauts pouvant
affecter son fonctionnement. En se basant sur cette estimation, une fonction de décision
déclenche une alarme quand un défaut certain est identifié.
Le rôle du diagnostiqueur consiste à inférer les occurrences des défauts non
observables en se basant sur les événements observables ainsi que les délais écoulés
entre ces événements. Nous souhaitons maximiser l’exploitation des contraintes tempo-
relles existantes dans le modèle du système, afin de pouvoir discriminer tout mode de
défaillance potentiel.
Dans la suite, nous illustrons les différents scénarios de discrimination de défauts que
doit supporter notre approche. En effet, pour permettre le diagnostic d’un SED, notre
approche repose sur des méthodes de discrimination combinant l’aspect événementiel et
l’aspect temporel de l’évolution d’un SED. D’abord, nous rappelons que la perturba-
tion du comportement d’un SED qui se produit suite à l’occurrence d’un défaut, peut
correspondre à une perturbation purement événementielle (apparition d’un nouvel événe-
ment ou le changement de l’ordre des événements qui suivent le défaut) et/ou temporelle
(changement des dates d’occurrence des événements qui suivent le défaut). En effet, nous
pouvons distinguer trois scénarios de discrimination de défauts, déterminés par la nature
de la perturbation observée (temporelle ou événementielle) :
(1) Discrimination purement événementielle c’est sur ce principe que re-
pose les travaux de Sampath (Sampath et al., 1995, 1996) dans le cadre du diagnostic à
base de modèles logiques. En effet, le diagnostic d’un SED est établi en utilisant unique-
ment une séquence d’événements observables non temporisée qui suit l’occurrence d’un
défaut. Un défaut peut être identifié uniquement si son occurrence affecte, d’une manière
unique et discriminante, la trajectoire des événements observables succédant le défaut.
A titre d’exemple, cette approche peut être appliquée pour permettre le diagnostic d’un
débordement dans un bassin en phase de remplissage. En effet, un capteur de niveau
d’urgence émet une alarme lors du débordement. Cet événement (l’alarme du capteur)
permet de distinguer la trajectoire défaillante du système, sans ayant recours à d’autres
informations comme la date d’occurrence de cet événement.
Il faut noter que cette approche ne sera plus d’une grande utilité si les trajectoires
à distinguer admettent des projections observables identiques d’un point de vue logique
(même ordre des événements dans les séquences observées). Dans ce cas, il faut prendre
en considération les dates d’occurrence des événements observables, ce qui nous conduit
à définir le deuxième scénario de discrimination.
(2) Discrimination temporelle par le biais d’événements temporisés
84
Chapitre 4. Diagnostic des systèmes temporisés
Selon la gravité de cette fuite, le niveau du liquide dans le bac baissera d’une manière
progressive. En admettant qu’il s’agit d’une petite fuite, l’occurrence de ce défaut va
affecter légèrement la date d’occurrence de l’événement rempli qui se produit lorsque
x ∈ [40, 50] (pareil que le cas du fonctionnement normal). Pendant la phase de chauf-
fage, le niveau du liquide va baisser d’une manière considérable dans le fonctionnement
affecté par la fuite. En effet, à la fin de la phase d’évacuation, l’événement vide, généré
par le capteur de niveau S2 , se produit à une date définie par (x < 20). Par contre, cet
événement se produit à une date postérieure, définie par x ∈ [20, 25], dans le comporte-
ment normal. Ainsi, la date d’occurrence de l’événement vide permet la discrimination
du comportement défaillant.
(3) Discrimination temporelle sur le dépassement d’un seuil d’attente
Comme dans le cas précédent, nous allons illustrer ce scénario de discrimination à
travers l’introduction d’un autre cas de défaut. En effet, nous introduisons sur le modèle
illustré de la figure 4.9, un cas de défaut correspondant au blocage de la vanne V1 en
position fermée. Suite à l’occurrence de ce défaut, la phase de remplissage ne va pas
s’achever et par conséquent, l’événement rempli ne sera pas généré par le capteur de
niveau S1 . Dans le modèle considéré, nous modélisons l’état défaillant qui suit l’occur-
rence de l’événement de défaut blocage_V1 par le sommet final vanne bloquée. En
effet, lorsque le système évolue vers ce sommet, il ne peut plus progresser vers un autre
sommet.
La discrimination de ce scénario de défaut peut être établi à travers le dépassement
d’un délai seuil d’attente sans observer des événements. Ainsi, si l’événement rempli
n’est pas observé au bout de 50 u.t., nous pouvons conclure que le système a évolué vers
85
Chapitre 4. Diagnostic des systèmes temporisés
le sommet vanne bloquée. Ainsi, le dépassement d’un seuil d’attente nous a permis
d’identifier ce défaut.
blocage_V1 , x ≤ 50 ?
remplissage f uite, x ≤ 50
- rempl & fuite
vanne bloquée
x ≤ 50 x ≤ 50
rempli,x ≤ 50 ∧ x ≥ 40 vide, x ≤ 25 ∧ x ≥ 20 vide, x < 20
x := 0
I x := 0
I
rempli,x ≤ 50 ∧ x ≥ 40 x := 0
x := 0
chauffage évacuation chauf & fuite évac & fuite
x ≤ 60
- x ≤ 25 -
x ≤ 60 x < 20
évacuer,x = 60 évacuer,x = 60
x := 0 x := 0
Remarque 1. Dans les modèles illustrés dans les figures 4.8 et 4.9, les événements des
défauts peuvent se produire uniquement pendant la phase de remplissage (à partir du
sommet remplissage). Cependant, il est possible que ces défauts se produisent pendant
la phase de chauffage ou d’évacuation. Le choix de ne pas représenter certaines transitions
de défaut est considéré dans le but d’alléger la structure du modèle permettant ainsi de
simplifier la compréhension de notre approche, qui reste toutefois applicable pour un
modèle plus complet.
Nous présentons dans cette section les différentes étapes de notre méthode de diag-
nostic à base d’automates temporisés. Dans une première étape, nous caractérisons les
spécifications et les hypothèses retenues sur le modèle automate temporisé du système
à diagnostiquer. Dans une seconde étape, nous illustrons l’algorithme de synthèse du
diagnostiqueur qui représente le cœur de notre approche de diagnostic.
Dans notre travail, nous avons choisi le formalisme des automates temporisés comme
outil de base pour la modélisation des systèmes à diagnostiquer. Ce choix est justi-
fié par la généralité qu’offrent les automates temporisés, leur capacité à représenter les
contraintes temporelles liées à l’occurrence des événements, leur pouvoir d’expression et
les possibilités de modélisation qu’ils donnent (Alur, 1999). En plus, ces modèles bénéfi-
cient d’une grande capacité d’analyse (Bengtsson et Yi., 2004). En effet, plusieurs outils
86
Chapitre 4. Diagnostic des systèmes temporisés
de modélisation d’analyse ont été développés dans la littérature tel que UPPAAL (Larsen
et al., 1997) et KRONOS (Yovine, 1997). Par ailleurs, comme nous avons indiqué dans
le chapitre précédent, certains outils de modélisation temporisés, tel que le modèle RdP
temporel, peuvent être traduits à des automates temporisés, ayant un comportement
équivalent, obtenus en appliquant des algorithmes de transformation (Cassez et Roux,
2006).
Nous supposons que le système à diagnostiquer est modélisé par un automate tem-
porisé A = (Q, X, Σ, E, q0 , Qf , I). Par ailleurs, nous supposons que ce modèle respecte
un ensemble de spécifications, caractérisant essentiellement la modélisation des défauts.
Ces spécifications sont énumérées ci-dessous :
• le modèle du système est "complet", ainsi, il permet de décrire les comportements
normaux et anormaux (défaillants) ;
• les défauts sont supposés être permanents. En effet, le système ne peut pas
retourner au comportement normal après l’occurrence d’un défaut ;
• à son état initial, nous supposons que le système est dépourvu de défauts. Ainsi,
cet état fait partie de l’ensemble des états du comportement normal.
Dans la suite, nous considérons une propriété permettant de caractériser une des
hypothèses à considérer sur le modèle du système. Intuitivement, cette propriété stipule
que : si deux chemins dans un automate temporisé ont les mêmes séquences de transitions
observables, alors ils doivent avoir des ensembles de réinitialisation d’horloges identiques
87
Chapitre 4. Diagnostic des systèmes temporisés
(∃j ∈ {1, . . . , n}, ∀i ∈ {1, . . . , j}, σio = σ̃io ) ⇒ (∀i ∈ {1, . . . , j}, Yio = Ỹio )
Par une simple inspection de cet automate temporisé, nous pouvons af-
firmer qu’il vérifie la propriété 1. En effet, les transitions sur les événements
a u b c a f b c
b et c, dans les chemins 1 → − 2 → − 3 → − 4 → − 5 et 1 → − 2 →− 7 → − 8 →
− 9,
admettent les mêmes ensembles de réinitialisation d’horloges. Les réinitiali-
sations d’horloges dans les transitions sur les événements d et e peuvent être
différentes.
La vérification de cette propriété est simple à effectuer sur cet exemple. Par contre,
elle sera plus compliquée à réaliser pour des modèles de plus grandes tailles. Ainsi, il
faut disposer d’une technique systématique permettant la vérification de cette propriété.
Pour ce faire, nous proposons l’application d’un algorithme inspiré de la procédure de
déterminisation des automates à états finis (Cassandras et Lafortune, 1999). Dans une
première étape, nous éliminons toutes les contraintes de gardes et d’invariants définies
dans l’automate. Ensuite, nous appliquons l’algorithme de déterminisation d’automates à
états finis, en considérant les événements non observables comme des actions silencieuses.
Cette construction permet de définir une classe d’équivalence sur l’ensemble des sommets
88
Chapitre 4. Diagnostic des systèmes temporisés
de l’automate, où chaque paire de sommets équivalents est accessible par deux chemins
vérifiant la propriété 1. Pendant cette opération de déterminisation, si deux transitions
sur le même événement observable, issues de deux sommets équivalents, admettent des
ensembles de réinitialisation différents, nous arrêtons l’algorithme et nous annonçons
que la propriété 1 n’est pas vérifiée. Lorsque l’algorithme se termine normalement, nous
annonçons que le modèle vérifie la propriété.
La figure 4.11 présente une application de l’algorithme de vérification de la propriété 1
sur le modèle de la figure 4.10.
Hypothèses :
Nous supposons que le modèle du système A satisfait les hypothèses suivantes :
H1 ) A est fortement non-zénon ;
H2 ) aucune affectation d’horloges n’est autorisée dans les transitions sur des
événements non observables ;
H4 ) les horloges {x1 , . . . , xn } sont bornées par une constante entière positive K, dans
chaque sommet q non-final ; i.e., I(q) = x1 ≤ K ∧ · · · ∧ xn ≤ K, q ∈ Q − Qf , et
sont non bornées dans chaque sommet final ; i.e., I(q) = vrai, q ∈ Qf .
Nous remarquons que les hypothèses H2 et H3 permettent de caractériser les en-
sembles de réinitialisation d’horloges définis dans les transitions de l’automate temporisé.
Nous notons que le mise à zéro aléatoire d’horloges constitue une des principales sources
d’indécidabilité du problème de déterminisation des automates temporisés (Bérard et al.,
1998). En effet, les auteurs présentent dans (Alur et Dill, 1994) un exemple où la déter-
minisation d’un automate temporisé, comportant une réinitialisation d’horloge sur une
-transition, nécessite un nombre infini d’horloges.
L’hypothèse H1 garantit l’existence d’une borne inférieure pour l’exécution de chaque
cycle de l’automate temporisée et par conséquent, la divergence du temps de chaque
exécution. Cette hypothèse est intrinsèquement vérifiée dans les systèmes réels où la
progression temps diverge.
89
Chapitre 4. Diagnostic des systèmes temporisés
Enfin, l’hypothèse H4 restreint la durée de séjour dans chaque sommet non final
de l’automate temporisé. Aucune restriction n’est imposée pour le séjour dans les som-
mets finaux. Ainsi, l’automate peut séjourner indéfiniment dans un sommet final, sans
pouvoir progresser vers un autre sommet. C’est pourquoi on peut qualifier les sommets
finaux par sommets puits. Cette hypothèse est très importante puisqu’elle nous permet
de délimiter l’espace d’état du système. Ainsi les valuations des états correspondant à
des sommets non-finaux sont incluses dans un hypercube (Allaham, 2008) de dimen-
sion K. En considérant cette hypothèse, l’analyse d’atteignabilité appliquée au modèle
considéré se termine au bout d’un temps fini (sans besoin de normalisation de zones), en
considérant que l’espace d’état définit un ensemble fini de zones d’horloges.
Remarque 2. La combinaison des hypothèses H1 et H2 conduit à l’absence de cycles de
transitions sur des événements non observables. En effet, à partir d’un sommet non-final,
une transition sur un événement observable se produit toujours au bout d’un délai fini.
Exemple 4.4.2
Nous pouvons constater, par une simple inspection de l’automate temporisé
dans la figure 4.9, que ce dernier vérifie les spécifications de modélisation
considérées. En effet, ce modèle comporte deux événements de défauts f uite
et blocage_V1 . Ces deux défauts sont permanents (pas de transitions de re-
tour vers le comportment normal).
Nous allons vérifier dans ce qui suit, si ce modèle satisfait les hypothèses
Hi∈{1,...,4} :
1. H1 est satisfaite par le modèle. En effet, chaque transition sur un événe-
ment non observable comporte un ensemble de réinitialisation d’horloges
vide ;
2. H2 est satisfaite par le modèle. En effet, l’horloge x est réinitialisée
dans deux transitions appartenant aux deux cycles du modèle. En plus,
nous constatons que chacun de ces deux cycles comporte une transition
ayant une contrainte de garde inférieurement bornée par la valeur 40 ;
3. H3 est satisfaite par le modèle. La propriété 1 est satisfaite par ce
modèle puisque les deux cycles : celui du comportement normal et celui
du comportement défaillant, admettent le même ensemble d’affectation
d’horloges (x := 0) dans toutes les transitions.
4. H4 n’est pas satisfaite par le modèle. En effet, les sommets non fi-
naux admettent différentes conditions d’invariants. Pour pallier à ce
problème, nous proposons de borner l’horloge x dans tous les sommets
non-finaux par la valeur 60. Ainsi, nous obtenons le modèle illustré dans
la figure 4.12, qui vérifie l’hypothèse H4 .
Remarque 3. Comme dans cet exemple, nous sommes contraints parfois de changer les
conditions d’invariants afin que le modèle du système respecte l’hypothèse H4 , ce qui
90
Chapitre 4. Diagnostic des systèmes temporisés
blocage_V1 , x ≤ 50
?
remplissage f uite, x ≤ 50
- rempl & fuite
vanne bloquée
x ≤ 60 x ≤ 60
rempli,x ≤ 50 ∧ x ≥ 40 vide, x ≤ 25 ∧ x ≥ 20 vide, x < 20
x := 0
I x := 0
I
rempli,x ≤ 50 ∧ x ≥ 40 x := 0
x := 0
chauffage évacuation chauf & fuite évac & fuite
x ≤ 60
- x ≤ 60 -
x ≤ 60 x ≤ 60
évacuer,x = 60 évacuer,x = 60
x := 0 x := 0
Fig. 4.12 – Modèle du système de chauffage de liquides vérifiant toutes les hypothèses de
modélisation
Nous présentons dans cette partie la structure du diagnostiqueur que nous désirons
construire à partir d’un automate temporisé vérifiant les hypothèses et les spécifications
énumérées ci-dessus. La structure de notre diagnostiqueur est inspirée du modèle du
diagnostiqueur proposé dans les travaux de Sampath (Sampath et al., 1995, 1996).
Notre diagnostiqueur est un automate temporisé déterministe, compilé à partir du
modèle du système. Cet automate est exécuté en-ligne avec le système pour permettre
l’élaboration du diagnostic. Une évolution d’un sommet à un autre dans cet automate se
91
Chapitre 4. Diagnostic des systèmes temporisés
fait uniquement par le biais de transitions sur des événements observables. Par ailleurs,
le diagnostiqueur peut évoluer vers un autre sommet suite à l’écoulement d’un délai seuil
d’attente à travers des transitions urgentes (Barbuti et Tesei, 2004).
Les sommets du diagnostiqueur correspondent à des macro-états (Ghazel, 2005),
pouvant contenir plusieurs ensembles d’états du système enrichis par des informations
relatives aux défauts. En effet, après l’occurrence de chaque événement observable, le
diagnostiqueur évolue vers le prochain sommet qui fournit une estimation de l’état du
système, à l’instant du franchissement de cet événement. Par ailleurs, à chacun de ces
états est associé une étiquette de diagnostic permettant d’indiquer si un défaut s’est
produit dans l’exécution menant vers cet état.
Dans la suite, nous présentons une définition formelle de l’automate temporisé du
diagnostiqueur.
Nous notons par Φ = {N , F1 , F2 , . . . , Fm }, un ensemble d’étiquettes, dites étiquettes
de diagnostic. Ces étiquettes permettent de déterminer le mode de défauts affectant un
ensemble d’états du système. En effet, un ensemble d’états du système est qualifié de
Fi -défaillant, s’il est associé à une étiquette Fi . Autrement dit, un défaut de l’ensemble
Fi s’est produit avant d’atteindre un état de cet ensemble. De même, un ensemble d’états
est qualifié de normal, s’il est associé à l’étiquette N . Dans ce dernier cas, aucun défaut
ne s’est produit avant d’atteindre un état de cet ensemble.
Définition 25. Un diagnostiqueur est un automate temporisé déterministe D =
(Qd , X, Σo , E d , q0d , Qdf , I), où :
• Qd ⊂ 2Q×F ×C(X) est un ensemble de sommets du diagnostiqueur. Chaque sommet
du diagnostiqueur est défini par un ensemble q d = ({(qi , φi ), i ∈ {1, . . . , k}}, z), où
z désigne une zone d’horloges et (qi , φi ), i ∈ {1, . . . , k} correspond à un ensemble
de couples "sommet/étiquette de diagnostic".
• E d est un ensemble fini de transitions. Une transition entre deux sommets du
diagnostiqueur qd et qd0 est définie par un quintuplet (qd , σ, g, Y, qd0 ), où σ désigne un
événement observable ; i.e., σ ∈ Σo , et g est une contrainte de garde de l’ensemble
C(X).
• q0d désigne le sommet initial du diagnostiqueur. Ce sommet est défini comme suit :
q0d = ({(q0 , N )}, z0 ), où q0 désigne le sommet initial du modèle du système et z0
désigne la zone d’horloge initiale. Cette zone ponctuelle associe la valeur 0 pour
toutes les horloges de l’ensemble X ; i.e., x1 = x2 = · · · = xn = 0. L’étiquette N
indique que cet état initial fait partie du comportement normal du système.
• Qdf désigne l’ensemble des sommets finaux,
• I est la fonction qui associe une contrainte d’invariant à chaque sommet.
Remarque 3. Nous soulignons que, contrairement à la définition originale des automates
temporisés introduite dans (Alur et Dill, 1994), les conditions des gardes des transitions
définies dans l’automate temporisé du diagnostiqueur contiennent des contraintes diago-
92
Chapitre 4. Diagnostic des systèmes temporisés
Exemple 4.4.3
L’automate temporisé de la figure 4.13 représente le diagnostiqueur du sys-
tème de chauffage de liquides, obtenu à partir du modèle de la figure 4.12.
Chaque sommet de ce diagnostiqueur comporte un ensemble de paires (som-
met,étiquette), associé à une contrainte sur l’horloge x qui définie la valuation
de cette horloge après le franchissement de la transition d’entrée du sommet.
Afin de construire ce diagnostiqueur, nous avons considéré la partition de
défauts suivante : Σf = F1 ∪ F2 , où F1 = {f uite} correspond à l’occurrence
d’une fuite et F2 = {blocage_V1 } correspond au blocage de la vanne V1 . Nous
allons considérer deux cas d’application de ce diagnostiqueur. Nous suppo-
sons, dans un premier cas, que le système effectue une exécution sur la trace :
(f uite,10)(rempli,37.4)(évacuer,60)(vide,13). En observant la projection ob-
servable de cette trace : (rempli,47.4)(évacuer,60)(vide,13), le diagnostiqueur
évolue vers le sommet ({(rempl. & fuite,F1 )}, x = 0). La fonction de dé-
cision constate que le sommet est F1 -certain et génère, par conséquence, une
93
Chapitre 4. Diagnostic des systèmes temporisés
?
vanne bloquée,F2 remplissage,N
x ≥ 51 x=0
51
6 rempli,40 ≤ x ≤ 50,x := 0
?
chauffage,N
-
chauf & fuite,F1
x=0
rempli,40 ≤ x ≤ 50,x := 0 évacuer,x = 60, x := 0
?
évacuation,N
évac & fuite,F1 - rempl & fuite,F1
x=0 x=0
vide, 0 ≤ x < 20, x := 0
rempli,40 ≤ x ≤ 50,x := 0
vide, 20 ≤ x ≤ 25, x := 0 ?
?
remplissage,N chauf & fuite,F1
x=0 x=0 vide, 0 ≤ x < 20, x := 0
51
évacuer,x = 60, x := 0
?
évac & fuite,F1
x=0
Remarque 4. Dans cet exemple, nous avons utilisé dans l’automate temporisé du diag-
nostiqueur la notion de transitions urgentes. La sémantique des transitions urgentes
n’a pas été spécifiée dans la définition présentée du modèle automate temporisé. Une
transition urgente est prioritaire. Elle est franchie dès que sa condition de garde est
satisfaite, sans besoin d’être synchronisée avec l’occurrence d’un événement (Barbuti
et Tesei, 2004). Dans notre modèle, une transition urgente est étiquetée par un entier
naturel qui détermine le temps de séjour maximal dans son sommet de départ, avant
qu’elle soit franchie. L’implémentation d’une telle transition revient, dans une première
étape, à définir une horloge, qu’on va désigner par y, permettant de mesurer le temps
écoulé dans chaque sommet du diagnostiqueur. En effet, cette horloge est remise à zéro
après le franchissement de chaque transition dans le diagnostiqueur. Dans une deuxième
étape, nous associons à chaque transition urgente, étiquetée par un entier τ , une garde
de la forme y = τ . Par ailleurs, nous associons au sommet de départ de cette transition
94
Chapitre 4. Diagnostic des systèmes temporisés
[Link] Pré-requis
• Nous définissons l’opérateur de propagation des étiquettes de diagnostic ⊗ : Φ ×
Σ → Φ. Cet opérateur permet de déterminer l’étiquette de diagnostic associée à
un état donné
suite à l’occurrence d’un événement σ ∈ Σ.
Fi , if φ = Fi ;
φ⊗σ = Fi , if φ = N and σ ∈ Fi ;
N , if φ = N and σ ∈ /Σ . f
Nous pouvons considérer l’extension de cet opérateur pour propager une étiquette
sur une séquence d’événements. Dans ce cas, il suffit d’appliquer successivement cet
opérateur sur chaque événement de cette séquence, tout en propageant le résultat
obtenu à chaque étape.
• Nous définissons la fonction d’accessibilité non-observable UR qui permet de dé-
terminer l’ensemble d’états accessibles depuis un ensemble d’états de départ, en
franchissant toutes les séquences possibles de transitions sur des événements non
observables. Les étiquettes de diagnostic associées aux états de départ sont propa-
gées durant ce calcul d’accessibilité, en utilisant l’opérateur ⊗.
UR : 2Q×C(X)×Φ → 2Q×C(X)×Φ
s
[(qi , zi ), φi ] 7→ {[(qj , zj ), φj ] | ∃s ∈ (Σuo ×R+ )∗ , (qi , zi ) (qj , zj ) et φj =
φi ⊗ k s k}
Dans cette définition de la fonction UR, l’ensemble des états de départ est donné
sous la forme d’un ensemble de triplets {[(q1 , z1 ), φ1 ], . . . , [(qk , zk ), φk ]}. Chaque
triplet [(qi , zi ), φi ] représente un état symbolique (qi , zi ) associé avec une étiquette
de diagnostic φi .
95
Chapitre 4. Diagnostic des systèmes temporisés
terminaison de cet algorithme est garantie grâce aux hypothèses considérées sur
le modèle qui assurent l’absence de cycles de transitions non observables (voir
Remarque 2). Ainsi, l’algorithme se termine au bout d’un nombre fini d’itérations.
96
Chapitre 4. Diagnostic des systèmes temporisés
97
Chapitre 4. Diagnostic des systèmes temporisés
correspondent aux états d’ombres vérifiant les gardes des transitions sur l’événement a.
L’étape suivante consiste à créer une partition sur l’ensemble des états franchissables.
Selon la valuation d’horloges v à l’instant de l’observation de l’événement a, nous pouvons
distinguer trois cas possibles :
• si v(x) ∈ [1, 2[, l’état estimé du système correspond à {(q0 , v, N )} ;
• si v(x) ∈ [2, 3], l’état estimé du système correspond à {(q0 , v, N ), (q2 , v, F). Cette
situation correspond au cas illustré dans notre exemple. En effet, l’événement a
est observé après 2.6 u.t., les états estimés à cet instant sont : {(q0 , hx = y =
2.6i, N ), (q2 , x = y = 2.6, F) ;
• si v(x) ∈]3, 4], l’état estimé du système correspond à {(q2 , v, F)}.
A partir de cette partition sur l’ensemble des états franchissables, nous pouvons
construire trois sommets successeurs. Dans la figure 4.15, un seul sommet successeur
est illustré. Ce sommet est obtenu en calculant les successeurs discrets de l’ensemble
d’états {(q0 , hy = x ∈ [2, 3]i, N ), (q2 , hy = x ∈ [2, 3]i, F). Ainsi, nous obtenons le sommet
({(q1 , N ), (q3 , F)}, hx ∈ [2, 3] ∧ y = 0i).
Dans la suite, nous exposons l’ossature de l’algorithme de synthèse du diagnos-
tiqueur d’une manière plus détaillée. Dans ce pseudo-code, nous désignons par q d
le sommet en cours d’élaboration (recherche de ses sommets successeurs) et SOM-
METS_A_TRAITER l’ensemble des sommets qui restent à traiter. Cet ensemble est
une structure de type file d’attente (FIFO). Par ailleurs, SOMMETS_TRAITÉS désigne
l’ensemble des sommets du diagnostiqueur qui ont déjà été traités. Nous rappelons que le
sommet initial q0d = {{(q0 , N )}, z0 } du diagnostiqueur est constitué par le sommet initial
98
Chapitre 4. Diagnostic des systèmes temporisés
1. initialisations :
{
(a) créer le sommet initial q0d ← {{(q0 , N )}, z0 },
(b) ajouter q0d à SOMMETS_A_TRAITER
(c) SOMMETS_TRAITÉS ← {},
}
99
Chapitre 4. Diagnostic des systèmes temporisés
iii. répéter pour chaque zone d’horloges η décrivant les valuations d’un sous-
ensemble d’états franchissables de la partition :
• créer un sommet du diagnostiqueur q̃ d , contenant les successeurs dis-
crets sur σ du sous-ensemble considéré de la partition d’états franchis-
sables.
• créer une transition de q d à q̃ d ayant comme une contrainte de garde le
prédicat η.
• ajouter q̃ d à SOMMETS_A_TRAITER s’il n’a pas été encore visité ;
i.e., q̃ d ∈SOMMETS_TRAITÉS.
/
}
}
Afin de mieux illustrer les différentes étapes de ce pseudo-code, nous allons construire
dans l’exemple suivant, le diagnostiqueur correspondant à l’automate temporisé de la
figure 4.17.
Exemple 4.4.4
Dans la figure 4.17, nous présentons une partie d’un automate temporisé
dont on désire construire le diagnostiqueur. Il est clair que cette partie vérifie
les hypothèses nécessaires pour l’application de l’algorithme de synthèse du
diagnostiqueur. Les événements a et b sont observables tandis que f constitue
le seul événement de défaut. Ainsi, nous aurons un seul mode de défauts,
F1 = {f }. Par ailleurs, les sommets de ce modèle sont non-finaux, auxquels
nous associons la condition d’invariant hx ≤ 20 ∧ y ≤ 20i, où 20 est une
valeur arbitrairement choisie.
La construction du diagnostiqueur se déroule comme suit :
• créer du sommet initial ({(1, N )}, hx = y = 0i),
• à partir du sommet initial, [(1, hx = y = 0i), N ], appliquer la fonction
d’accessibilité non-observable afin de déterminer les états d’ombre. On
100
Chapitre 4. Diagnostic des systèmes temporisés
a, x ≤ 10, y := 0 b, x ≥ 12
R
1 - 2 - 3 - ...
f, x ≥ 3
?
4 - 5 - 6 - ...
a, x ≤ 7, y := 0 b, y ≤ 4
101
Chapitre 4. Diagnostic des systèmes temporisés
Fig. 4.18 – Exemple de construction d’un diagnostiqueur : zones disjointes des états
franchissables.
102
Chapitre 4. Diagnostic des systèmes temporisés
sur les états franchissables admettent les mêmes ensembles de réinitialisation d’horloges
puisque le modèle du système vérifie la propriété 1.
4.5 Diagnosticabilité
Nous avons présenté dans la première partie de notre démarche de diagnostic les
concepts liés à la synthèse et l’utilisation du diagnostiqueur. Cependant, une question
importante s’impose par rapport au déploiement du diagnostiqueur : est-il capable d’iden-
tifier l’occurrence de tout défaut affectant le système au bout d’un délai fini ?
Afin de répondre à cette question, nous allons étudier la notion de diagnosticabilité
des systèmes temporisés. Nous allons établir qu’un diagnostiqueur conçu à partir d’un
modèle automate temporisé non diagnosticable peut aboutir à des situations ambiguës,
où il ne réussit pas à identifier l’occurrence d’un défaut. Dans un tel cas, le comportement
observable du système fait évoluer l’automate du diagnostiqueur vers un ensemble de
sommets Fi -incertain où aucune décision sur l’occurrence du défaut ne peut être prise.
Dans cette section, nous commençons par définir la notion de diagnosticabilité d’un
langage temporisé, étant donnée une partition sur l’ensemble des défauts. Ensuite, nous
présentons une méthode systématique permettant de vérifier la diagnosticabilité d’un
langage accepté par un automate temporisé soumis aux hypothèses considérées dans
notre travail. Enfin, nous présentons un théorème permettant de lier la notion de diag-
nosticabilité avec l’application de la méthode de vérification proposée.
103
Chapitre 4. Diagnostic des systèmes temporisés
104
Chapitre 4. Diagnostic des systèmes temporisés
Exemple 4.5.1
Nous présentons dans la suite quelques exemples de traces valides et non
valides.
• la trace "ω = 5, a, 6, b, 3.1, c" est une trace valide. Cette trace est équi-
valente à "ω = (a, 5)(b, 6)(c, 3.1)" selon la notation utilisée dans les parties
précédentes ;
• la trace "ω = 5, a, 6, b, 3.1, 5, c" n’est pas une trace valide. En effet, on ne
doit pas avoir deux délais successifs, suivis par un événement. Une notation
valide de cette trace pourra être "ω = 5, a, 6, b, 8.1, c" ;
• la trace "ω = 5, a, 6, b, 6.5, c, 1, 1, 1, 1, 1 . . . " est une trace valide. Elle per-
met de représenter l’écoulement infini du temps après l’occurrence de l’évé-
nement c. Il faut noter que cette trace ne peut être représentée en utilisant
la notation basée sur une séquence de couples (événement,délai).
Nous notons par PΣo l’opérateur permettant de projeter une trace temporisée sur
l’ensemble des événements observables. Pour une meilleure lisibilité, nous pouvons sim-
plement noter cet opérateur par P . Nous donnons dans la suite quelques exemples de
projections observables de traces temporisées. Nous considérons que les événements a, b
et c sont les uniques événements observables.
Exemple 4.5.2
• pour "ω = 2, a, 2, u, 6.6, b, 2.1, f, 2, c", "P (ω) = 2, a, 8.6, b, 4.1, c" ;
• pour "ω = 2, a, 3, f, 6, b, 1, 1, 1, . . . ", "P (ω) = 2, a, 9, b, 1, 1, 1, . . . ".
105
Chapitre 4. Diagnostic des systèmes temporisés
Exemple 4.5.3
Nous considérons dans cet exemple un ensemble d’événements Σ =
{a, b, c, f1 , f2 } et une partition de défauts Σf = F1 ∪ F2 , où F1 =
{f1 } et F2 = {f2 }. Par ailleurs, nous considérons les traces tempo-
risées "ω = 4, a, 6, b, 1, f1 , 3, c" ; "ω 0 = 1, a, 2, f2 , 6, b, 4, c" et "ω 00 =
1, a, 5, f2 , 7, b, 9, c, 1, 1, . . . " :
• il est clair que ω ∈ L1 et ω 0 ∈ L2 ;
• pour ∆ = 10, nous avons ω 0 ∈ L∆ 2 et ω ∈/ L∆
1 ;
0 ∆ ∆
• pour ∆ = 2, nous avons ω ∈ L2 et ω ∈ L1 ;
• pour tout ∆ ≥ 0, nous avons ω 00 ∈ L∆ 2 .
Dans ce qui suit, nous présentons une définition formelle pour la diagnosticabilité
d’un langage temporisé.
Définition 28. Soit L un langage temporisé à temps-divergent. Le langage L est dit
diagnosticable par rapport à une partition de m modes de défauts, Σf = F1 ∪ · · · ∪ Fm ,
si :
Exemple 4.5.4
Dans cet exemple, nous étudions la diagnosticabilité du language temporisé
106
Chapitre 4. Diagnostic des systèmes temporisés
107
Chapitre 4. Diagnostic des systèmes temporisés
108
Chapitre 4. Diagnostic des systèmes temporisés
Exemple 4.5.5
L’automate temporisé de la figure 4.21(b) représente l’automate symbolique
compagnon du diagnostiqueur décrit dans la figure 4.21(a).
109
Chapitre 4. Diagnostic des systèmes temporisés
Ce lemme établit une équivalence entre le langage accepté par l’automate temporisé A
du système et les langages acceptés par le diagnostiqueur D et son automate symbolique
compagnon S. Ce lemme découle de la construction des modèles du diagnostiqueur et
son automate compagnon. Il permet d’un coté de traduire l’équivalence entre le langage
accepté par le modèle du système et celui accepté par l’automate compagnon, et d’un
autre coté entre le langage accepté par le diagnostiqueur et la projection observable du
langage accepté par son compagnon d’un autre.
Dans la suite, nous proposons un lemme qui découle de la construction du diag-
nostiqueur. Ce lemme établit que, pour chaque paire d’états d’entrée appartenant à un
sommet du diagnostiqueur et ayant la même valuation d’horloges, il existe une paire de
traces temporisées ayant la même projection observable et faisant évoluer l’automate
temporisé du système vers ces deux états.
110
Chapitre 4. Diagnostic des systèmes temporisés
• ω ∈ Li et ω̃ ∈ L − Li .
Nous présentons dans cette partie les conditions permettant de garantir la diagnosti-
cabilité du (langage accepté par le) modèle considéré dans notre travail. Ces conditions
sont vérifiées sur la structure du diagnostiqueur et son automate symbolique compagnon.
D’abord, nous définissons quelques notions nécessaires pour caractériser les conditions
de diagnosticabilité. Ensuite, nous détaillons ces conditions. Enfin, un théorème liant
formellement la vérification de ces conditions et la définition du diagnosticabilité est
formalisé.
111
Chapitre 4. Diagnostic des systèmes temporisés
ce cycle sont inclus dans les sommets du cycle du diagnostiqueur. Ce cycle est
appelé cycle Fi -sûr, noté Ci .
Exemple 4.5.6
Le diagnostiqueur du système de chauffage de liquides présenté dans la fi-
gure 4.13 ne comporte pas de cycles de sommets Fi -incertain. En effet, le
modèle du système, à partir duquel le diagnostiqueur a été construit, est
diagnosticable. Nous proposons dans la suite d’introduire des modifications
sur le modèle de la figure 4.12. Le modèle obtenu est présenté dans la fi-
gure 4.22. Dans la nouvelle version du modèle, nous pouvons remarquer que
vide,15≤x≤22,x:=0
la transition (évac & fuite) −−−−−−−−−−−→ (rempl & fuite) admet une
condition de garde différente que celle définie dans le modèle original.
Nous constatons que l’introduction de cette simple modification rend
ce modèle non diagnosticable. En effet, nous pouvons remarquer à par-
tir du modèle du diagnostiqueur et de son automate symbolique compa-
gnon, représentés respectivement dans les figures 4.23 et 4.24, l’existence
d’un cycle F1 -incertain. Si nous considérons une exécution du diagnostiqueur
sur la trace d’événements observables ((rempli, 45)(évacuer, 60)(vide, 21))∗ ,
deux trajectoires peuvent exister dans ce cas expliquant la trace ob-
112
Chapitre 4. Diagnostic des systèmes temporisés
blocage_V1 , x ≤ 50
?
remplissage f uite, x ≤ 50
- rempl & fuite
vanne bloquée
x ≤ 60 x ≤ 60
rempli,40 ≤ x ≤ 50 vide, 20 ≤ x ≤ 25 vide, 15 ≤ x ≤ 22
x := 0
I x := 0
I
rempli,40 ≤ x ≤ 50 x := 0
x := 0
chauffage évacuation chauf & fuite évac & fuite
x ≤ 60
- x ≤ 60 -
x ≤ 60 x ≤ 60
évacuer,x = 60 évacuer,x = 60
x := 0 x := 0
?
51
vanne bloquée,F2 remplissage,N
x ≥ 51 - x=0
6 rempli,40 ≤ x ≤ 50,x := 0
?
chauffage,N
chauf & fuite,F1
x=0
évacuer,x = 60, x := 0
?
évacuation,N - rempl & fuite,F1
évac & fuite,F1
vide, 15 ≤ x < 20, x := 0 x=0
x=0
vide, 22 < x ≤ 25, x := 0 rempli,40 ≤ x ≤ 50,x := 0
vide, 20 ≤ x ≤ 22, x := 0 ?
?
remp & fuite,F1 chauf & fuite,F1
remplissage,N x=0 vide, 15 ≤ x ≤ 22, x := 0
x=0 rempli,x ∈ [40, 50],x := 0
51
évacuer,x = 60, x := 0
?
évac & fuite,F1
x=0
Cycle F1 -indéterminé
113
Chapitre 4. Diagnostic des systèmes temporisés
Cycle F1 -défaillant C1
Cycle F1 -sûr (C1 )
blocage_V1 , x ≤ 50 ?
(vanne bloquée,F2 f uite, x ≤ 50
(remplissage,N ,hx = 0i) -
htruei) - (rempl & fuite,F1 ,
-
h0 ≤ x ≤ 60)
? ?
(évacuation,N ,hx = 0i)
(évac & fuite,F1 ,hx = 0i)
vide, 20 ≤ x ≤ 22, x := 0
vide, 20 ≤ x ≤ 22, x := 0
Afin de prouver ce théorème, nous commençons par présenter deux lemmes établissant
quelques propriétés sur les cycles Fi -indéterminé. Nous prouvons que, étant donné un
cycle Fi -indéterminé dans le diagnostiqueur, il existe pour tout entier α ≥ 0, une paire de
traces appartenant au langage L et ayant la même projection observable, où l’exécution
de S sur la première trace le fait évoluer α fois dans le cycle Ci , et l’exécution de S
sur la deuxième trace le fait évoluer dans le cycle Ci . Afin de prouver l’existence de
ces deux traces, nous introduisons un premier lemme qui permet la construction d’une
partie de ces traces en raisonnant sur chaque sommet et son prédécesseur dans le cycle
Fi -indéterminé . Ensuite, le résultat de ce premier lemme sera utilisé dans le second pour
la construction de la paire de traces parcourant les cycles Ci et Ci .
d
Lemme 5. Soit qn+1 un sommet appartenant à un cycle Fi -indéterminé et soient
d
(qn+1 , Fi ), (q̃n+1 , φ̃n+1 ) ∈ Dis(qn+1 ), tels que φ̃n+1 6= Fi , (qn+1 , Fi , zn+1 ) ∈ Ci et
d
(q̃n+1 , φ̃n+1 , zn+1 ) ∈ Ci , où zn+1 = Z(qn+1 ). Nous notons par qnd le prédécesseur de
d σn+1 ,gn+1 ,Yn+1
qn+1 dans le cycle Fi -indéterminé, sur la transition qnd −−−−−−−−−→ qn+1 d
∈ E d . Alors,
pour toute valuation vn+1 ∈ zn+1 , il existe une valuation vn ∈ zn = Z(qnd ), une paire
d’éléments (qn , Fi ), (q̃n , φ̃n ) ∈ Dis(qnd ) et une paire de traces temporisées ωn+1 et ω̃n+1 ,
telles que :
• (qn , Fi , zn ) ∈ Ci et (q̃n , φ̃n , zn ) ∈ Ci ;
ωn+1 ω̃n+1
• (qn , vn ) (qn+1 , vn+1 ) et (qn , vn ) (qn+1 , vn+1 ) ;
• P (ωn+1 ) = P (ω̃n+1 ) = "d.σn+1 ", où d ∈ R+ .
114
Chapitre 4. Diagnostic des systèmes temporisés
0
Alors, étant donné un entier naturel α ≥ 0 et ∀vn,p ∈ zn , il existe une valuation
d’horloges vn,p ∈ zn et une paire de traces temporisées ω , ω̃ α telles que :
α α
ωα
α
1. L’exécution (qnp , vn,p ) 0
(qnp , vn,p ) fait évoluer S α fois dans le cycle Ci ,
0 ω̃ α
2. L’exécution (q̃nq , vn,p
α
) (q̃nq , vn,p
0
) fait évoluer S dans le cycle Ci ,
3. P (ω α ) = P (ω̃ α ).
Preuve du théorème : 1
Nécessité :
Nous prouvons la nécessité par contradiction. Deux cas seront étudiés :
Premier cas : le diagnostiqueur contient un sommet Fi -incertain et final q d ∈ Qfd .
Alors, ∃(q, Fi ), (q̃, φ̃) ∈ Dis(q d ), i ∈ {1, . . . , m} and φ̃ 6= Fi , and q, q̃ ∈ Qf .
D’après le lemme 3, ∀v ∈ Z(q d ), il existe une paire de traces temporisées : ω et ω̃,
telle que :
• P (ω) = P (ω̃),
ω ω̃
• (q0 , v0 ) (q, v) et (q0 , v0 ) (q̃, v).
• ω ∈ Li et ω̃ ∈ L − Li .
Nous désignons par tf la date de la première occurrence d’un défaut de l’ensemble
Fi dans ω. Puisque les sommets q et q̃ sont finaux ; i.e., les invariants sur les sommets
sont non bornés (égales à vrai), alors chaque exécution atteignant ces sommets vont
y séjourner indéfiniment sans pouvoir évoluer vers un d’autres sommets. Alors, étant
données deux valeurs ∆ ∈ R+ et d > tf + ∆, il existe deux traces ωe , ω̃e ∈ L telles
que ωe ="ω.d", ω̃e = "ω̃.d". Puisque P (ωe ) = P (ω̃e ), ωe ∈ Li et ω̃e ∈ L − Li , nous
concluons que notre hypothèse de départ est contredite et par conséquent L n’est pas
diagnosticable.
Second cas : il existe un cycle Fi -indéterminé dans D. En effet, il existe un cycle
de sommets Fi -incertain dans D, auquel correspond un cycle Fi -défaillant ; i.e., Ci , et un
cycle Fi -sûr ; i.e., Ci , dans l’automate S.
Puisque l’automate temporisé A est fortement non-zeno, alors chaque exécution cy-
clique admet une durée d’exécution supérieure à une valeur δ > 0. Puisque chaque cycle
dans l’automate temporisé S correspond à au moins un cycle dans A, alors la durée écou-
lée par chaque exécution évoluant dans le cycle Ci est supérieure à δ u.t.. Nous désignons
par ∆ une valeur arbitrairement large et α = b∆/δc + 1.
Soit qkd un élément du cycle Fi -indéterminé. Puisque qkd is Fi -incertain, alors il existe
(qk , Fi ) et (q̃k , φ̃k 6= Fi ) ∈ Dis(q d ), tels que (qk , Fi , Z(qkd )) ∈ Ci et (q̃k , φ̃k , 6= Fi , Z(qkd )) ∈
115
Chapitre 4. Diagnostic des systèmes temporisés
Ci . Soit vk0 une valuation dans Z(qkd ). D’après le lemme 6, il existe une valuation d’horloges
vkα ∈ Z(qkd ) et une paire de traces temporisées ω α , ω̃ α , telles que :
ωα
1. l’exécution (qk , vkα ) (qk , vk0 ) fait évoluer S α fois dans le cycle Ci ,
ω̃ α
2. l’exécution (q̃k , vkα ) (q̃k0 , vk0 ) fait évoluer S dans le cycle Ci ,
3. P (ω α ) = P (ω̃ α ).
D’après le lemme 3, il existe une paire de traces ωk ∈ Li et ω̃k ∈ L − Li , telle que
ω ω̃
(q0 , v0 ) k (qk , vkα ), (q0 , v0 ) k (q̃k , vkα ) et P (ω) = P (ω̃).
Nous notons par ω et ω̃, la concaténation de respectivement, ωk et ω α , et ω̃k et ω̃ α ;
i.e., ω ="ωk .ω α " et ω̃ ="ω̃k .ω̃ α ". Il est simple d’établir que ω ∈ Li et ω̃ ∈ L − Li
(puisque le cycle Ci ne contient pas des transitions sur des défauts de l’ensemble Fi ,
sinon, l’étiquette Fi sera propagée dans tous les sommets du cycle Ci ). Puisque ∆ ≤ α.δ
et ω ∈ Lα.δ ∆
i , alors, ω ∈ Li . En considérant que P (ω) = P (ω̃), nous concluons la non
diagnosticabilité du langage L.
Preuve de la sufficance :
Considérons un diagnostiqueur D ne contenant ni un cycle Fi -indéterminé ni un sommet
final Fi -incertain. Considérons ω ∈ Li . D’après le lemme 1, l’automate du diagnostiqueur
D accepte le langage temporisé P (L), en effet, il accepte la trace temporisée P (ω). Soit
q d un sommet du diagnostiqueur, accessible par une exécution de D sur la trace P (ω).
Nous distinguons deux cas :
1. q d est Fi -certain :
D’après le lemme 4, ∀ω̃ ∈ L | P (ω) = P (ω̃) ⇒ ω̃ ∈ Li . Nous concluons que L is
diagnosticable.
2. q d est Fi -incertain :
Puisqu’il n’existe aucun cycle Fi -indéterminé et que qd ne peut être final, deux cas
sont possibles :
(a) Il n’existe aucun cycle de sommets Fi -incertain dans le diagnostiqueur D. En
plus, le diagnostiqueur séjourne dans chaque sommet Fi -incertain pour seule-
ment une durée bornée de temps vue qu’aucun sommet Fi -incertain ne peut
être aussi final. Puisque le diagnostiqueur comporte un nombre fini de som-
mets, une continuation assez longue de la trace ω ferait évoluer le diagnostieur
vers un sommet Fi -certain, après une durée finie de temps (sinon, il évolue-
rait toujours dans des cycle Fi -incertain, ce qui contradit notre hypothèse sur
l’absence de cycle de sommets Fi -incertain). Nous retrouvons ici le cas 2, et
par conséquent, L est diagnosticable.
(b) Il existe un ou plusieurs cycles de sommets Fi -incertain dans D, tels que aucun
cycle ne lui correspond les cycles Ci et Ci dans S. Nous réutilisons ici une partie
de la preuve établie dans (Sampath et al., 1995). En effet, nous prouvons qu’il
116
Chapitre 4. Diagnostic des systèmes temporisés
Nous présentons dans cette section un aperçu sur quelques outils développés dans la
littérature, permettant l’implémentation de notre algorithme de construction du diagnos-
tiqueur. Ensuite, nous présentons une étude de la complexité des algorithmes employés
par notre approche de diagnostic.
117
Chapitre 4. Diagnostic des systèmes temporisés
l’analyse des automates temporisés (Alur, 1999). Les opérations nécessaires à l’analyse
en avant ont été développées sur la base de DBM (Bengtsson et Yi., 2004). Afin d’avoir
une représentation plus compacte des zones non-convexes, plusieurs améliorations ont été
introduites sur cette structure de donnée telle que l’utilisation des CDD "Clock Difference
Diagrams" (Pearson et al., 1998). Cette structure de donnée peut être envisagée pour
l’implémentation de notre algorithme de synthèse du diagnostiqueur.
118
Chapitre 4. Diagnostic des systèmes temporisés
4.7 Conclusion
119
Chapitre 4. Diagnostic des systèmes temporisés
120
Chapitre 5
5.1 Introduction
Les systèmes de production complexes peuvent être vus comme des systèmes dyna-
miques hybrides ayant des dynamiques continues et divers aspects discrets. L’utilisation
d’une approche de diagnostic reposant sur une abstraction des dynamiques continues
d’un SDH, à travers l’utilisation de modèles SED, entraîne une perte considérable d’in-
formations, parfois indispensables pour l’identification des défauts. Ainsi, dans certains
cas, les comportements défaillants se manifestent par une déviation des trajectoires des
dynamiques continues du système. Ceci rend l’utilisation d’une démarche de diagnostic
fondée sur une abstraction purement discrète de l’évolution du système, inadéquate pour
l’identification des défauts.
Afin de pallier à ce problème, nous avons proposé dans le chapitre précédent, une
démarche de diagnostic qui prend en considération l’aspect temporel dans l’évolution du
SED à diagnostiquer. Cette approche repose sur l’utilisation d’un modèle complet du
système sous la forme d’un automate temporisé. Ce modèle décrit l’évolution temporelle
des événements du système à travers l’utilisation d’un ensemble d’horloges. Ces variables
fictives permettent d’abstraire les intéractions entre les dynamiques continues (les
variables) et les dynamiques discrètes (les événements) d’un système, en utilisant un
ensemble de contraintes temporelles conditionnant les évolutions discrètes. Par exemple,
nous supposons qu’un capteur de niveau génère l’événement plein lorsque le niveau du
liquide dans un bac, qu’on modélise avec une variable x, atteint une valeur seuil x = 200,
sachant que le remplissage s’effectue avec une dynamique ẋ ∈ [4, 5] à partir du niveau
initial x = 0. Cette évolution du système peut être modélisé à travers l’utilisation d’une
horloge fictive y qui mesure le temps écoulé à partir du début de la phase de remplissage,
121
Chapitre 5. Diagnostic des systèmes hybrides rectangulaires
et en associant la contrainte y ∈ [40, 50] à la transition sur l’événement plein. Dans cet
exemple, l’utilisation de l’horloge y permet d’abstraire la variable continue x.
Une telle abstraction des dynamiques continues à travers l’utilisation de contraintes
sur des horloges n’est pas simple à réaliser surtout lorsqu’il s’agit d’un système complexe
comportant plusieurs variables continues. Dans certains cas, cette abstraction n’est même
pas possible puisque les modèles hybrides sont strictement plus expressifs que les modèles
SED temporisés (Henzinger et al., 1998).
Ainsi, il serait plus convenable d’utiliser un modèle concis des systèmes réels qui
décrit intrinsèquement l’interaction entre son aspect continu et son aspect discret, tel
que le modèle automate hybride. Le modèle automate hybride représente un outil puis-
sant permettant la modélisation et l’analyse des SDH. Cet outil bénéficie d’une grande
flexibilité et d’une puissante expressivité (Henzinger, 1996). Toutefois, l’utilisation de
ce modèle est confrontée à l’indécidabilité de certains problèmes fondamentaux tel que
l’analyse d’accessibilité et le problème de déterminisation.
C’est dans ce cadre que nous présentons notre démarche de diagnostic pour une sous-
classe de SDH. Notre approche repose sur la modélisation du comportement complet du
système à travers une sous-classe simple d’automates hybrides : les automates hybrides
rectangulaires, sous certaines conditions. Ce formalisme permet d’approximer les com-
portements de la dynamique continue du système à travers l’utilisation de conditions de
flux rectangulaires de la forme ẋ ∈ [a, b]. Dans ce chapitre, nous introduisons d’abord
le modèle automate hybride rectangulaire. Ensuite, nous présentons une procédure de
diagnostic qui représente le cœur de notre démarche de diagnostic pour les SDH. Nous dé-
finissons une notion de diagnosticabilité, dite diagnosticabilité à horizon de temps limité,
pour les langages temporisés acceptés par les automates rectangulaires hybrides considé-
rés dans notre contribution. Enfin, une méthode systématique permettant la vérification
de cette notion est décrite.
Nous présentons dans cette partie le modèle Automate Hybride Rectangulaire (AHR),
qui constitue le cadre de modélisation de l’approche de diagnostic que nous désirons
développer dans ce chapitre. Ce modèle peut être considéré comme une généralisation
du modèle automate temporisé, où l’évolution continue n’est plus représentée par des
horloges mais par des équations différentielles sur les variables continues du système.
Dans la suite de cette section, nous présentons formellement le modèle automate
hybride rectangulaire, en rappelant les aspects syntaxique et sémantique de ce modèle.
Ensuite, nous introduisons une méthode permettant l’analyse comportemenentale d’un
SDH modélisé par un AHR. Cette méthode repose sur l’application d’une fonction d’ana-
122
Chapitre 5. Diagnostic des systèmes hybrides rectangulaires
5.2.1 Syntaxe
Définition 30.
Définition 31. Une valuation sur X est un vecteur de Rn , v = (v1 , . . . , vn ), qui définit
une valeur vi ∈ R pour chaque variable xi ∈ X.
Définition 32. Une region sur l’ensemble X est un sous-ensemble de Rn . Pour chaque
région z et xi ∈ X, z(xi ) = {vi ∈ R | v ∈ z}. Nous notons par [[ψ]] la région composée
par l’ensemble des vecteurs v ∈ Rn , où le prédicat ψ est vrai si on remplace xi par la
valeur correspondante vi , pour chaque i ∈ {1, . . . , n}.
En l’absence de toute ambiguïté, nous pouvons désigner une région [[ψ]] par l’ex-
pression du prédicat correspondant ψ. Pour un prédicat rectangulaire ψ et une variable
xi , nous désignons par [[ψ]](xi ) l’intervalle de valeurs décrit par les ième composants des
vecteurs vérifiant v ∈ [[ψ]].
123
Chapitre 5. Diagnostic des systèmes hybrides rectangulaires
Dans la suite de notre travail, nous considérons uniquement les AHRs ayant un non-
déterminisme borné. Par ailleurs, nous supposons que pour chaque sommet q et chaque
variable xi ∈ X, les bornes de l’intervalle [[f lux(q)]](ẋi ) doivent être des valeurs entières,
en plus, [[f lux(q)]](ẋi ) ⊂ (−∞, 0] ou [[f lux(q)]](ẋi ) ⊂ [0, +∞).
Exemple 5.2.1
La figure 5.1 illustre l’exemple d’un automate hybride rectangulaire initia-
lisé. Nous pouvons constater que ce modèle comporte trois états discrets et
deux variables x1 et x2 . Par ailleurs, chacune de ces variables est réinitialisée
lorsqu’elle change de flux entre deux sommets. La condition initiale de ce
sommet correspond à la région hx1 = 0 ∧ x2 = 0i.
124
Chapitre 5. Diagnostic des systèmes hybrides rectangulaires
x1 = 0 ∧ x2 = 0
w x1 ≥ 0 x1 ≤ 30 x1 ≥ 0
1 ∧x2 ≤ 60 2 ∧x2 ≥ 0 3
∧x2 ≥ 0
a, x2 ≤ 60, [x1 := 20] b, x1 = 30, [x2 := 90]
ẋ1 = 1 - ẋ1 ∈ [2, 4] - ẋ1 ∈ [2, 4]
ẋ2 = 3 ẋ2 = 3 ẋ2 = 5
5.2.2 Sémantique
A chaque instant, l’état d’un automate hybride rectangulaire est donné par une paire
(q, v) correspondant à l’association d’un état discret du système q et d’un vecteur v ∈ Rn
indiquant la valeur courante de chaque variable.
Nous présentons la sémantique d’un automate hybride rectangulaire H, en terme de
tous les comportements qui peuvent être générés par l’évolution du système modélisé.
Dans ce sens, la sémantique d’un système continu, définie par un ensemble d’équations
différentielles, est donnée par l’ensemble de toutes ses solutions, notamment de toutes
ses trajectoires.
L’évolution d’un modèle automate rectangulaire hybride est réalisée selon deux types
de transitions :
• transitions continues (figure 5.2-a) : la partie discrète de l’état reste constante
dans le même sommet q, tandis que la partie continue évolue de la valuation v
à la valuation v0 . Cette évolution se fait via une trajectoire continue, décrite par
les dynamiques des variables évoluant dans des intervalles de flux spécifiés par
f lux(q), tout en respectant les contraintes d’invariants décrites par inv(q). Cette
125
Chapitre 5. Diagnostic des systèmes hybrides rectangulaires
δ
− (q, v0 ), où δ ∈ R+ désigne le temps écoulé durant
transition est notée par (q, v) →
la transition ;
• transitions discrètes (figure 5.2-b) : correspondent aux changements discrets et
instantanés de sommets comme décrit par le quintuplet e = (q, σ, g, r, R, q 0 ) ∈ E.
e
− (q 0 , v0 ). Une transition ne peut être franchie
Cette transition est notée par (q, v) →
que si le prédicat de la garde est satisfait par la partie continue de l’état : v ∈ [[g]].
Dans ce cas, la partie discrète change du sommet q au sommet q 0 et la partie
continue est mise à jour selon l’ensemble des affectations de variables.
inv(q)
(q, v)
q q0
(q 0 , v 0 )
j
(q, v 0 ) (q, v) e
-
(b)
(a)
Ainsi, le système passe du temps dans chaque état discret, permettant ainsi aux
variables continues d’évoluer et effectue des transitions discrètes entre ces états. La dy-
namique associée aux variables continues est spécifiée par la fonction de flux. Le fran-
chissement d’une transition discrète est synchronisé avec l’occurrence d’un événement.
La valuation des variables dans X lors de ce franchissement doit vérifier la condition de
garde définie. Une transition est dite autonome, si elle est franchie dès que sa condition
de garde est vérifiée. Dans notre travail, la syntaxe définissant un AHR ne considère pas
les transitions autonomes. Par contre, nous pouvons avoir des transitions équivalentes
en définissant des transitions sur des événements non observables et des conditions des
gardes et d’invariants bien déterminées.
Définition 37.
• Une exécution d’un AHR H est une séquence finie ou infinie de transitions continues
et/ou discrètes (q0 , v0 ) →
− (q1 , v1 ) →
− (q2 , v2 ) →
− . . . , où (q0 , v0 ) ∈ init.
• Un état (q, v) est dit accessible (ou atteignable), s’il existe une exécution de H qui
rejoint cet état à partir d’un état initial (q0 , v0 ) ∈ init.
126
Chapitre 5. Diagnostic des systèmes hybrides rectangulaires
sont des éléments de Σ et δi ∈ R+ , correspond au temps écoulé entre les occurrences des
événements successifs σi et σi+1 .
Une trace temporisée ω est dite acceptée par un AHR H, s’il existe une exécution de
H étiquetée avec les éléments de ω. L’opérateur temps(ω) renvoie la durée d’une trace
temporisée ω.
Définition 38. Un AHR H est dit Fortement Non-Zénon (FNZ) (Roux et Rusu, 1996),
s’il existe un entier naturel d > 0, pour lequel chaque exécution inscrite dans un cycle de
transitions de H admet une durée supérieure à d. Nous pouvons facilement établir que
les conditions suivantes garantissent le fait qu’un automate temporisé H est fortement
non-zénon :
e 1 e
2 ek−1 e k
pour chaque cycle de transitions dans H, q1 − → q2 −
→ . . . −−→ qk − → q1 :
• il existe au moins une variable x ∈ X, telle que ẋ admet une borne inférieure stric-
tement positive dans tous les sommets du cycle, ou ẋ admet une borne supérieure
strictement négative dans tous les sommets du cycle ;
• il existe deux transitions e, e0 dans ce cycle, où x n’est pas réinitialisée dans les
transitions entre e et e0 , et deux entiers c, c0 ∈ Z, avec c < c0 , tels que :
– si ẋ est strictement positive alors la variable x est réinitialisée à c dans e et
admet comme borne inférieure c0 ; i.e., x ≥ c0 , dans la condition de garde de e0 .
– si ẋ est strictement négative alors x est réinitialisée à c0 dans e et admet comme
borne supérieure c ; i.e., x ≤ c, dans la condition de garde de e0 .
Dans un AHR fortement non-zénon, les traces infinies sont nécessairement à temps-
divergent comme il est le cas pour les automates temporisés. En effet, après le parcours de
chaque cycle de transitions, le temps d’une exécution de l’AHR progresse uniformément
avec une durée minimale, supérieure à d u.t..
Exemple 5.2.2
La figure 5.3 présente un exemple d’automate hybride rectangulaire fortement
non-zénon. Nous pouvons constater que la variable x1 garde une dynamique
strictement positive dans tous les états discrets de l’automate. En plus cette
variable est réinitialisée à 0, dans la transition entre les sommets 3 et 1,
et admet comme borne inférieure la valeur 30 dans la contrainte de garde
de la transition entre les sommets 2 et 3. Ainsi, dans chaque exécution de
l’automate, parcourant ce cycle de sommets, s’écoule une durée de temps
supérieure à 15 u.t..
127
Chapitre 5. Diagnostic des systèmes hybrides rectangulaires
x1 = 0 ∧ x2 = 0
w
1 x2 ≤ 60 2 x1 ≤ 30 3 x2 ≥ 0
a, x2 ≤ 60 b, x1 = 30
ẋ1 = 1 - ẋ1 = 2 - ẋ1 ∈ [2, 4]
ẋ2 ∈ [3, 6] ẋ2 = 3 ẋ2 = −5
6 c, x2 = 0, [x1 := 0]
Preuve :
1) Immédiate d’après la définition d’un AHR initialisé.
2) Chaque cycle de transitions dans l’AHR H correspond à un cycle dans H1 ou
H2 , ou la synchronisation de deux cycles, le premier dans H1 et le second dans H2 . Par
conséquent, dans chaque exécution inscrite dans un cycle de H s’écoule une durée de
temps supérieure à d > 0, qui correspond à la durée d’exécution d’un cycle dans H1
et/ou dans H2 .
128
Chapitre 5. Diagnostic des systèmes hybrides rectangulaires
par (qm , zm ).
Les successeurs d’un état symbolique sont calculés itérativement, en alternant le
calcul de successeurs continus et discrets (Roux et Rusu, 1996) (figure 5.4).
q1 q2 q3
e1 e2
- z1 - z2 - z3 -
Le calcul du successeur continu d’un état symbolique (q, z) est réalisé en utilisant
l’opérateur P ostc , défini de la manière suivante :
δ
P ostc ((q, z)) = {(q, v0 )|(q, v) →
− (q, v0 ), v ∈ z, δ ∈ R+ }.
Pratiquement, le calcul d’une région (q 0 , z 0 ), successeur d’une région (q, z) sur une
transition e = (q, σ, g, r, R, q 0 ), est effectué en appliquant les étapes suivantes (Guéguen
et Zaytoon, 2004) :
1. calculer z1 qui correspond à l’intersection de l’invariant du sommet q ; i.e., inv(q),
et le futur de la région z. Le futur d’une région correspond à l’ensemble des états
accessibles à partir de la région de départ en appliquant la fonction de flux (voir
l’exemple dans la figure 5.5) ;
2. calculer z2 qui correspond à l’intersection de z1 avec la condition de garde g ;
3. calculer z3 en appliquant la fonction de réinitialisation définie par R et r sur la
région z2 ;
4. calculer z4 qui correspond à l’intersection de la région z3 et l’invariant du sommet
q 0 ; i.e., inv(q 0 ) ;
129
Chapitre 5. Diagnostic des systèmes hybrides rectangulaires
Fig. 5.5 – Futur d’un polyhèdre hx ∈ [1, 3] ∧ y ∈ [0, 2]i sur une fonction de flux hẋ =
1 ∧ ẏ ∈ [1, 3]i
Cet algorithme de calcul d’accessibilité peut ne pas converger lorsqu’il est appliqué
sur un automate hybride linéaire sans restrictions. D’un point de vue théorique cette
130
Chapitre 5. Diagnostic des systèmes hybrides rectangulaires
non convergence s’explique par le fait que le problème d’analyse d’accessibilité d’un tel
automate est non-décidable (Alur et al., 1995) ; i.e, il n’est pas possible de trouver un
algorithme qui réalise ce calcul et dont la convergence est assurée en un temps fini.
Cependant, des cas particuliers (sous-classes d’automates hybrides linéaires) de
convergence de cet algorithme ont été identifiés dans la littérature, il s’agit du mo-
dèle automate hybride rectangulaire initialisé. En effet, il a été prouvé dans (Henzinger
et al., 1998) que l’analyse d’accessibilité pour ce modèle est décidable et que l’algorithme
d’accessibilité en avant admet une complexité PSPACE.
Les modèles des systèmes hybrides se distinguent par leur grande expressivité, leur
capacité à représenter intrinsèquement les interactions entre les dynamiques continues
et discrètes d’un système. Toutefois, le développement d’applications à partir de ces mo-
dèles, telles que la synthèse de superviseurs, de diagnostiqueur ou le model-checking peut
se confronter aux résultats d’indécidabilités liés à la plupart des problèmes standards :
vérification du vide, universalité, analyse d’accessibilité, déterminisation . . ., (Alur et al.,
1995). Ces indécidabilités nous conduisent à considérer des sous-classes de modèles hy-
brides, ayant des dynamiques plus simples.
En effet, dans le cadre de notre travail, nous utilisons une sous-classe des automates
hybrides rectangulaires pour modéliser le système à diagnostiquer. Malgré la simplicité
de la dynamique continue de ce modèle, il est doté d’une grande expressivité à travers
sa capacité à représenter, d’une manière approximative, la dynamique discrète et la
dynamique continue d’un SDH en utilisant des bornes inférieures et supérieures sur les
dérivées des variables continues (par exemple, ẋ ∈ [2, 5]) (Kopke, 1996).
Toutefois, le problème de synthèse hors-ligne d’un diagnostiqueur à partir d’un mo-
dèle automate hybride rectangulaire est indécidable. Ce résultat est attendu puisque
ce problème est aussi indécidable pour un cas particulier de AHR à savoir, le modèle
automate temporisé (sans restrictions).
C’est à partir de ces constatations que nous proposons une solution de diagnostic
en-ligne d’une sous-classe de SDH modélisée par des automates hybrides rectangulaires.
Dans notre solution, nous nous sommes inspirés d’un ensemble de techniques développées
dans les travaux de Tripakis (Tripakis, 2002) et Sampath (Sampath et al., 1995, 1996).
Elle repose sur l’utilisation d’une procédure de diagnostic sous la forme d’un algorithme
d’estimation d’état, exécuté en-ligne avec le système à diagnostiquer. La procédure de
diagnostic est passive dans le sens où elle n’influence pas le fonctionnement du système
à diagnostiquer.
131
Chapitre 5. Diagnostic des systèmes hybrides rectangulaires
Dans la figure 5.6, nous illustrons le schéma global de notre solution de diagnostic.
Cette solution s’appuie sur un modèle "complet" du SDH à diagnostiquer, décrivant
son comportement normal et ses possibles comportements anormaux (défaillants). Ce
modèle est donné sous la forme d’un automate hybride rectangulaire, vérifiant certaines
hypothèses. A partir de ce modèle, des événements observables générés par le système
et les délais de temps séparant ces événements, la procédure de diagnostic estime l’état
courant du système ainsi que les défauts non observables qui affectent son fonctionne-
ment. Nous notons que la procédure n’a aucune connaissance directe sur les valeurs
des variables continues. Ces valeurs seront estimées en analysant le comportement
discret observable du système. Le diagnostic des défauts est ainsi élaboré uniquement
à partir de l’analyse du comportement discret observable du système, en s’appuyant
également sur l’aspect temporel qui caractérise cette évolution.
Modèle
AHR du système
Système
- PO
compte-rendus
commandes
PC
Afin de présenter le principe de notre approche de diagnostic pour les SDH, nous
considérons, tout au long de ce chapitre, l’exemple du système de chauffage de liquides
introduit dans le chapitre 4. Dans la suite, nous décrivons ce système en considérant
l’évolution de sa dynamique continue.
Exemple 5.3.1
132
Chapitre 5. Diagnostic des systèmes hybrides rectangulaires
Par la suite, le liquide est chauffé pendant une durée de 40 u.t., mesurée par
l’horloge x2 . Le liquide est ensuite évacué à travers la vanne V2 avec un débit
ẋ1 ∈ [−8, −6] jusqu’à ce que le bac soit vide ; i.e., x1 = 0. A ce moment,
le capteur S2 génère un événement de notification, le contrôleur commence
alors un nouveau cycle de chauffage.
La figure 5.7(b) illustre un modèle automate hybride rectangulaire décri-
vant le comportement normal et les comportements défaillants de ce système.
Ce modèle ne représente que quelques aspects du fonctionnement de ce sys-
tème. En effet, pour des raisons de clarté, certains événements, jugées non
pertinents pour la compréhension de notre exemple, n’ont pas été illustrés
(comme les événements d’ouverture et de fermeture des vannes). Nous suppo-
sons que le fonctionnement de ce système peut être affecté par deux défauts
non observables :
• le premier défaut correspond à l’existence d’une fuite dans le bac. Ce
défaut est représenté par l’événement f uite ;
• le deuxième défaut correspond au blocage de la vanne V1 en position
fermée. Ce défaut est représenté par l’événement blocage_V1 .
Les événements s1 et s2 sont observables et correspondent aux notifica-
tions générées par, respectivement, par les capteurs S1 et S2 . L’événement
u est non observable. Cet événement a été introduit pour permettre la re-
présentation d’une transition autonome, franchie lorsque l’horloge x2 atteint
la valeur 40. Le système admet un ensemble d’états initiaux désigné par la
région (1, hx1 ∈ [0, 500] ∧ x2 = 0i).
7 vrai
ẋ1 = 0
ẋ2 = 1
blocage_V1 , x1 ≤ 500
6
x1 ∈ [0, 500] ∧ x2 = 0 s2 , x1 = 0, [x1 := 0]
s1 , x1 = 500, [x2 := 0; x1 := 500]
^ ?
1 x1 ≤ 500 2 x2 ≤ 40 3 x1 ≥ 0
ẋ1 ∈ [3, 5] - ẋ1 = 0 - ẋ1 ∈ [−8, −6]
V1 ẋ2 = 1 ẋ2 = 1 ẋ2 = 1
u, x2 = 40, [x2 := 40; x1 := 500]
f uite
?
4 x1 ≤ 500 5 x2 ≤ 40 6 x1 ≥ 0
S1 ẋ1 ∈ [2, 4] - ẋ1 ∈ [−2, −1]
- ẋ1 ∈ [−9, −8]
ẋ2 = 1 ẋ2 = 1 ẋ2 = 1
S2 a s1 , x1 = 500, [x2 := 0] u, x2 = 40
V2
6
s2 , x1 = 0
(a) (b)
Fig. 5.7 – Modèle automate hybride rectangulaire d’un système de chauffage de liquides
133
Chapitre 5. Diagnostic des systèmes hybrides rectangulaires
Nous présentons dans la suite les différents étapes de notre demarche de diagnostic
pour les SDH, introduite dans (Derbel et al., 2009b,a). Dans un premier lieu, nous
caractérisons les spécifications et les hypothèses retenues sur le modèle automate hybride
rectangulaire du système à diagnostiquer. En second lieu, nous présentons la procédure
de diagnostic des défauts, qui constitue la base de notre contribution.
Dans notre travail, nous avons choisi le formalisme des automates hybrides rectan-
gulaires comme un cadre de modélisation des SDH à diagnostiquer. L’application de
notre approche de diagnostic nécessite la vérification de certaines spécifications et hypo-
thèses sur le modèle du système. Les spécifications imposées permettent de caractériser
la modélisation des défauts. Certaines de ces contraintes de modélisation ont été consi-
134
Chapitre 5. Diagnostic des systèmes hybrides rectangulaires
135
Chapitre 5. Diagnostic des systèmes hybrides rectangulaires
x1 = 0
R
1 x1 ≤ 30 a, x1 = 30 2 x1 ≥ 0 b, x1 = 0 3 x1 ≤ 50 4 x1 ≥ 0
c, x1 = 50
- - -
ẋ1 = 2 ẋ1 = −2 ẋ1 = 5 ẋ1 = 0
6
f u, x1 = 10
?
5 x1 ≤ 30 a, x1 = 30 6 x1 ≥ 10
ẋ1 = 2
- ẋ1 ∈ [−4, −3]
Fig. 5.8 – Sommets accessibles par des exécutions correspondant à de différents modes
de fonctionnement
(
0, si q ∈ {1, 2, 3, 4} ;
ϕ(q) =
1, sinon.
x1 = 0
R
1 x1 ≤ 30 a, x1 = 30 2 x1 ≥ 0 b, x1 = 0 3 x1 ≤ 50 4 x1 ≥ 0
c, x1 = 50
- - -
ẋ1 = 2 ẋ1 = −2 ẋ1 = 5 ẋ1 = 0
?
5 x1 ≤ 30 a, x1 = 30 6 x1 ≥ 10 u, x1 = 10 7 x1 ≥ 0 b, x1 = 0 8 x1 ≤ 50 c, x1 = 50 9 x1 ≥ 0
- ẋ - - -
ẋ1 = 2 1 ∈ [−4, −3] ẋ1 = −2 ẋ1 = 5 ẋ1 = 0
Nous notons par H0 la restriction d’un AHR H, qui décrit son comportement normal.
Cette restriction peut être obtenue en éliminant du modèle initial H tout sommet q véri-
fiant la condition ϕ(q) 6= 0. Par ailleurs, l’élimination d’un sommet implique l’élimination
de toute transition issue de, ou vers, ce sommet. Dans la figure 5.10, nous illustrons la
restriction du comportement normal de l’AHR présenté dans la figure 5.9. L’AHR H0
correspond à la partie de l’automate encadrée en pointillés.
Hypothèses : nous supposons que le modèle H vérifie les hypothèses suivantes :
H1 : H est fortement non-zénon.
H2 : la restriction du fonctionnement normal H0 est un AHR initialisé.
La première hypothèse permet de garantir la divergence du temps dans les exécutions
infinies. Ainsi, cette hypothèse garantit la progression du temps de chaque exécution du
système. La seconde hypothèse stipule que la restriction du fonctionnement H0 est un
136
Chapitre 5. Diagnostic des systèmes hybrides rectangulaires
H0
x1 = 0
R
1 x1 ≤ 30 a, x1 = 30 2 x1 ≥ 0 b, x1 = 0 3 x1 ≤ 50 4 x1 ≥ 0
c, x1 = 50
- - -
ẋ1 = 2 ẋ1 = −2 ẋ1 = 5 ẋ1 = 0
?
5 x1 ≤ 30 a, x1 = 30 6 x1 ≥ 10 u, x1 = 10 7 x1 ≥ 0 b, x1 = 0 8 x1 ≤ 50 c, x1 = 50 9 x1 ≥ 0
- ẋ - - -
ẋ1 = 2 1 ∈ [−4, −3] ẋ1 = −2 ẋ1 = 5 ẋ1 = 0
AHR initialisé. Nous rappelons que dans ce cas chaque changement de flux d’une va-
riable entre deux sommets implique une réinitialisation de cette variable. La vérification
de ces deux hypothèses est nécessaire pour l’application de notre méthode de test de
la diagnosticabilité, tandis que l’application de notre procédure de diagnostic nécessite
uniquement la vérification de la première hypothèse.
Nous allons vérifier ces hypothèses sur le modèle du système de chauffage de liquides
décrit dans l’exemple 5.3.1. L’automate hybride rectangulaire présenté dans la figure 5.7
vérifie les spécifications énumérées ci-dessus, si l’on considère la partition de défauts
Σf = F1 ∪ F2 , où F1 = {f uite} et F2 = {blocage_V1 }. La fonction de répartition ϕ est
définie comme suit :
0, si q ∈ {1, 2, 3},
ϕ(q) = 1, si q ∈ {4, 5, 6},
2, si q ∈ {7}.
Dans ce qui suit, nous vérifions que le modèle considéré satisfait les hypothèses H1 et
H2 :
1. H1 est satisfaite par le modèle. Il suffit de remarquer que dans les deux cycles
du modèle, l’horloge x2 (1) admet la dynamique ẋ2 = 1 dans tous les sommets,
(2) est remise à zéro dans les transitions sur l’événement s2 et (3) admet la va-
leur 40 comme une borne inférieure dans la garde de chaque transition associée à
l’événement u (ainsi, dans chaque exécution d’un cycle s’écoule au moins 40 u.t.).
2. H2 est satisfaite par le modèle. En effet, le modèle du comportement normal,
constitué par les sommets 1, 2 et 3 correspond à un AHR initialisé.
Tout au long de cette partie, nous supposons que le système à diagnostiquer est mo-
délisé par un automate hybride rectangulaire H = (L, X, Σ, E, inv, f lux, init), vérifiant
137
Chapitre 5. Diagnostic des systèmes hybrides rectangulaires
138
Chapitre 5. Diagnostic des systèmes hybrides rectangulaires
6
nouvelle
Oui
estimation ? ?Oui
selon Annoncer Annoncer
(σ, t ≤ DAM) ou t = DAM
défaillance Fi Normal
? ?
Attendre événement Intialiser t à 0 Calculer
DAM
ou l’expiration de t armer t = DAM
6 6
événements observables
139
Chapitre 5. Diagnostic des systèmes hybrides rectangulaires
Un état de diagnostic d est dit Fi -certain, i ∈ {1, . . . , m}, si Éval(d) = Fi ; i.e., tous
ses éléments sont Fi -certain.
Nous présentons dans la suite, la fonction d’accessibilité non observable à temps borné,
notée T R. La fonction T R permet de déterminer l’ensemble des états accessibles depuis
un ensemble d’états de départ ddépart , suite à l’occurrence d’événements non observables
et l’écoulement d’une durée de temps, donnée par le paramètre β ≥ 1, depuis l’occurrence
du dernier événement observable (lorsque aucun événement observable ne s’est produit,
nous considérons cette durée à partir des états initiaux).
L’application de cette fonction nécessite l’ajout d’une horloge y au modèle AHR du
système, permettant de mesurer le temps écoulé à partir de la dernière occurrence d’un
événement observable. Cette horloge est réinitialisée à 0 dans chaque état initial et lors
du franchissement de chaque transition sur un événement observable. Dans chaque état
140
Chapitre 5. Diagnostic des systèmes hybrides rectangulaires
141
Chapitre 5. Diagnostic des systèmes hybrides rectangulaires
142
Chapitre 5. Diagnostic des systèmes hybrides rectangulaires
Exemple 5.4.1
Nous considérons deux cas d’application de la procédure de diagnostic sur le
système de chauffage de liquides représenté dans la figure 5.3.1. Dans chaque
cas, nous illustrons les étapes de l’exécution de la procédure de diagnos-
tic étant donnée une séquence d’observations générée par le système. Nous
rappelons que l’application de notre procédure nécessite l’introduction de
l’horloge y dans le modèle du système, qui permet de déterminer le temps
qui s’est écoulé depuis l’occurrence du dernier événement observable. Nous
considérons la partition de défauts suivante : Σf = F1 ∪ F2 , où F1 = {f uite}
et F2 = {blocage_V1 }.
Dans le premier cas d’application, nous supposons que
le système effectue une exécution sur la trace "ω1 =
125, s1 , 40, u, 70, s2 , 10, f uite, 115, s1 , 40, u, 55, s2 ". Nous fixons la valeur
du paramètre T à 80. Nous présentons dans la suite les étapes de l’exécution
de la procédure, lorsque le système génère la partie observable de ω1 ; i.e.,
"P (ω1 ) = 125, s1 , 110, s2 , 125, s1 , 95, s2 ".
1. Initialement, dcour := {[(1, hx1 ∈ [0, 500] ∧ x2 = y = 0i), N ]} ;
2. Le délai DAM est estimé à 80 u.t.. Le temporisateur t expire après 80
u.t., dcour ← {[(1, hx1 ∈ [240, 500] ∧ x2 = 80 ∧ y = 80i), N ], [(4, hx1 ∈
[160, 500] ∧ x2 = 80 ∧ y = 80i), F1 ], [(7, hx1 ∈ [0, 500] ∧ x2 = 80 ∧ y =
80i), F2 ]}. La procédure génère le diagnostic "État incertain" ;
3. DAM ← 80. L’événement s1 est observé à t = 45, dcour ← {[(2, hx1 =
500 ∧ x2 = 0 ∧ y = 0i), N ], [(5, hx1 = 500 ∧ x2 = 0 ∧ y = 0i), F1 ]}. La
procédure génère le diagnostic "État incertain" ;
4. DAM ← 80. Le temporisateur expire à t = 80, dcour ← {[(3, hx1 ∈
[180, 260] ∧ x2 = 80 ∧ y = 80i), N ], [(6, hx1 ∈ [60, 140] ∧ x2 = 80 ∧ y =
80i), F1 ]}. La procédure génère le diagnostic "État incertain" ;
5. DAM ← 80. L’événement s2 est observé à l’instant t = 30, dcour ←
{[(1, hx1 = 0∧x2 = 110∧y = 0i), N ]}. La procédure génère le diagnostic
"Normal" ;
6. DAM ← 80. Le temporisateur expire à t = 80, dcour := {[(1, hx1 ∈
[240, 400] ∧ x2 = 190 ∧ y = 80i), N ], [(4, hx1 ∈ [260, 320] ∧ x2 = 190 ∧ y =
80i), F1 ], [(7, hx1 ∈ [0, 400] ∧ x2 = 190 ∧ y = 80i), F2 ]}. La procédure
génère le diagnostic "État incertain" ;
7. DAM ← 80. L’événement s1 est observé à t = 45, dcour := {[(2, hx1 =
500 ∧ x2 = 0 ∧ y = 0i), N ], [(5, hx1 = 500 ∧ x2 = 0 ∧ y = 0i), F1 ]}. La
procédure génère le diagnostic "État incertain" ;
143
Chapitre 5. Diagnostic des systèmes hybrides rectangulaires
144
Chapitre 5. Diagnostic des systèmes hybrides rectangulaires
145
Chapitre 5. Diagnostic des systèmes hybrides rectangulaires
Dans les deux exemples étudiés, la procédure de diagnostic réussit à identifier l’oc-
currence du défaut. Notre procédure de diagnostic demeure applicable, même s’il s’agit
d’un modèle non diagnosticable du système. Cependant, la consistence du résultat fourni
dans ce dernier cas n’est pas garantie puisque la procédure est incapable d’identifier l’oc-
currence de tout mode de défaillance au bout d’un délai fini. En effet, dans un modèle
non diagnosticable, il peut exister deux traces ayant la même projection observable et
qui correspondent à deux modes de fonctionnement différents du système. En s’appuyant
sur un modèle non diagnosticable, la procédure de diagnostic peut générer indéfiniment
le diagnostic "état incertain" alors qu’un défaut s’est produit. Dans ce cas, il est impos-
sible de distinguer le comportement observable du mode de défaillance correspondant
à ce défaut et les comportements observables associés aux autres modes de fonctionne-
ment du système. Cette conclusion nous amène à étudier, dans la section suivante, la
diagnosticabilité du modèle utilisé pour le diagnostic.
Nous présentons dans cette section une notion de diagnosticabilité de langages tempo-
risés, en considérant une partition de plusieurs modes de défaillance, que nous appelons
la diagnosticabilité à Horizon de Temps Limité (HTL). Ensuite, nous présentons une
approche systématique permettant la vérification de la diagnosticabilité à HTL d’un
(language temporisé accepté par un) AHR soumis aux conditions considérées dans notre
démarche de diagnostic (Derbel et al., 2009d).
Soit L un langage temporisé accepté par un AHR H, vérifiant les conditions dis-
cutées dans la sous section 5.4.1. Nous associons à chaque ensemble de défauts Fi ,
i ∈ {1, . . . , m}, un sous langage de L, noté Li , tel que chaque trace dans Li contient
au moins un événement de l’ensemble Fi . Nous désignons par L0 ⊆ L, le sous-ensemble
de traces de L, ne contenant pas de défauts.
La propriété suivante découle de l’absence du scénario de défauts multiples dans notre
modèle ; i.e, une trace ne peut pas contenir deux défauts appartenant à deux modes
différents.
146
Chapitre 5. Diagnostic des systèmes hybrides rectangulaires
P (ω) = P (ω 0 ) =⇒ ω 0 ∈ Li .
Exemple 5.5.1
Considérons le langage temporisé L accepté par l’AHR illustré dans la fi-
gure 5.12. Nous supposons que Σo = {a, b} et Σf = {f1 , f2 }. Trois cas sont
considérés dans cet exemple.
147
Chapitre 5. Diagnostic des systèmes hybrides rectangulaires
4 x ≤ 60 a, x = 60 5 x≥0
x=0 -
f1 , x = 0
* ẋ = 3 ẋ = 2
w 1 x ≤ 60 2 x ≤ 90 3 x≥0
a, x = 60 - b, x = 90
-
ẋ = 3 ẋ = 3 ẋ = 3
f2 , x = 0 6 x ≤ 60 a, x = 60 7 x ≤ 90 b, x = 90 8 x≥0
j - ẋ ∈ [1, 2]
-
ẋ = 3 ẋ ∈ [1, 2]
148
Chapitre 5. Diagnostic des systèmes hybrides rectangulaires
149
Chapitre 5. Diagnostic des systèmes hybrides rectangulaires
Proposition 2. Nous notons par L(Hi ) et L(Hi ), les langages temporisés acceptés par
les AHRs Hi et Hi , respectivement. Pour i ∈ {1, . . . , m}, les propositions suivantes
découlent de la construction des AHRs Hi et Hi :
[m
• L(Hi ) = L − Lk = L0 ∪ Li ;
k=1,k6=i
• L(Hi ) = L − Li .
Proposition 3. Pour tout i ∈ {1, . . . , m}, les propositions suivantes sont équivalentes :
1. Il existe une paire d’exécutions de Hi et Hi , sur les traces temporisées ω1 et ω2 ,
atteignant les états (q1 , v1 ) et (q2 , v2 ), tel que P (ω1 ) = P (ω2 ) ;
2. Il existe une exécution de Hi,i , sur une trace temporisée ω, atteignant l’état
((q1 , q2 ), v1 v2 ).
150
Chapitre 5. Diagnostic des systèmes hybrides rectangulaires
L’existence d’une trace temporisée acceptée par Hi,i et contenant un défaut de l’en-
semble Fk , implique l’existence d’une paire de traces de Lk et L − Lk , respectivement,
ayant la même projection observable, comme établit le lemme suivant :
θ
Dans la troisième étape de la procédure, nous construisons l’AHR Hi,i = (Qi,i , Xi,i ,
Σi,i , Ei,i , invi,i , f luxi,i , initi,i , Mi,i ), qui correspond au produit de Hi,i avec un simple AHR
à deux sommets, noté T B θ = ({qM , qM }, {y 1 , . . . , y m }, {µ}, E, inv, f lux, init, {qM }) et
illustré dans la figure 5.13. Nous remarquons l’absence de synchronisation d’événements
au cours de ce produit puisque µ ∈ / Σ. L’application de cette étape nous permet d’isoler
l’ensemble des traces appartenant à Lθkk , pour k ∈ {1, . . . , m}. En effet, la progression du
θ
temps est bloquée dans les exécutions de l’AHR Hi,i contenant des défauts de l’ensemble
Fk , k ∈ {1, . . . , m} après l’expiration de fenêtre temporelle définie par l’intervalle [0, θi ] ;
i.e., lorsque y k = θk . Ainsi, lorsque le chronomètre y k atteint la valeur θk dans une
θ
exécution de Hi,i contenant un défaut de Fk , k ∈ {1, . . . , m}, une transition discrète vers
un sommet marqué sera franchie. Ensuite, la condition d’invariant de ce sommet marqué
sera violée instantanément après l’entrée dans ce sommet, impliquant le blocage de cette
exécution.
j µ, y 1 ≥ θ1
qM qM
.
y 1
∈ [0, θ1 ] . q y 1 ∈ [0, θ1 ]
∧ . - ∧
... µ, y i ≥ θi ...
∧ . 1 m
∧
y m ∈ [0, θm ] .
.
y ∈ [0, θm ]
µ, y k ≥ θk
151
Chapitre 5. Diagnostic des systèmes hybrides rectangulaires
Cette fonction utilise une analyse symbolique pour vérifier l’existence d’états marqués,
accessible depuis l’ensemble des états initiaux, représentés par (q0 , z0 ).
Le théorème suivant établit la convergence de la procédure d’analyse d’accessibilité,
appliquée sur l’AHR
θ
Théorème 2. La fonction d’analyse d’accessibilité, appliquée aux AHRs Hi,i , pour tout
i ∈ {1, . . . , m}, s’arrête au bout d’un temps fini.
Intuitivement, ce résultat peut être expliqué dans les deux points suivants. D’une part,
θ
la restriction du comportement normal de l’AHR Hi,i est un AHR initialisé qui est une
sous-classe décidable pour le problème d’analyse d’accessibilité (Henzinger et al., 1998).
En effet, la procédure d’analyse s’arrête au bout d’un temps fini en parcourant cette
restriction. D’autre part, l’analyse de la partie restante de l’AHR (les comportements
défaillants) s’arrête sous l’influence des conditions d’invariants définies sur les chrono-
mètres y i , i ∈ {1, . . . , m}, dans les sommets associés aux comportements défaillants. Une
preuve complète de ce théorème est donnée dans l’annexe B.
θ
L’AHR Hi,i , i ∈ {1, . . . , m} permet d’isoler toute paire de traces dans Lk et L − Lk ,
k ∈ {1, . . . , m}, telle que θk u.t. se sont écoulées après la première occurrence d’un défaut
de l’ensemble Fk . En effet, l’existence d’une trace temporisée dont l’exécution atteint un
θ
sommet marqué, dans un AHR Hi,i , i ∈ {1, . . . , m}, implique l’existence d’une paire
de traces dans Lθkk et L − Lk ayant la même projection observable. Cette propriété est
formulée dans le lemme suivant :
Preuve : le sens (=⇒) : nous supposons qu’un sommet marqué est accessible dans
θ
Hi,i En effet, ∃q ∈ Mi,i , i ∈ {1, . . . , m}, tel que le sommet marqué q est accessible à
.
θ
travers une exécution de Hi,i sur une trace temporisée ω. D’après le lemme 8, il existe
152
Chapitre 5. Diagnostic des systèmes hybrides rectangulaires
une paire de traces ω1 ∈ Lθkk et ω2 ∈ L − Lk , k ∈ {1, . . . , m}, telle que P (ω1 ) = P (ω2 ).
En conclusion, L n’est pas diagnosticable dans l’HTL θ.
Dans le sens opposé (⇐=), nous supposons que L n’est pas diagnosticable. Alors, il
existe k ∈ {1, . . . , m} et une paire de traces ω1 ∈ Lθkk et ω2 ∈ / Lk , telle que P (ω1 ) =
P (ω2 ). Puisque ω2 ∈ L − Lk et d’après le lemme 8, nous pouvons conclure qu’il existe
θ
i ∈ {1, . . . , m} et une exécution de l’AHR Hi,i , atteignant un sommet marqué.
Exemple 5.5.2
Nous présentons dans les figures 5.14, 5.15, 5.16, et 5.17 les différents
AHRs nécessaires pour la vérification de la diagnosticabilité du modèle décrit
dans la figure 5.7. Pour des raisons de clarté, nous n’avons pas présenté les
θ θ
AHRs H1,1 et H2,2 . Ces AHRs peuvent être déduits facilement à partir des
AHRs H1,1 et H2,2 .
7 vrai
ẋ1 = 0
ẋ2 = 1 s2 , x1 1
1 = 0, [x1 := 0]
x1 1
1 ∈ [0, 500] ∧ x2 = 0
ẏ 2 = 1 s1 , x1 1 1
1 = 500, [x2 := 0; x1 := 500]
w ?
6 11 x1 21 x1
2 ≤ 40 31 x1
1 ≥ 0
blocage_V1 , x1 ≤ 500 1 ≤ 500
ẋ1
1 1∈ [3, 5]
- ẋ1
1=0 - ẋ1
1 ∈1[−8, −6]
ẋ2 = 1 ẋ1=1 ẋ2 = 1
1 12
s2 , x1 = 0, [x1 := 0]
ẏ =0 ẏ = 0 ẏ 1 = 0
u1 , x1
2 = 40, [x1 1
2 := 40; x1 := 500]
x1 ∈ [0, 500] ∧ x2 = 0 f uite, x1
1 ≤ 500
s1 , x1 = 500, [x2 := 0; x1 := 500]
?
w ? 41 x1
1 ≤ 500 51 x1
2 ≤ 40 61 x1
1 ≥ 0
1 x1 ≤ 500 2 x2 ≤ 40 3 x1 ≥ 0
ẋ1
1 ∈ [2, 4]
- ẋ1
1 ∈ [−2, −1] - ẋ1
1 ∈1[−9, −8]
ẋ1 ∈ [3, 5] - ẋ1 = 0 - ẋ1 ∈ [−8, −6] ẋ1
2 = 1 ẋ1
2 = 1
ẋ2 = 1
1 1
ẋ2 = 1 ẋ2 = 1 ẏ = 1 ẏ = 1 ẏ 1 = 1
ẋ2 = 1
s1 , x1 1
1 = 500, [x2 := 0] 1 1
u , x2 = 40
ẏ 2 = 0 ẏ 2 = 0 ẏ 2 = 0 6
u, x2 = 40, [x2 := 40; x1 := 500] s2 , x1
1 = 0
H1 H1
153
Chapitre 5. Diagnostic des systèmes hybrides rectangulaires
11 , 7 x1
1 ≤ 500
ẋ1
1 = 0
ẋ1 = 0
ẋ1
2 = 1 ẋ2 = 1
ẏ 1 = 0 ẏ 2 = 1
s2 , x1 1
6
blocage_V1 , x1 ≤ 500 1 = 0 ∧ x1 = 0, [x1 := 0; x1 := 0]
x1
1 ≥ 0
x1 ∈ [0, 500] ∧ x2 = 0 u1 , x1
2 = 40 31 , 2 x2 ≤ 40
u, x2 = 40
1 1
x1 ∈ [0, 500] ∧ x2 = 0 [x1
:= 40; x1
1 := 500]
2 ẋ1
[x2 := 40; x1 := 500]
1
s1 , x1 = 500 ∧ x1 = 500 1 ∈ [−8, −6]
1 1 ẋ1 = 0
[x2 := 0; x1 := 500; x2 := 0; x1 := 500]
ẋ1
w ? s
x1 x1 2 = 1 x1
1 ≥ 0
1 ≤ 500 2 ≤ 40 ẋ2 = 1
11 , 1 21 , 2 31 , 3 x ≥ 0
x1 ≤ 500 x2 ≤ 40 ẏ = 0 ẏ 2 = 0
1 1
1
ẋ1 ∈ [3, 5] ẋ1
1 = 0
ẋ11 ∈ [−8, −6]
ẋ1 ∈ [3, 5] - x1 ≥ 0 ẋ ∈ [−8, −6]
ẋ1 = 0 1
ẋ1 21 , 3 x1 ≤ 40 ẋ1
ẋ1
2 = 1 2 = 1 2 2 = 1
ẋ2 = 1 ẋ2 = 1 ẋ2 = 1
ẋ1
1 = 0
1
ẏ = 0 ẏ = 0 2 ẏ = 0 ẏ 2 = 0
1
ẋ1 ∈ [−8, −6] ẏ 1 = 0 ẏ 2 = 0
1
ẋ1
2 = 1 u1 , x1
u, x2 = 40 ẋ2 = 1 2 = 40
[x1 1
s
[x2 := 40; x1 := 500] ẏ 1 = 0 ẏ 2 = 0 2 := 40; x1 := 500]
f uite, x1
1 ≤ 500 x1
1 ≥ 0
61 , 2 x2 ≤ 40 u, x2 = 40
u1 , x1
2 = 40 [x2 := 40; x1 := 500]
ẋ1
1 ∈ [−9, −8] j
? ẋ1 = 0 x1
x1 x1 ẋ1 1 ≥ 0
41 , 1 1 ≤ 500 2 ≤ 40 2 = 1 61 , 3
51 , 2 x1 ≥ 0
x1 ≤ 500 x2 ≤ 40 ẋ2 = 1
ẋ1 ẋ1 ẏ = 1 ẏ 2 = 0
1 ẋ1
1 ∈ [−9, −8]
1 ∈ [2, 4] 1 ∈ [−2, −1]
ẋ1 ∈ [3, 5]
- ẋ1 = 0 ẋ1 ∈ [−8, −6]
1
ẋ1 x1 ≥ 0 ẋ1
2 = 1
ẋ2 = 1 2 = 1 51 , 3
ẋ2 = 1 ẋ2 = 1 x1
2 ≤ 40
ẋ2 = 1
ẏ = 1 ẏ 2 = 0
1
ẏ 1 = 1 ẏ 2 = 0 ẏ 1 = 1 ẏ 2 = 0 ẋ1
1 ∈ [−2, −1]
s1 , x1 ẋ1 ∈ [−8, −6] 3
1 = 500 ∧ x1 = 500 u1 , x1
6
[x1 ẋ1
2 = 1 2 = 40
2 := 0; x2 := 0; x1 := 500] u, x2 = 40 j
ẋ2 = 1
[x2 := 40; x1 := 500] 1
ẏ = 1 ẏ 2 = 0
s2 , x1
1 = 0 ∧ x1 = 0, [x1 := 0]
72 vrai
ẋ2
1 = 0
ẋ2
2 = 1
s2 , x1 = 0, [x1 := 0]
ẏ 2 = 1 x1 ∈ [0, 500] ∧ x2 = 0 s1 , x1 = 500, [x2 := 0; x1 := 500]
R ?
6
blocage_V1 , x2 1 x1 ≤ 500 2 x2 ≤ 40 3 x1 ≥ 0
1 ≤ 500
ẋ1 ∈ [3, 5] - ẋ1 = 0 - ẋ1 ∈ [−8, −6]
ẋ2 = 1 ẋ2 = 1 ẋ2 = 1
s2 , x 2 2 ẏ 1 = 0 1
ẏ = 0 ẏ 1 = 0
1 = 0, [x1 := 0]
u, x2 = 40, [x2 := 40; x1 := 500]
x2 2
1 ∈ [0, 500] ∧ x2 = 0 f uite, ≤ 500
s1 , x2 2 2
1 = 500, [x2 := 0; x1 := 500] ?
w ? 4 x1 ≤ 500 5 x2 ≤ 40 6 x1 ≥ 0
2 2 x2 ≤ 40 2
1 x2
1 ≤ 500 2 3 x1 ≥ 0
ẋ1 ∈ [2, 4] - ẋ1 ∈ [−2, −1] - ẋ1 ∈ [−9, −8]
ẋ2 ẋ2
1 = 0
ẋ2
1 ∈ [−8, −6] ẋ2 = 1 ẋ2 = 1 ẋ2 = 1
1 ∈ [3, 5]
- -
1 1
ẋ2 ẋ2 ẏ = 1 ẏ = 1 ẏ 1 = 1
ẋ2
2 = 1 2 = 1 2 = 1
s1 , x1 = 500, [x2 := 0] u, x2 = 40
ẏ 2 = 0 ẏ 2 = 0 ẏ 2 = 0 6
u2 , x2 2 2
2 = 40, [x2 := 40; x1 := 500] s2 , x1 = 0
H2 H2
θ
l’AHR H1,1 . Par conséquent, il existe un sommet marqué accessible depuis un
état initial et ainsi, le langage L n’est pas diagnosticable dans cette fenêtre
temporelle. A titre d’exemple, nous pouvons retenir l’accessibilité de l’état
154
Chapitre 5. Diagnostic des systèmes hybrides rectangulaires
12 , 7 x2
1 ≤ 500
ẋ2
1 = 0
ẋ1 = 0
ẋ2
2 = 1 ẋ2
2 = 1
ẏ 1 = 0 ẏ 2 = 1
s2 , x2 2
6
blocage_V1 , x2 1 = 0 ∧ x1 = 0, [x1 := 0; x1 := 0]
1 ≤ 500
x2
1 ≥ 0
x1 ∈ [0, 500] ∧ x2 = 0 32 , 2 x2 ≤ 40
u2 , x2
2 = 40 u, x2 = 40
x2 2
1 ∈ [0, 500] ∧ x2 = 0 [x2 2
2 := 40; x1 := 500]
ẋ2 [x2 := 40; x1 := 500]
1 ∈ [−8, −6]
ẋ1 = 0
w ? ẋ2
2 = 1
s
x2 x2
2 ≤ 40
x2
1 ≥ 0
12 , 1 1 ≤ 500 ẋ2 = 1
22 , 2 ẏ = 0 ẏ 2 = 0
1 32 , 3 x ≥ 0
x1 ≤ 500 x2 ≤ 40 1
ẋ21 ∈ [3, 5] ẋ2 ẋ2
- 1 = 0 x1 ≥ 0 1 ∈ [−8, −6]
ẋ1 ∈ [3, 5] ẋ1 = 0 ẋ1 ∈ [−8, −6]
2 22 , 3 x2 ≤ 40
ẋ2
2 = 1 ẋ 2 = 1 2 ẋ2
2 = 1
ẋ2 = 1 ẋ2 = 1 ẋ2 = 1
ẋ2
1 = 0
1
ẏ = 0 ẏ = 02 ẏ = 0 ẏ 2 = 0
1
ẋ1 ∈ [−8, −6] ẏ = 0 ẏ 2 = 0
1
1
s1 , x2 = 500 ∧ x1 = 500 ẋ2
2 = 1 u2 , x2
2 = 40
1 u, x2 = 40
[x2 2
2 := 0; x1 := 500; x2 := 0; x1 := 500] ẋ2 = 1
[x2 := 40; x2
s
[x2 := 40; x1 := 500] ẏ 1 = 0 ẏ 2 = 0 2 1 := 500]
f uite, x1 ≤ 500 x2 ≥ 0
1 u2 , x2
2 = 40
22 , 6 x2 ≤ 40 [x2 := 40; x2
u, x2 = 40
2 1 := 500]
ẋ1 ∈ [−9, −8] j
? ẋ21 = 0 x2
x2 x2 ẋ2 1 ≥ 0
12 , 4 1 ≤ 500 2 ≤ 40 2 = 1 32 , 6
22 , 5 x1 ≥ 0
x1 ≤ 500 x2 ≤ 40 ẋ2 = 1
ẋ1 ∈ [2, 4] ẋ1 ∈ [−2, −1] ẏ 1 = 1 ẏ 2 = 0 ẋ1 ∈ [−9, −8]
ẋ2
- ẋ2 ẋ2
1 ∈ 2[−8, −6]
1 2∈ [3, 5] 1 = 0 ẋ2 = 1
ẋ2 x1 ≥ 0
ẋ2 = 1 2 = 1 32 , 5 ẋ2 = 1
ẋ2 = 1 ẋ 2 = 1 x2
2 ≤ 40
ẏ 1 = 1 ẏ 2 = 0
ẏ 1 = 1 ẏ 2 = 0 ẏ 1 = 1 ẏ 2 = 0 ẋ1 ∈ [−2, −1]
s1 , x1 = 500 ∧ x2 ẋ2
1 ∈ 2[−8, −6]
3
1 = 500 u, x2 = 40
6[x2 := 0; x2 2 ẋ2 = 1
2 := 0; x1 := 500] u , x2 = 40
2 2 j
ẋ2 = 1
[x2 2
2 := 40; x1 := 500] ẏ 1 = 1 ẏ 2 = 0
s2 , x2
1 = 0 ∧ x1 = 0, [x1 := 0]
5.6 Complexité
Dans un premier volet, nous présentons quelques remarques sur les issues d’implé-
mentation de notre procédure de diagnostic et de notre démarche de vérification de la
155
Chapitre 5. Diagnostic des systèmes hybrides rectangulaires
11 , 7, qM x1
1 ≤ 500
µ, y 1 ≥ 125
ẋ1
1 = 0
ẋ1 = 0 - ... ... ... ...
ẋ1
2 = 1 ẋ2 = 1 ...
1 6 6
µ, y ≥ 125 6
ẏ 1 = 0 ẏ 2 = 1 1
1 ≥ 125
µ, y ≥ 125
6 µ, y µ, y 1 ≥ 125
s2 , x1 0, [x1
6 = 0 ∧ x1 = := 0; x1 := 0]
blocage_V1 , x1 ≤ 500 1 1
x1
1 ≥ 0
x1 ∈ [0, 500] ∧ x2 = 0 u1 , x1
2 = 40 31 , 2, qM x ≤ 40
2 u, x2 = 40
x1 1 [x1 1
2 := 40; x1 := 500]
>
1 ∈ [0, 500] ∧ x2 = 0 ẋ1 [x2 := 40; x1 := 500]
s1 , x1 ∧ x1 = 500 1 ∈ [−8, −6]
1 = 500 ẋ1
R ? 1 1
[x2 := 0; x1 := 500; x2 := 0; x1 := 500] ẋ1 = 0 2 = 1
j
x1 ≤ 500 x1 ≤ 40 ẋ2 = 1 x1
1 ≥ 0
11 , 1, qM x11 ≤ 500 21 , 2, qM x22 ≤ 40 31 , 3, qM
1
y ≤ 125 y 1 ≤ 125 ẏ 1 = 0 ẏ 2 = 0 x1 ≥ 0
ẋ1
1 ∈ [3, 5] ẋ1 = 0 ẋ1 ẋ1
1 ∈ [−8, −6]
ẋ1 ∈ [3, 5] - 1 = 0 x1 ≥ 0 ẋ1 ∈ [−8, −6]
ẋ1 =1 21 , 3, qM x1
1
ẋ2 = 1 2 2 ≤ 40 ẋ1
2 = 1
ẋ = 1 ẋ2 = 1 ẋ2 = 1
2 ẋ1
1 = 0
ẏ 1 = 0 ẏ 2 = 0 ẏ 1 = 0 ẏ 2 = 0 ẋ1 ∈ [−8, −6] 1 ẏ = 0 ẏ 2 = 0
1
ẋ1
2 = 1 u1 , x1
u, x2 = 40 2 = 40
ẋ2 = 1 [x1 := 40; x1
j
[x2 := 40; x1 := 500] ẏ = 0 ẏ 2 = 0
1 2 1 := 500]
f uite, x1
1 ≤ 500 x11 ≥ 0
61 , 2, qM x ≤ 40 u, x2 = 40
2
u1 , x1
2 = 40
> [x2 := 40; x1 := 500]
ẋ11 ∈ [−9, −8] q
? ẋ1 = 0 x11 ≥ 0
x1 ≤ 500 x1 ≤ 40 ẋ1 61 , 3, qM x1 ≥ 0
41 , 1, qM x11 ≤ 500 51 , 2, qM x22 ≤ 40 2 = 1
y 1 ≤ 125
ẋ2 = 1 y 1 ≤ 125
y 1 ≤ 125 ẏ 1 = 1 ẏ 2 = 0 ẋ1
ẋ1
1 ∈ [2, 4] 1 ∈ [−9, −8]
- ẋ1
1 ∈ [−2, −1] ẋ1 ∈ [−8, −6]
ẋ1 ∈ [3, 5] ẋ1 = 0 x1 ≥ 0 ẋ1
ẋ1
2 = 1 ẋ1
2 = 1 51 , 3, qM 2 = 1
x12 ≤ 40 ẋ2 = 1
ẋ2 = 1 ẋ2 = 1 y 1 ≤ 125
1 2 ẏ = 1 ẏ 2 = 0
1
ẏ = 1 ẏ = 0 ẏ = 1 ẏ 2 = 0
1
ẋ1
1 ∈ [−2, −1] *
s1 , x1 ẋ1 ∈ [−8, −6]
1 = 500 ∧ x1 = 500 u1 , x1
6
[x1 ẋ1
2 = 1 2 = 40
2 := 0; x2 := 0; x1 := 500] u, x2 = 40 q
ẋ2 = 1
[x2 := 40; x1 := 500]
1 ẏ = 1 ẏ 2 = 0
1
µ, y ≥ 125
µ, y 1 ≥ 125 s2 , x1
1 = 0 ∧ x1 = 0, [x1 := 0]
? ?
... x1 2 ≤ 40
µ, y 1 ≥ 125 µ, y 1 ≥ 125
51 , 2, qM µ, y 1 ≥ 125
x2 ≤ 40
y 1 ≤ 125 ? ?
ẋ1 = 0
? ...
...
ẋ1 ...
2 = 1
ẋ2 = 1
ẏ = 1 ẏ 2 = 0
1
θ
Fig. 5.18 – Exemple de l’accessibilité d’un sommet marqué dans l’AHR H1,1 .
diagnosticabilité à HTL. Dans un second volet, nous présentons quelques éléments sur
la complexité des algorithmes utilisés dans ce travail.
156
Chapitre 5. Diagnostic des systèmes hybrides rectangulaires
Les polyèdres peuvent être classés en deux ensembles : les polyèdres convexes et les
polyèdres non-convexes. La première classe de polyèdres est la plus simple à utiliser.
Les différentes opérations appliquées dans notre travail pour le calcul des successeurs
d’une région : intersection, futur et réinitialisation ainsi que l’utilisation de contraintes
de gardes et d’invariants rectangulaires, préservent la convexité des régions calculées. La
manipulation de polyhèdres convexes dans les algorithmes développés dans notre travail
facilite la tâche de calcul et réduit la taille des structures de données utilisées pour le
stockage de ces régions.
Plusieurs outils de vérification d’automates hybrides linéaires développés ont été pro-
posés dans la littérature, tels que PHAVer (Frehse, 2005) et HyTech (Henzinger et al.,
1997). Ces outils implémentent des structures de données ainsi qu’un ensemble d’opéra-
tions élémentaires permettant d’analyser l’espace d’état des automates hybrides linéaires.
Dans le cadre de notre travail, nous pouvons utiliser la bibliothèque de manipulation
de polyhèdres Parma (Bagnara et al., 2002) pour l’implémentation de la procédure de
diagnostic. Cette bibliothèque, utilisée par l’outil PHAVer, présente une implémenta-
tion des régions polyhèdrales ainsi que les opérations employées dans notre travail pour
leur manipulation. Cette implémentation est robuste puisqu’elle permet de supporter
des valeurs arbitrairement larges. Afin d’appliquer notre procédure de vérification de
diagnosticabilité, nous pouvons utiliser l’implémentation de la procédure d’analyse d’ac-
cessibilité développée dans l’outil PHAVer. Afin de forcer la convergence de l’algorithme
d’analyse en avant, PHAVer applique des techniques d’approximation sur les régions
polyhédrales calculées. Ces techniques d’approximation peuvent être désactivées lors de
l’analyse des AHRs considérés dans notre travail puisque la convergence de la procédure
d’analyse d’accessibilité est garantie pour ces AHRs.
157
Chapitre 5. Diagnostic des systèmes hybrides rectangulaires
dcour associée à une étiquette Fi ; i ∈ {1, . . . , m} et calculée depuis plus que θi u.t.. En
d’autres termes, toute estimation associée à une étiquette Fi expire après l’écoulement
de θi u.t. puisqu’elle ne peut pas inclure l’état courant du système, sinon, la condition
de diagnosticabilité est contredite.
La complexité de la vérification de la diagnosticabilité à HTL correspond essentiel-
θ
lement à la complexité de la fonction d’analyse accessibilité, appliquée sur l’AHR Hi,i ,
pour i ∈ {1, . . . , m}. Afin de calculer cette complexité, nous supposons une exécution
sur deux étapes de cette procédure (la même démarche considérée dans la preuve du
0
théorème 3). Dans la première étape, l’algorithme parcourt la restriction Hi,i ⊗ T B θ de
θ
l’AHR Hi,i . D’après la propsition 4, cette restriction correspond à un AHR initialisé.
Par conséquent, la complexité de l’algorithme d’analyse, appliqué sur cette restriction,
est PSPACE. D’un autre coté, la complexité d’exécution de la seconde étape est ex-
ponentielle en fonction du nombre de sommets de cet automate ; i.e., elle est égale à
θmax
O(k bk. d c ), où k désigne le nombre de sommets de Hi,i θ
, θmax = max(θ1 , . . . , θm ) et d la
θ
durée minimale pour l’exécution d’un cycle dans Hi,i . En conclusion, la complexité de la
vérification de la diagnosticabilité à HTL est exponentielle.
5.7 Conclusion
Nous avons présenté dans ce chapitre une démarche de diagnostic pour les SDH mo-
délisés par des automates hybrides rectangulaires vérifiant certaines conditions. Cette dé-
marche nécessite la conception d’un modèle complet du système puis l’application d’une
procédure de diagnostic en-ligne, qui estime l’état courant du système ainsi que les occur-
rences de défauts. L’élaboration d’une estimation peut être déclenchée par l’observation
d’un événement ou le dépassement d’un délai seuil d’attente. Nous avons présenté par la
suite une notion de diagnosticabilité appelée diagnosticabilité à horizon de temps limité.
Cette notion permet de garantir l’identification de tout mode de défaillance au bout
d’un délai fini de temps défini par une fenêtre temporelle θ. Nous avons développé une
méthode systématique permettant la vérification de la diagnosticabilité à HTL. Cette mé-
thode repose sur l’application d’une fonction d’analyse d’accessibilité sur un ensemble de
produits synchrones d’automates, construits à partir du modèle du système. Enfin, nous
avons présenté quelques éléments sur l’implémentation et la complexité des algorithmes
utilisés dans notre travail.
158
Chapitre 6
Conclusion générale et
perspectives
L’objectif de cette thèse était la mise en œuvre d’une démarche de diagnostic pour les
systèmes à événements discrets temporisés et une sous-classe de systèmes dynamiques
hybrides. Nous nous sommes basés sur un ensemble de travaux de référence (Sampath
et al., 1995, 1996; Tripakis, 2002) pour l’élaboration de notre démarche.
Dans un premier temps, nous nous sommes intéressés au diagnostic des systèmes
temporisés, en utilisant le modèle automate temporisé. Ce modèle permet de repré-
senter explicitement l’information temporelle dans un SED à travers l’utilisation d’un
ensemble d’horloges réelles. Ainsi, notre approche permet l’identification des défauts qui
s’expriment par un changement des dates d’occurrence des événements observables. La
solution présentée dans notre travail repose sur la construction hors-ligne d’un diagnos-
tiqueur. Cette solution hors-ligne nous permet de minimiser le calcul effectué pendant la
phase en-ligne du diagnostic. Le calcul en-ligne se réduit dans notre cas au franchissement
d’une transition dans l’automate temporisé du diagnostiqueur et une simple évaluation
de son sommet courant. Afin de contourner l’indécidabilité du problème de synthèse du
diagnostiqueur à partir du modèle général d’automate temporisé, nous avons considéré
un ensemble d’hypothèses sur le modèle du système à diagnostiquer, telles que l’absence
d’affectations d’horloges dans les transitions sur des événements non observables et la
spécification de conditions de gardes bornées dans les sommets non-finaux.
Notre démarche de diagnostic à base de modèles SED temporisés commence par la
conception d’un modèle automate temporisé vérifiant certaines hypothèses. Ce modèle
décrit le comportement normal et les comportements défaillants du système. Ensuite,
nous avons présenté, intuitivement puis formellement, l’algorithme de synthèse du diag-
nostiqueur. Le diagnostiqueur obtenu suite à l’application de cet algorithme est un auto-
mate temporisé déterministe qui évolue en fonction des événements observables générés
159
Chapitre 6. Conclusion générale et perspectives
par le système. Chaque sommet de cet automate permet de retrouver une estimation de
l’état courant du système et les occurrences des événements de défauts non observables.
Une fonction de décision, analyse le sommet courant du diagnostiqueur et annonce l’oc-
currence d’un défaut du mode Fi lorsque ce sommet est Fi -certain. Enfin, nous avons
étudié la diagnosticabilité du modèle considéré dans notre démarche. Nous avons établi
que l’utilisation d’un diagnostiqueur est soumise à la vérification de la notion de diag-
nosticabilité du modèle considéré. Une méthode systématique permettant de vérifier la
diagnosticabilité du modèle automate temporisé a été élaborée. Cette méthode repose
sur la détection de cycles Fi -indéterminé et des sommets finaux Fi -incertain. Un théo-
rème liant la notion de diagnosticabilité et la vérification de ces conditions a été ensuite
présenté.
Dans un second temps, nous nous sommes intéressés à l’élaboration d’une approche
de diagnostic pour une sous-classe de SDH. L’élaboration de cette approche est motivée
par la capacité des modèles hybrides à représenter intrinsèquement les intéractions entre
la dynamique continue et la dynamique discrète d’un système réel. En plus, l’approxi-
mation du comportement d’un système en adoptant une modélisation SED temporisée
peut conduire à une perte considérable d’informations nécessaires pour la discrimination
des comportements défaillants. En effet, nous avons proposé une démarche de diagnostic
pour une sous-classe de SHD, représentée par le modèle automate hybride rectangulaire
vérifiant certaines hypothèses. Le choix de ce modèle nous a permis de contourner la
complexité que pose l’analyse des modèles hybrides en général. Notre méthode de diag-
nostic repose sur l’utilisation d’une procédure de diagnostic en-ligne, qui estime l’état
courant du système ainsi que les occurrences des défauts. L’élaboration d’une estimation
peut être déclenchée par l’observation d’un événement ou le dépassement d’un délai seuil
d’attente. Nous avons présenté par la suite une notion de diagnosticabilité appelée diag-
nosticabilité à horizon de temps limité. Cette notion permet de garantir l’identification de
tout mode de défauts au bout d’un délai fini à partir du temps d’occurrence du défaut,
défini par une fenêtre temporelle θ. Nous avons développé une méthode systématique
permettant la vérification de la diagnosticabilité à HTL. Cette méthode repose sur l’ap-
plication d’une fonction d’analyse d’accessibilité sur un ensemble de produits synchrones
d’automates, construits à partir du modèle du système.
Plusieurs perspectives peuvent être envisagées, à court terme ou à long terme, comme
suite au travail présenté dans cette thèse. Nous les avons regroupées selon quatre axes :
Dans un premier axe, nous envisageons implémenter les deux démarches de diagnostic
développées dans ce travail. Pour ce faire, nous utiliserons les différentes bibliothèques
proposées dans la littérature, permettant la modélisation et l’analyse des automates
temporisés et des automates hybrides rectangulaires. Une étude de la performance des
algorithmes développés sera ensuite établie afin de permettre de choisir l’implémentation
la plus optimale en termes de temps d’exécution de ressources consommées.
160
Chapitre 6. Conclusion générale et perspectives
Dans un second axe, nous visons à étendre notre démarche de diagnostic temporisé
dans le cadre des SDH. Il s’agit d’élaborer une démarche de diagnostic pour les SDH
basée sur la synthèse hors-ligne d’un diagnostiqueur en utilisant un modèle hybride.
L’élaboration de cette démarche nécessite d’un coté, la caractérisation d’une sous-classe
de modèles hybrides capable de rendre ce problème décidable et d’un autre, la conception
d’un algorithme de construction du diagnostiqueur approprié à ce type de modèles.
Dans un troisième axe, nous envisageons de prendre en considération la mesurabilité
de certaines variables continues au cours de notre démarche de diagnostic des SDH. L’ap-
proche de diagnostic pour les SDH présentée dans notre travail repose uniquement sur
l’observation d’une trajectoire d’événements discrets temporisés générée par le système.
Cependant, certaines variables telles que la température ou le débit peuvent être direc-
tement mesurées en utilisant des capteurs continus. L’abstraction de ces mesures par
l’utilisation de quelques événements discrets peut conduire à des inférences erronées. En
effet, une perspective de notre travail consiste à combiner notre solution avec l’approche
de Lunze (Lunze, 2006) qui repose sur une fine discrétisation des trajectoires continues.
Ainsi, la solution à développer doit répondre à ce compromis : minimiser la perte d’in-
formations engendrée par la discrétisation des trajectoires continues d’un coté, et éviter
le problème d’explosion combinatoire dû à cette opération d’un autre.
Dans un dernier axe, nous proposons de combiner notre approche de diagnostic à base
de modèles temporisés avec la théorie du contrôle supervisé développée par Ramadge
et Wonham (Ramadge et Wonham, 1987). Ce travail peut être envisagé dans le cadre
d’une extension de l’approche proposée dans (Sampath et al., 1998). Il s’agit de proposer
une solution intégrée qui permet de coupler le module du diagnostic avec le module du
contrôle. Cette solution repose sur la synthèse d’un superviseur qui permet d’autoriser
ou d’inhiber certains événements contrôllables du système afin de déterminer le plus
grand sous-langage temporisé diagnosticable. Ainsi, le diagnostiqueur résultant d’une
telle approche permet l’identification de tout mode de défaillance au bout d’un délai
fini de l’occurrence du correspondant défaut puisque le modèle du système est toujours
diagnosticable.
161
Chapitre 6. Conclusion générale et perspectives
162
Annexe A
163
Annexe A. Algorithme complet de synthèse du diagnostiqueur
164
Annexe B
Preuves
Preuve :
Nous prouvons ce lemme par induction sur le nombre de transitions discrètes n dans
le diagnostiqueur, effectuées pour accéder au sommet qnd à partir du sommet initial du
diagnostiqueur q0d .
Base : Le sommet initial du diagnostiqueur q0d = ({(q0 , N )}, z0 ) vérifie la propriété
en considérant que ω est égale à la trace vide.
induction : Nous supposons que la propriété est vraie pour l’ordre n ≥ 0, alors pour
chaque sommet qnd , accessible suite à n discrete transitions et pour chaque valuation
v ∈ Z(qnd ), le lemme est vérifié. Nous avons besoin de prouver que ce lemme est vrai pour
tous les sommets accessibles suite à travers n + 1 transitions discrètes.
d
Soit qn+1 un sommet du diagnostiqueur accessible à travers n + 1 transitions discrètes
dans D, alors, par construction du diagnostiqueur, il existe au moins un prédécesseur
d
de qn+1 , noté qnd , tel que qnd est accessible sur n transitions discrètes à partir du sommet
σn+1 ,ηn+1 ,Yn+1
d
initial du diagnostiqueur. Soit qnd −−−−−−−−−→ qn+1 la transition du sommet qnd vers le
165
Annexe B. Preuves
d
sommet qn+1 , alors :
1)
uo uo σ 1 ,g 1 σ 2 ,g 2
1-a) il existe un chemin de transitions (qn , φn , zn ) −−−−→ (qn1 , φ1n , zn1 ) −−
uo uo
−−→
σ k ,g k
uo uo σn+1 ,ηn+1 ,Yn+1
. . . −− −−→ (qnk , φkn , znk ) −−−−−−−−−→ (qn+1 , φn+1 , zn+1 ) dans l’automate S, où
1 k d
σuo , . . . , σuo ∈ Σuo . Par conséquence, pour toute valuation vn+1 ∈ Z(qn+1 ), il existe
ωu
un état (qn , vn ) où vn ∈ zn et une trace ωu telle que (qn , vn ) (qn+1 , vn+1 ).
1-b) A partir de notre hypothèse d’induction sur qnd , il existe une trace ωn ∈ L, telle
ω
que (q0 , v0 ) n (qn , vn ).
Nous concluons à travers (a) et (b) qu’il existe une trace de L, ωn+1 = ’ωn .ωu ’, telle
ωn+1
que (q0 , v0 ) (qn+1 , vn+1 ).
d
2) Maintenant, nous supposons que qn+1 contient au moins une paire d’éléments
d
(qn+1 , φn+1 ), (q̃n+1 , φ̃n+1 ) ∈ Dis(qn+1 ). Soit vn+1 ∈ Zn+1 , nous allons prouver qu’il existe
une paire d’exécution sur les traces ωn+1 , ω̃n+1 ∈ L, respectivement, atteignant les états
(qn+1 , vn+1 ) et (q̃n+1 , vn+1 ) avec P (ωn+1 ) = P (ω̃n+1 ).
2-a) Par construction du diagnostiqueur, il existe deux chemins de transitions
σ 1 ,g 1
uo uo σ 2 ,g 2 σ k ,g k σn+1 ,ηn+1 ,Yn+1
dans S, (qn , φn , zn ) −−−−→ (qn1 , φ1n , zn1 ) −−
uo uo uo uo
−−→ . . . −−−−→ (qnk , φkn , znk ) −−−−−−−−−→
0 0
σ̃ 1 ,g̃ 1
uo uo σ̃ 2 ,g̃ 2 σ̃ k ,g̃ k 0 0 0
(qn+1 , φn+1 , zn+1 ) et (q̃n , φ̃n , zn ) −−−−→ (q̃n1 , φ̃1n , z̃n1 ) −−
uo uo uo uo
−−→ . . . −−−−→ (q̃nk , φ̃kn , z̃nk )
σn+1 ,ηn+1 ,Yn+1 1 k 1 k 0
−−−−−−−−−→ (q̃n+1 , φ̃n+1 , zn+1 ), tels que σuo , . . . , σuo , σ̃uo , . . . , σ̃uo ∈ Σuo .
0
Par construction du prédicat ηn+1 , nous avons ηn+1 ⊆ znk et ηn+1 ⊆ z̃nk . Soient
(qnk , vn+1
e
) et (q̃nk , vn+1
e e
) deux états tels que vn+1 ∈ ηn+1 et vn+1 = vn+1 e
[Yn+1 ← 0]. Alors, il
existe une paire d’exécution sur deux traces temporisées ωu et ωu (dans (Σuo × R+ )∗ ), et
0
ω
une paire d’états (qn , vn ) et (q̃n , ṽn ), où vn ∈ zn et ṽn ∈ z̃n , telle que (qn , vn ) u (qnk , vn+1
e
)
ω0
et (q̃n , vn ) u (q̃nk , vn+1
e
). Puisque les transitions sur les événements non observables ne
permettent pas les affectations d’horloges (Hypothèse H2 ), il existe d, d˜ ∈ R+ , tels que
e
vn+1 = vn + d et vn+1 e ˜ Par conséquence, ṽn = vn + (d − d)
= ṽn + d. ˜ (nous supposons que
d − d˜ ≥ 0, sinon, nous inversons les termes de l’égalité). Par conséquence, l’état (q̃n , ṽn )
d−d˜
est accessible depuis l’état (q̃n , vn ) suite à l’écoulement de d − d˜ u.t. ; i.e., (q̃n , vn ) −−→
(q̃n , ṽn ). Nous notons que cette transition est possible puisque l’invariant du sommet q̃n
est convexe et égale à l’invariant du sommet qn . Par conséquence, il existe une exécution
ω̃ ˜ 0 ’. Il est clair
sur la trace temporisée ω̃u , telle que (q̃n , vn ) u (q̃nk , vn+1
e
), et ω̃u = ’(d − d).ω u
que temps(ωu ) = temps(ω̃u ) = d.
2-b) Selon notre hypothèse d’induction, il existe une paire de traces ωn , ω̃n ∈ L, telle
ω ω̃
que (q0 , v0 ) n (qn , vn ), (q0 , v0 ) n (q̃n , vn ) et P (ω) = P (ω̃).
166
Annexe B. Preuves
En concussion, d’après (a) et (b), il existe une paire de traces telle que
ωn+1 ω̃n+1
(q0 , v0 ) (qn+1 , vn+1 ) et (q0 , v0 ) (q̃n+1 , vn+1 ), où ωn+1 = ’ωn .ωu .σn+1 ’ et ω̃n+1 =
’ω̃n .ω̃u .σn+1 ’. En plus, P (ωn+1 )=’P (ωn ).temps(ωu ).σn+1 ’. Puisque temps(ωu ) =
temps(ω̃u ) et P (ω) = P (ω̃), alors, P (ωn+1 ) = P (ω̃n+1 ).
Lemme 5
d
Soit qn+1 un sommet d’un cycle Fi -indéterminé et soit (qn+1 , Fi ), (q̃n+1 , φ̃n+1 ) ∈
d
Dis(qn+1 ), tel que φ̃n+1 6= Fi , (qn+1 , Fi , zn+1 ) ∈ Ci et (q̃n+1 , φ̃n+1 , zn+1 ) ∈ Ci , où
d
zn+1 = Z(qn+1 d
). Nous notons par qnd le prédécesseur de qn+1 dans le cycle Fi -indéterminé,
σn+1 ,gn+1 ,Yn+1
sur la transition qnd −−−−−−−−−→ qn+1 d
∈ E d . Alors, pour toute valuation vn+1 ∈ zn+1 , il
existe une valuation vn ∈ zn = Z(qnd ), une paire d’éléments (qn , Fi ), (q̃n , φ̃n ) ∈ Dis(qnd )
et une paire de traces temporisées ωn+1 et ω̃n+1 , telles que :
• (qn , Fi , zn ) ∈ Ci et (q̃n , φ̃n , zn ) ∈ Ci ;
ωn+1 ω̃n+1
– (qn , vn ) (qn+1 , vn+1 ) et (qn , vn ) (qn+1 , vn+1 ) ;
• P (ωn+1 ) = P (ω̃n+1 ) = ’d.σn+1 ’, où d ∈ R+ .
Preuve : Nous allons utiliser la technique employée pour la preuve du Lemme 2.
Par construction du diagnostiqueur, il existe deux chemins de transitions dans
uo uo σ 1 ,g 1 σ 2 ,g 2 σ k ,g k σn+1 ,ηn+1 ,Yn+1
S, (qn , Fi , zn ) −−−−→ (qn1 , Fi , zn1 ) −−
uo uo uo uo
−−→ . . . −−−−→ (qnk , Fi , znk ) −−−−−−−−−→
0 0
uo uo σ̃ 1 ,g̃ 1 σ̃ 2 ,g̃ 2 σ̃ k ,g̃ k 0 0 0
(qn+1 , Fi , zn+1 ) dans Ci et (q̃n , φ̃n , zn ) −−−−→ (q̃n1 , φ̃1n , z̃n1 ) −−
uo uo uo uo
−−→ . . . −−−−→ (q̃nk , φ̃kn , z̃nk )
σn+1 ,ηn+1 ,Yn+1 0
−−−−−−−−−→ (q̃n+1 , φ̃n+1 , zn+1 ) dans Ci , tel que φ̃n , φ̃1n , . . . , φ̃kn , φ̃n+1 6= Fi .
0
Par construction du prédicat ηn+1 , nous avons ηn+1 ⊆ znk et ηn+1 ⊆ z̃nk . Soient
k e 0
(qn , vn+1 ) et (q̃nk , vn+1
e e
) deux états tels que vn+1 e
∈ ηn+1 et vn+1 = vn+1 [Yn+1 ← 0]. Alors,
0 ∗
il existe une paire de traces temporisées ωu , ωu ∈ (Σuo ×R+ ) et une paire d’états, (qn , vn )
ω ω0 0
et(q̃n , ṽn ), où vn ∈ zn , ṽn ∈ z̃n , (qn , vn ) u (qnk , vn+1
e
) et (q̃n , vn ) u (q̃nk , vn+1
e
).
Puisque les transitions sur les événements non observables ne réinitialisent pas les
horloges, (hypothèse H2 ), alors il existe d, d˜ ∈ R+ tel que vn+1
e e
= vn + d et vn+1 ˜
= ṽn + d.
Par conséquence, ṽn = vn + (d − d)˜ (nous supposons que d − d˜ ≥ 0, sinon, nous inversons
les termes de l’égalité).
L’état (q̃n , ṽn ) est accessible depuis (q̃n , vn ) sur l’écoulement de d − d˜ u.t. ;
d−d˜ ω̃ ˜ 0 ’.
i.e.,(q̃n , vn ) −−→ (q̃n , ṽn ). Par conséquence, (q̃n , vn ) u (q̃ k , v e ), où ω̃u = ’(d − d).ω
n n+1 u
En plus, il est clair que temps(ωu ) = temps(ω̃u ).
167
Annexe B. Preuves
ωn+1
Soient ωn+1 =’ωu .σn+1 ’ et ω̃n+1 = ’ω̃u .σn+1 ’. Il est clair que (qn , vn ) (qn+1 , vn+1 ) et
ω̃n+1
que (q̃n , vn ) (q̃n+1 , vn+1 ). En plus, P (ωn+1 ) = P (ω̃n+1 )=’temps(ωu ).σn+1 ’.
Lemme 6
Soit qnd un sommet du diagnostiqueur appartenant à un cycle Fi -indéterminé et
(qn , Fi ), (q̃n , φ̃n ) ∈ Dis(q d ), tels que φ̃n 6= Fi , (qnp , Fi , zn ) ∈ Ci , (q̃nq , φ̃qn , zn ) ∈ Ci et
zn = Z(qnd ).
0
Alors, étant donné un entier naturel α ≥ 0 et ∀vn,p ∈ zn , il existe une valuation
d’horloges vn,p ∈ zn et une paire de traces temporisées ω , ω̃ α telles que :
α α
ωα
α
1. L’exécution (qnp , vn,p ) 0
(qnp , vn,p ) fait évoluer S α fois dans le cycle Ci ,
0 ω̃ α
α
2. L’exécution (q̃nq , vn,p ) 0
(q̃nq , vn,p ) fait évoluer S dans le cycle Ci ,
3. P (ω α ) = P (ω̃ α ).
Preuve :
Nous prouvons ce lemme par induction sur le nombre de cycles α, effectuée par une
exécution de S dans Ci .
Base : α = 0, cas trivial. ω 0 et ω̃ 0 sont égales à la trace vide.
Induction : nous supposons que la propriété de l’induction est vérifiée pour l’ordre
order α, nous montrons qu’elle est aussi vérifiée pour l’ordre α + 1.
α
D’après l’hypothèse de l’induction, il existe une valuation vn,p ∈ zn et une paire de
ωα
traces temporisées ω α , ω̃ α telles que l’exécution (qnp , vn,p
α
) (qnp , vn,p
0
) fait évoluer S, pour
0 ω̃ α
α fois, dans le cycle Ci , l’exécution (q̃nq , vn,p
α
) (q̃nq , vn,p
0
) fait évoluer S dans le cycle Ci et
α α
P (ω ) = P (ω̃ ).
Nous supposons que lorsque le système effectue un cycle d’exécution dans Ci , il effec-
σ1 ,g1 ,Y1 σn−1 ,gn−1 ,Yn−1
tue au même temps p cycles dans le diagnostiqueur q1d −−−−→ q2d . . . qn−1
d
−−−−−−−−−→ qnd
σn ,gn ,Yn
−−−−−→ q1d , p ≥ 1.
α d
Soit vk+1,j une valuation d’horloges dans Z(qk+1 ), où j ∈ {1, . . . , p} and k ∈
d d
{1, . . . , n}, qn+1 = q1 .
168
Annexe B. Preuves
α
Selon le Lemme 5, il existe vk,j ∈ zk , une paire d’éléments (qkj , Fi ), (q̃kj , Fi ) ∈ Dis(qkd
j j
et une paire de traces ωk+1 et ω̃k+1 , telles que :
1. (qkj , Fi , zk ) ∈ Ci et (q̃kj , φ̃k , zk ) ∈ Ci ;
j j
ωk+1 ω̃k+1
2. (qkj , vk,j
α
) j
(qk+1 α
, vk+1,j ) et (q̃kj , vk,j
α
) j
(q̃k+1 α
, vk+1,j );
j j
3. P (ωk+1 ) = P (ω̃k+1 ) = ’djk+1 .σk+1 ’, où djk+1 ∈ R+ .
p
Par la construction des traces ωnp , ω̃np , ωn−1 p
,ω̃n−1 ,. . ., ω1p ,ω̃1p , ωnp−1 , ω̃np−1 . . ., ω21 , ω˜21 ,ω11 ,
ω˜11 à partir des valuations vn,p
α
, nous concluons qu’il existe une valuation vn,p α+1
et une
1 p
α+1 ω1 ω1 ωn−1 p
p
ωn
exécution (qnp , vn,p ) (q11 , v1,1
α
) 2 (q21 , v2,1
α
) . . .(qn1 , vn,1
α
) (qn−1 α
, vn−1,p ) ... (qnp , vn,p
α
),
faisant évoluer S dans le cycle Ci .
Soit ω = ’ω11 .ω21 . . . . .ωn1 .ω12 . . . . .ωnp ’ et ω̃ = ’ω̃11 .ω̃11 . . . . .ω̃n1 .ω̃12 . . . . .ω̃np ’. Il est clair que
α+1 ω 00 α+1 ω 0
P (ω) = P (ω̃) et que (qnp , vn,p ) (qnp , vn,p α
), et (q̃nq , vn,p ) (q̃nq , vn,p α
).
Soient ω α+1 =’ω.ω α ’ et ω̃ α+1 =’ω̃.ω̃ α ’. Il est clair que P (ω α+1 ) = P (ω̃ α+1 ). En
ω α+1
plus, (qnp , vn,p
α+1
) (qnp , vn,p
0
) fait évoluer S, α + 1 fois, dans le cycle Ci et l’exécution
00 ω̃ α+1
(q̃nq , vn,p
α+1
) 0
(q̃nq , vn,p ) fait évoluer S dans le cycle Ci .
Preuve :
(1) ⇒ (2) : Nous supposons
h qu’il existe
i une exécution de Hi,i , sur une trace temporisée
ω, qui atteint l’état ((q1 , q2 ), v1 v2 ), telle que ω contient un défaut de l’ensemble Fk .
D’après la proposition 3, il existe une paire d’exécutions de Hi et Hi , respectivement
sur les traces temporisées ω1 et ω2 , menant aux états (q1 , v1 ) et (q2 , v2 ), telles que
P (ω1 ) = P (ω2 ). D’après la proposition 2, nous avons ω1 ∈ L0 ∪ Li et ω2 ∈ L − Li .1 .
1
Puisque chaque événement non observable σki ∈ Σi , existant dans la trace ω1 , correspond à un évé-
nement σk dans Σ, nous supposons un passage implicite entre ces deux événements pour que l’inclusion
ω1 ∈ L0 ∪ Li soit correcte syntaxiquement.
169
Annexe B. Preuves
(2) ⇒ (1) : Dans le sens inverse, nous supposons qu’il existe une paire de traces ω1 ∈ Lk
et ω2 ∈ L − Lk , telle que P (ω1 ) = P (ω2 ). En effet, ω1 ∈ L(Hk ) et ω2 ∈ L(Hk ). D’après la
proposition 3, il existe une exécution de Hk,k sur une trace temporisée ω qui correspond
à la synchronisation des exécutions de Hk et Hk , sur respectivement, ω1 et ω2 . Puisque
ω1 contient un défaut de l’ensemble Fk et Hk,k = Hk ⊗ Hk , alors, la trace ω contient une
défaut de l’ensemble Fk .
θ
Théorème 4. La fonction d’analyse d’accessibilité, appliquée aux AHRs Hi,i , pour tout
i ∈ {1, . . . , m}, s’arrête au bout d’un temps fini.
Preuve : Afin de prouver l’arrêt de cet algorithme, nous divisons son exécution sur
0
deux étapes : (1) dans la première étape, l’algorithme explore la restriction Hi,i ⊗ TB
θ
de Hi,i , i ∈ {1, . . . , m}. Cette partie de l’algorithme suspend le calcul du successeur de
chaque état symbolique atteint suite à une transition sur un événement de défaut. Nous
plaçons cet état symbolique dans un ensemble intermédiaire, appelé EN _AT T EN T E,
pour qu’il soit traité ultérieurement.
(2) Dans la seconde étape de l’exécution de la fonction, nous initialisons l’ensemble
A_T RAIT ER par le contenu de l’ensemble EN _AT T EN T E, puis nous exécutions
l’algorithme pour explorer les successeurs des états symboliques dans EN _AT T EN T E,
qui n’ont pas été explorés lors de la première étape. Nous pouvons établir, facilement,
que l’exécution de ces deux étapes est équivalente à une exécution de la fonction.
La l’arrêt de l’exécution de la première étape est garantie. Les successeurs des états
symboliques sur des transitions de défauts ne vont pas être explorés. Par conséquence,
0
l’algorithme va effectuer l’analyse d’accessibilité de la restriction Hi,i ⊗ T B θ de Hi,i
θ
.
0
Puisque Hi,i est un AHR initialisé, (d’après la proposition 4), cette première étape
170
Annexe B. Preuves
Preuve :
(1) ⇒ (2) : Nous supposons qu’il existe i ∈ {1, . . . , m} et une exécution sur la trace
θ
ω
b dans Hi,i q , v), où qb ∈ Mi,i et v est une valuation de Xi,i . Puisque
, atteignant l’état (b
θ
chaque transition vers un sommet marqué dans Hi,i se produit sur l’événement µ, alors, la
trace ωb admet comme suffixe l’événement µ. Puisque toutes les conditions de garde dans
θ
les transitions de Hi,i ont la forme y k ≥ θk , k ∈ {1, . . . , m},alors il existe k ∈ {1, . . . , m},
tel que v(y k ) ≥ θk . Par conséquent, la trace ω b contient nécessairement un défaut de
l’ensemble Fk .
θ
Puisque Hi,i = Hi,i ⊗ T B θ , nous supposons que le sommet qb correspond à une paire
(qi,i , qM ), où qi,i est un sommet de l’AHR Hi,i . Soit ω une trace temporisée dont l’exé-
cution atteint l’état (qi,i , v) (la trace ω est obtenue en éliminant l’événement µ de ω b ).
Puisque ω contient un défaut de l’ensemble Fk , d’après le lemme 7, il existe une paire de
traces ω1 ∈ Lk et ω2 ∈ L − Lk , telle que P (ω1 ) = P (ω2 ), et atteignant h respectivement,
i
les états (q1 , v1 ) dans Hi et (q2 , v2 ) dans Hi , où qi,i = (q1 , q2 ) et v = v1 v2 . Deux cas
peuvent se présenter :
171
Annexe B. Preuves
172
Bibliographie
Alla, H. et R. David. 1998, «Continuous and hybrid petri nets», Journal of Circuits,
Systems and Computer, vol. 8, no 1, p. 159–188.
Allam, M. et H. Alla. 1996, «From hybrid petri nets to hybrid automata», Journal
européen des systèmes automatisés, vol. 320, no 9-10, p. 1165–1185.
Alur, R. 1999, «Timed automata», Theoretical Computer Science, vol. 126, p. 183–235.
Bagnara, R., E. Ricci, E. Zaffanella et P. Hill. 2002, «Possibly not closed convex po-
lyhedra and the parma polyhedra library», dans Int. Symp. Volume 2477 of LNCS.,
Springer, p. 213–229.
Barbuti, R. et L. Tesei. 2004, «Timed automata with urgent transitions», Acta Inf.,
vol. 40, no 5, p. 317–347.
173
Bibliographie
Bouyer, P. et F. Chevalier. 2005, «Fault diagnosis using timed automata», dans Foun-
dations of Software Science and Computational Structures : 8th International Confe-
rence, FOSSACS 2005, Held as Part of the Joint European Conferences on Theory
and Practice of Software, ETAPS 2005, Springer-Verlag, p. 4–8.
Cassez, F. et O. H. Roux. 2006, «Structural translation from time petri nets to timed
automata», Journal of Software and Systems, vol. 79, p. 1456–1468.
174
Bibliographie
Chen, Y. et G. Provan. 1997, «Modeling and diagnosis of timed discrete event systems-
a factory automation example», dans The American Control Conference, New Mexico,
p. 31–36.
Chow, E. et A. Wilsky. 1984, «Analytical redundancy and the designe of robust failure
detection system», IEEE transactions on Automatic and Control, vol. 29, no 7, p.
603–614.
David, R. et H. Alla. 1989, Du Grafcet aux réseaux de Petri, Hermes Science Publications,
Paris.
David, R. et H. Alla. 2004, Discrete, Continuous, and Hybrid Petri Nets, Springer, Berlin
Heidelberg.
175
Bibliographie
Desel, J., W. Reisig et G. Rozenberg. 2004, «Lectures on concurrency and petri nets :
advances in petri nets», Lecture Notes on Concurrency and Petri Nets, p. 87–124.
Feng, S. N., F. Zhao, G. Biswas et E. Hung. 2000, «Fault isolation in hybrid systems
combining model based diagnosis and signal processing», dans Proceedings of the 4th
IFAC Symp. SAFEPROCESS, p. 1074–1079.
Frehse, G. 2005, «Phaver : Algorithmic verification of hybrid systems past hytech», dans
Fifth International Workshop on Hybrid Systems : Computation and Control (HSCC),
p. 258–273.
176
Bibliographie
Ghazel, M. 2005, Surveillance des Systèmes à Evénements Discrets à l’Aide des Réseaux
de Petri T-Temporels, thèse de doctorat, l’Ecole Centrale de Lille et l’Université des
Sciences et Technologies de Lille.
Ghazel, M., Toguéni et M. Bigang. 2005, «A monitoring approach for discrete events
systems based on a timed perti net model», dans 16th IFAC World Congress.
Guéguen, H. et J. Zaytoon. 2004, «On the formal verification of hybrid systems», Control
Engineering Practice, vol. 12, no 10, p. 1253–1267.
Henzinger, T., P. Kopke, A. Puri et P. Varaiya. 1998, «The what’s decidable about hybrid
automata ?», Journal of Computer and System Sciences, vol. 57, p. 94–124.
Henzinger, T. A. 1996, «The theory of hybrid automata», Hybrid Systems II, LNCS, vol.
999, p. 278–292.
Isermann, R. 1984, «Process fault detection based on modeling and estimation methods
– a survey», Automatica, vol. 20, no 4, p. 387–404.
Jiang, S., Z. Huang, V. Chandra et R. Kumar. 2000, «A polynomial algorithm for testing
diagnosability of discrete event systems», IEEE Transactions on Automatic Control,
vol. 46, p. 1318–1321.
177
Bibliographie
Karsai, G., S. Abdelwahed et G. Biswas. 2003, «Integrated diagnosis and control for
hybrid dynamic systems», .
Kurovszky, M. 2002, Etude des sytèmes dynamiques hybrides par représentation d’état
discrète et automate hybride, thèse de doctorat, L’université Joseph Fourier, Grenoble.
Lunze, J. 2000, «Diagnosis of quantised systems», dans 4th IFAC Symposium on Fault
Detection. Supervision and Safety for Technical Processes, SAFEPROCESS’00, p. 28–
39.
Müller, O. et T. Stauner. 2000, «Modelling and verification using linear hybrid automata
- a case study», Mathematical and Computer Modelling of Dynamical Systems, vol. 6,
no 1, p. 71–89.
178
Bibliographie
Mosterman, J. 2001, «Diagnosis of physical systems with hybrid models using parame-
terised causality», dans Hybrid Systems : Computation and Control, 4th International
Workshop, HSCC’01, Rome, Italia, p. 447–458.
Mosterman, P. J. 1997, Hybrid Dynamic Systems : a Hybrid Bond Graph Modeling Pa-
radigm and its Application in Diagnosis, thèse de doctorat, Vanderbilt University.
Roux, O. et V. Rusu. 1996, «Uniformity for the decidability of hybrid automata», dans
Proceedings of the 8th Conference on COmputerAided Veri CAV’96, volume 1145 of
LNCS, p. 301–316.
179
Bibliographie
Toguyeni, A. 1992, Surveillance et diagnostic en ligne dans les ateliers flexibles de l’in-
dustrie manufacturière, thèse de doctorat, Université de Lille.
Tripakis, S. 2002, «Fault diagnosis for timed automata», dans Proceedings of the 7th
International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Sys-
tems, FTRTFT’02, Springer-Verlag, London, UK, ISBN 3-540-44165-4, p. 205–224.
Villemeur, A. 1988, Sûreté de fonctionnement des systèmes industriels, vol. 67, Edition
EYROLLES, Collection DER-EDF.
Willsky, A. 1976, «A survey of design methods for failure detection in dynamic systems»,
Automatica, vol. 12, no 6, p. 601–611.
Xue, F., D. Zheng et L. Yan. 2005, «Fault diagnosis of distributed discrete event systems
using obdd», IEEE Transactions On Automatic Control, vol. 16, no 3, p. 431–448.
180
Yovine, S. 1997, «Kronos : A verification tool for real-time systems», International Jour-
nal on Software Tools for Technology Transfer, vol. 1, p. 123–133.
Yovine, S. 1998, «Model checking timed automata», dans European Educational Forum :
School on Embedded Systems, Springer-Verlag, p. 114–152.
Abstract: In this thesis, we study the diagnosis of timed systems and a class of
hybrid dynamic systems. A diagnosis approach for timed systems, using timed automata
as system model, is given. This approach is based on the, off-line, construction of a timed
automaton called diagnoser. The diagnoser allows to estimate unobservable failure occur-
rences, given a record of timed observable events, generated by the system. A systematic
method for verifying the diagnosability of the studied model is also given. In the hybrid
dynamic systems context, a diagnosis approach based on rectangular hybrid automata, is
given. This approach consists on the execution of an on-line diagnosis procedure, which
estimates, on-the-fly, the system state as well as failure occurrences. A diagnosability
verification method of the studied hybrid model is provided.
Keywords : diagnosis, timed systems, hybrid dynamic systems, timed automata, rec-
tangular hybrid automata, reachability analysis.