| Přispěvatelé: |
Équipe Verification de Systèmes Temporisés Critiques (LAAS-VERTICS), Laboratoire d'analyse et d'architecture des systèmes (LAAS), Université Toulouse - Jean Jaurès (UT2J)-Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées-Université Fédérale Toulouse Midi-Pyrénées-Centre National de la Recherche Scientifique (CNRS)-Université Toulouse III - Paul Sabatier (UT3), Université Fédérale Toulouse Midi-Pyrénées-Institut National des Sciences Appliquées - Toulouse (INSA Toulouse), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse - Jean Jaurès (UT2J)-Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées, INSA, HLADIK Pierre-Emmanuel |
| Popis: |
National audience; We study the behaviour of Discrete Event Systems (DES) subjectto strong temporal constraints. We are more particularly interested in theformal verification of properties on the timed languages associated with theirexecutions. 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 timeduring which transitions stay enabled.Our goal is to use and extend techniques borrowed from model-checkingin order to check properties related to the diagnosability of a system. To thisend, we study properties on the intersection of the timed languages of systems.Our approach is based on the definition of a new composition operator, thatwe call synchronous product, that constrain different transitions to fire at thesame 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 oftheir state spaces.Our main contribution is the definition of a new formal model, calledProduct TPN (PTPN), that includes our notion of synchronous product inits syntax. We show how to extend the notion of State Class Graphs toPTPN and use this construction to check the diagnosability of single faultson TPN. We also study the diagnosability of more complex behaviours, expressedusing 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 lavérification de propriétés liées aux langages associés à leurs exécutions. Dansce 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 domainedu model-checking afin de répondre à des questions de diagnosticabilité.Pour ce faire, nous cherchons à vérifier des propriétés liées à l’intersectionentre les langages temporels (le comportement) de différent systèmes. Notreapproche repose sur la définition d’une nouvelle opération de produit synchroneentre TPN qui nous permet d’utiliser des techniques d’analyse plusdirectes. Ceci nous permet, en particulier, d’éviter de devoir calculer directementl’intersection entre langages au niveau des espaces d’état des systèmes.Notre contribution principale est la définition d’un nouveau modèle, lesProduct TPN (PTPN), qui internalise notre concept de produit synchroneentre transitions. Nous proposons une extension de la notion de graphes declasses au cas des PTPN et utilisons ce modèle pour vérifier la propriété dediagnosabilité sur les TPN dans le cas de fautes simples, mais également pourla diagnosticabilité de scénarios plus complexes, décrit sous la forme de motifs. |
