Synchronous Product of Time Petri Nets and its Applications to Fault-Diagnosis
Produit synchrone des réseaux de Petri temporels et ses applications au diagnostic de défauts
Résumé
We study the behaviour of Discrete Event Systems (DES) subject
to strong temporal constraints. We are more particularly interested in the
formal verification of properties on the timed languages associated with their
executions. In this context, we focus on DES modelled using Time Petri Nets
(TPN), an extension of classical Petri nets in which we can constrain the time
during which transitions stay enabled.
Our goal is to use and extend techniques borrowed from model-checking
in order to check properties related to the diagnosability of a system. To this
end, we study properties on the intersection of the timed languages of systems.
Our approach is based on the definition of a new composition operator, that
we call synchronous product, that constrain different transitions to fire at the
same time. This allows us to analyse the product of systems more directly,
without the need to compute the intersection of their language at the level of
their state spaces.
Our main contribution is the definition of a new formal model, called
Product TPN (PTPN), that includes our notion of synchronous product in
its syntax. We show how to extend the notion of State Class Graphs to
PTPN and use this construction to check the diagnosability of single faults
on TPN. We also study the diagnosability of more complex behaviours, expressed
using patterns of events, and explore a restricted case of timed pattern.
Cette thèse porte sur l’étude des Systèmes à Événements Discrets
(SED) soumis à des contraintes temporelles fortes, et plus précisément sur la
vérification de propriétés liées aux langages associés à leurs exécutions. Dans
ce contexte, nous nous concentrons à l’étude des réseaux de Petri temporels
(TPN) comme modèle pour la spécification des SED.
L’objectif général est d’utiliser et d’étendre des méthodes issues du domaine
du model-checking afin de répondre à des questions de diagnosticabilité.
Pour ce faire, nous cherchons à vérifier des propriétés liées à l’intersection
entre les langages temporels (le comportement) de différent systèmes. Notre
approche repose sur la définition d’une nouvelle opération de produit synchrone
entre TPN qui nous permet d’utiliser des techniques d’analyse plus
directes. Ceci nous permet, en particulier, d’éviter de devoir calculer directement
l’intersection entre langages au niveau des espaces d’état des systèmes.
Notre contribution principale est la définition d’un nouveau modèle, les
Product TPN (PTPN), qui internalise notre concept de produit synchrone
entre transitions. Nous proposons une extension de la notion de graphes de
classes au cas des PTPN et utilisons ce modèle pour vérifier la propriété de
diagnosabilité sur les TPN dans le cas de fautes simples, mais également pour
la diagnosticabilité de scénarios plus complexes, décrit sous la forme de motifs.
Origine : Fichiers produits par l'(les) auteur(s)