Analyses de modèles de diagnostic par des méthodes formelles

Étude formelle de propriétés relatives au diagnostic (diagnosticabilité, identifiabilité,...) dans les systèmes dynamiques (discrets, continus, hybrides).


La mise en œuvre de moniteurs de surveillance, de diagnostiqueurs ou de systèmes de protection contre les défauts est fortement compromise dès lors que les besoins ne sont pas pris en compte dès la phase de conception du système. Ces besoins s'expriment en termes de diagnosticabilité, d'identifiabilité et de reconfigurabilité / réparabilité. Ces propriétés permettent de connaître à l'avance quels défauts ou états le diagnostiqueur sera en mesure de discriminer avec l'instrumentation en place et quels défauts le contrôleur sera en mesure de compenser avec les actionneurs prévus. En outre, ces propriétés permettent d'identifier l'ensemble de capteurs et actionneurs supplémentaires qui sont nécessaires pour atteindre le degré de diagnosticabilité et/ou de reconfigurabilité / réparabilité requis, voire même de procurer des capacités d'auto-guérison dans le cadre des systèmes autonomes.



Les recherches menées par l'équipe DISCO couvrent la diagnosticabilité des systèmes continus, avec un accent sur les systèmes non-linéaires incertains, des systèmes à événements discrets, et des systèmes hybrides. Une définition unifiée de la diagnosticabilité, indépendante du type de système, a été établie sur la base de la notion de signature. L'identifiabilité est également étudiée comme une propriété essentielle lorsque les méthodes d'estimation des paramètres sont utilisées pour le diagnostic. Des ponts avec la diagnosticabilité sont à l’étude. Une attention particulière est portée aux systèmes distribués, souvent constitués en réseau de composants. On étudie les propriétés locales afin d'en déduire la diagnosticabilité globale, permettant dans un deuxième temps le déploiement automatique d'un protocole entre agents diagnostiqueurs locaux dont la capacité de diagnostic résultante est optimale.




FOCUS


Diagnosticabilité fonctionnelle et liens avec l'identifiabilité

Contrairement à la définition classique, la diagnosticabilité fonctionnelle exploite les propriétés temporelles des relations de redondance analytiques liées aux différents défauts et appelées signatures fonctionnelles. La diagnosticabilité fonctionnelle est étroitement liée à la notion d'identifiabilité qui garantit que les paramètres d'un modèle peuvent être déduits de manière univoque à partir des mesures des sorties du système. Ce lien a permis de fournir une condition suffisante pour tester la diagnosticabilité fonctionnelle d'un système. La diagnosticabilité fonctionnelle a été étendue au cadre ensembliste et liée à l'identifiabilité ensembliste. L'impact de l'identifiabilité ensembliste sur les propriétés des solutions obtenues par estimation de paramètres a été analysé.



Diagnosticabilité et le diagnostic de motifs de fautes

Une analyse de diagnosticabilité est une analyse a priori faite sur le système qui vise à garantir que lorsque le système sera en opération, si une faute a lieu, une fonction de diagnostic pourra la déterminer avec certitude et en un temps fini. L'analyse de diagnosticabilité dans les systèmes à événements discrets s'appuie sur la recherche d'une paire critique i.e deux évolutions du système ayant la même trace observable que l'évolution observée telle que la faute est présente dans une de ces deux évolutions et absente dans l'autre. Le diagnostic est formellement caractérisé par la notion de concordance de motif et posé comme un problème d'atteignabilité résolu par model checking. La recherche de paires critiques repose sur la construction d'un twin-plant et sur une recherche de cycle dans le twin-plant formulée comme un problème d'atteignabilité en Logique Temporelle Linéaire.



Diagnosticabilité des systèmes hybrides

La méthode détermine une première abstraction discrète de la dynamique continue d'un automate hybride et vérifie la diagnosticabilité de l'automate résultant par les méthodes standard pour les systèmes à événements discrets. Celles-ci vérifient s'il existe un contre-exemple, c'est-à-dire une paire critique de trajectoires ayant la même projection observable, l'une avec défaut et l'autre normale. Si aucun contre-exemple n'est trouvé, alors l'abstraction est diagnosticable, ce qui confère la propriété au système hybride initial. Dans le cas contraire, le contre-exemple est analysé et guide l'abstraction courante pour qu'elle soit affinée. Cette méthode construit ainsi une hiérarchie incomplète d'abstractions pour la diagnosticabilité des systèmes hybrides.