Diagnosability and diagnosabilisation of time patterns in time Petri nets
Diagnosticabilité et diagnosticabilisation de motifs temporels dans les réseaux de Petri temporels
Résumé
Diagnosability is the property of a system to produce sufficient observations (via sensors) to differentiate nominal from faulty behavior. It is possible for a diagnosable system to produce a certain diagnosis for a given fault, since the observable information returned by the system differs according to whether or not a fault has occurred. Verifying such a property on a system is therefore an important step in the process of building fault detection and isolation algorithms. This problem has been the subject of numerous studies in atemporal Discrete Event Systems (DES) (STL, Petri nets, etc.) and in time DES models (timed automata, time Petri nets, etc.), whether for simple faults (modeled by the occurrence of a single event) or for more complex behaviors called fault patterns.
In this work, we propose a method for analyzing the diagnosability of time Petri nets for a new type of fault called time pattern. Time patterns consist of the occurrence of different temporally constrained events. The method is based on a polyhedral abstraction of time Petri net language prefixes, which is the first contribution of this thesis. The second contribution of this work is a diagnosability analysis method, which makes it possible to check whether a system is diagnosable for a time pattern, and to provide structural explanations for non-diagnosability. This method is based on the analysis of polyhedra of the abstraction presented, which are divided into different zones sharing common diagnosis properties. From this analysis of zones is synthesized a graph grouping together the various sources of ambiguity in the different executions of the system. The last contribution of this work is a verification method for the time diagnosabilization problem, which consists in! parameterizing some bounds of the static time intervals of the initial time Petri net and finding values for these parameters for which the net thus generated is diagnosable for the pattern under study. We propose a method to check diagnosabilization that guarantees certain properties of the generated Petri net. This verification is based on the previously mentioned polyhedral abstraction, and consists in the construction of linear constraint sets. Verification of the existence of solutions can then be carried out using an SMT solver.
La diagnosticabilité est la propriété d'un système de produire suffisamment d'observations (par l'intermédiaire de capteurs) pour différencier les comportements nominaux des comportements fautifs. Il est possible pour un système diagnosticable pour une faute donnée (ou défaut) de produire un diagnostic certain, les informations observables retournées par le système étant différentes selon si une faute a eu lieu ou non. Vérifier une telle propriété sur un système est donc une étape importante dans le processus de construction d'algorithmes de détection et d'isolation de telles fautes. Ce problème a fait l'objet de multiples études dans les Systèmes à Événements Discrets (SED) atemporels (STL, réseaux de Petri, etc.) et dans les modèles SED temporels (automates temporisés, réseaux de Petri temporels, etc.), que ce soit pour des fautes simples (modélisées par l'occurrence d'un unique événement) ou pour des comportements plus complexes appelés motifs de faute.
Dans ce travail nous proposons une méthode d'analyse de diagnosticabilité de réseaux de Petri temporels pour un nouveau type de défaut appelé motif temporel. Les motifs temporels consistent en l'occurrence de différents événements contraints temporellement. Cette méthode se base sur une abstraction des préfixes du langage d'un réseau de Petri temporel sous forme de polyèdres qui constitue la première contribution de cette thèse. La seconde contribution de ce travail est une méthode d'analyse de diagnosticabilité, qui permet de vérifier si un système est diagnosticable pour un motif temporel, et de fournir des explications structurelles de non-diagnosticabilité le cas échéant. Cette méthode se base sur l'analyse des polyèdres issus de l'abstraction présentée, qui sont découpés en différentes zones partageant des propriétés de diagnostic communes. De cette analyse de zones est synthétisé un graphe regroupant les différentes sources d'ambiguïtés dans les différentes exécutions du système étudié. La dernière contribution de ce travail est une méthode de vérification pour le problème de diagnosticabilisation temporelle qui consiste à paramétrer les intervalles statiques du réseau de Petri temporel initial et à trouver des valeurs des paramètres pour lesquelles le réseau ainsi généré est diagnosticable pour le motif étudié. Nous proposons une méthode de vérification de cette propriété garantissant certaines propriétés sur le réseau de Petri engendré. Cette méthode de vérification se base sur l'abstraction polyédrique précédemment citée, et consiste en la construction d'ensembles de contraintes linéaires. La vérification de l'existence de solution peut être réalisée par la suite à l'aide d'un solveur SMT.
Origine : Fichiers produits par l'(les) auteur(s)