Modeling and Analytical Evaluation of the Response Time of Distributed Control Systems using Petri nets and Dioid Algebra
Louis Bal Dit Sollier · HAL (Le Centre pour la Communication Scientifique Directe) · 2024
La problématique abordée dans cette thèse concerne avant tout l'évaluation analytique d'une borne du temps de réponse pour un système de contrôle distribué, dans un contexte industriel critique. La téléologie des travaux consiste donc à prouver cette borne par une méthode qui doit se fonder sur deux aspects : une modélisation par un formalisme graphique (pouvant être simulé), et un calcul découlant de descriptions mathématiques du modèle. Dans la littérature, les méthodes classiques de vérifications formelles engendrent de l'explosion combinatoire : nous nous tournons dans ces travaux vers les méthodes algébriques.Au sein de ces dernières, l'algèbre tropicale fournit des éléments intéressants pour la description des Graphes d'Événements Temporisés (GET), puisque leur représentation est linéaire dans cette algèbre. Toutefois, cette classe de réseau de Petri ne permet de modéliser que des phénomènes de synchronisation et de parallélisme. Bien que ces phénomènes soient communs dans un système de contrôle, ils ne constituent qu'une partie de ce qu'il est intéressant de modéliser. Par conséquent, après avoir démontré la faisabilité d'une approche basée sur la description algébrique de modèles GET en utilisant le dioïde des séries formelles, nous proposons de construire un dioïde similaire pour la description des Réseaux de Petri Colorés Temporisés (RPCT), une classe beaucoup plus étendue car haut-niveau et interprétable. En suivant le théorème de Kleene-Schützenberger, nous construisons les séries formelles colorées (SFC), et, par preuve de leur rationalité, qu'elles réalisent le comportement d'une sous-classe de RPCT linéaires dans l'algèbre tropicale. Par ailleurs, nous explicitons les liens existants entre un modèle RPCT et sa mise en trajectoires SFC.Ces SFC sont construites autour d'un ordre total imposé arbitrairement sur l'ensemble des couleurs d'un modèle, et interprété comme l'ordre des priorités. On peut ainsi exprimer les décalages de couleurs et rendre le comportement d'un modèle RPCT complètement déterministe (même pour le cas non-linéaire).Les trajectoires des SFC permettent d'établir des lois/fonctions/algorithmes réalisant des opérations non-linéaires dans l'algèbre tropicale et induites par des phénomènes autres que la synchronisation ou le parallélisme (comme le conflit, la concurrence, le partage de ressources, la synchronisation partielle, les multiplicités…). Ces opérations non-linéaires expriment en particulier les décalages d'ordre induits sur les trajectoires. Sans être exhaustif, nous présentons différents cas de gestion de mécanismes non-linéaires pour montrer que l'utilisation des SFC offre des capacités plus larges que celles obtenues par les séries classiques associées aux GET. Nous donnons enfin quelques exemples de calculs de délais dans des modèles colorés pouvant être intégrés dans la méthode. Notamment, nous modélisons un réseau commuté en RPCT, et proposons sa mise en trajectoires. En utilisant des hypothèses de prédictibilités, nous calculons alors à partir de cette dernière le temps de voyage bout-en-bout dans le pire scénario.Par ailleurs, l'approche proposée est modulaire. Le comportement des parties linéaires peut être calculé via la théorie classique des dioïdes, développée à travers les GET, et assurant la simplification de tout modèle linéaire en une fonction de transfert, cette dernière étant la plus petite solution du système d'équations linéaires associée au modèle. Le comportement des parties non-linéaires peut lui être calculé par les nouvelles opérations que nous définissons (convolution, algorithmes itératifs, réductions de trajectoires, réordonnancements…). Le concept de trajectoire assure alors l'interopérabilité entre les différentes parties : pour toute opération prenant en entrées des trajectoires, et en construisant en sorties, il est possible de considérer cette opération de façon isolée au sein du calcul du comportement d'un système.