Search

This thesis consists of three parts. The first one is devoted to the verification of Petri nets, the second one to the verification of recursive Petri nets which extend Petri nets, and the final one aims at combining active learning and verification.A Petri net can be analyzed by computing and studying its Clover, that is the canonical representation of the downward over approximation of its reachability set. Using the Karp-Miller algorithm one can compute the Clover, but this algorithm is very inefficient and moreover, its original proof of correctness is not satisfying. Many variations of the original Karp-Miller algorithm computing the clover exist, but some are incomplete, others introduced an unknown supplementary memory size (possibly Ackermannian) and proofs are often heavy. Our first contribution is the design of a complete algorithm in such a way that we can theoretically bound the additional memory requirements.The key idea of this algorithm is the introduction of a new concept, called acceleration. More precisely using accelerations, we were able:1. to simplify the proof of correctness of the Karp-Miller algorithm; 2. to present the first simple modification of the original but incomplete Minimal Coverability Tree algorithm;3. to prove that the supplementary memory needed by our algorithm is elementary (2-EXPSPACE);4. to implement a prototype MinCov, showing experimentally that it is the most efficient one compared to other tools computing the Clover.In the early two-thousands, Recursive Petri nets (RPN) have been introduced in order to model distributed planning of multi-agent systems for which counters and recursivity were necessary. Although RPN strictly extend Petri nets and context-free grammars, most of the usual problems (reachability, termination, etc.) were shown to be decidable. For almost all other models extending Petri nets and context-free grammars, the complexity of coverability and termination are unknown or strictly larger than EXPSPACE. In contrast, we establish here that for RPN, the coverability, termination, boundedness and finiteness problems are EXPSPACE-complete as for Petri net. While having a great expressive power, RPN suffer several modeling limitations. We introduce Dynamic Recursive Petri nets (DRPN) which address these issues extending the expressiveness of RPN.This model generalizes almost all previous known models, which extend the Petri net and keep the coverability problem decidable. Thus we establish that the coverability problem is decidable for DRPN.For active learning and formal methods, our work focuses on Angluin's L* algorithm.Angluin's algorithm learns the minimal deterministic finite automaton (DFA) of a regular language using membership and equivalence queries. Its probabilistic approximately correct (PAC) version substitutes an equivalence query by a set of random membership queries. Thus, it can be applied to any kind of device and may be viewed as synthesizing an automaton from observations of the device. We are interested in how the PAC version behaves for devices which are obtained from a DFA by introducing some noise. More precisely, we study whether the algorithm reduces the noise, producing a DFA closer to the original one than the noisy device. We found that the reduction of the noise strongly depends on the type of noise and its amount.Moreover, we use this algorithm to develop a property-directed approach for verification of recurrent neural networks (RNNs). It learns a DFA as a surrogate model from a given RNN, which is then analyzed using model checking as a verification technique. We show that this not only allows us to discover small counterexamples fast, but also to generalize them by pumping towards faulty flows, hinting at the underlying error in the RNN.; Cette thèse contient trois parties. La première est consacrée à la vérification des réseaux de Petri, la seconde à la vérification des réseaux de Petri récursifs qui étendent les réseaux de Petri et la dernière combine l'apprentissage actif et la vérification.Un réseau de Petri peut être analysé en calculant et étudiant son Clover, la représentation canonique de la sur-approximation vers le bas de son ensemble d'accessibilité. A l'aide de l'algorithme de Karp-Miller on peut calculer le Clover, mais cet algorithme est très inefficace et sa preuve originelle de correction n'est pas satisfaisante.Il y a de nombreuses variantes de cet algorithme mais certaines sont incomplètes et d'autres requièrent une mémoire additionnelle de taille potentiellement ackermannienne. Enfin les preuves de correction sont souvent intriquées.Notre première contribution est la conception d'un algorithme complet incluant une borne théorique sur la taille de la mémoire additionelle.L'idée clef de cet algorithme est l'introduction d'un nouveau concept, appelé accélération.Plus précisément à l'aide des accélérations, nous avons pu:1. simplifier la preuve de correction de l'algorithme de Karp-Miller;2. présenter la première modification simple de l'algorithme incomplet de construction du ``Minimal Coverability Tree''. 3. prouver que la mémoire supplémentaire requise par notre algorithme est élémentaire (2-EXPSPACE);4. développer un prototype MinCov et de montrer expérimentalement qu'il est l'outil le plus efficace parmi ceux qui calculent le Clover.Au début des années 2000, les réseaux de Petri récursifs (RPN) ont été introduits en vue de la modélisation et de l'analyse de la planification distribuée de systèmes multi-agents pour lesquels la présence de compteurs et la recursivité sont nécessaires.Bien que les RPN étendent strictement les réseaux de Petri et les grammaires algébriques, la plupart des problèmes usuels(accessibilité, terminaison, etc.) restent décidables. Pour presque tous les modèles incluant les réseaux de Petri et les grammaires algébriques, la complexité des problèmes de la couverture et de la terminaison est inconnue ou strictement plus grande que EXPSPACE. Ici, nous montrons que les problèmes de couverture, terminaison, caractère borné et finitude des RPN sont EXPSPACE-complets comme ceux des réseaux de Petri. Bien qu'ayant un grand pouvoir d'expression, les RPN souffrent de plusieurs limitations en terme de modélisation.Aussi nous introduisons les réseaux de Petri récursifs dynamiques (DRPN) qui répondent à ces limitations et donc étendent le pouvoir d'expression des RPN.Les DRPN généralisent presque toutes les extensions de réseaux de Petri pour lesquelles le problème de couverture est décidable.Nous démontrons alors que le problème de couverture reste décidable pour les DRPN.Dans la troisième partie, notre travail se concentre sur l'algorithme L* d'AngluinL.Cet algorithme apprend l'automate fini déterministe (DFA) minimal d'un langage régulier à l'aide de questions d'appartenance et d'équivalence de langages. Sa version probabilistiquement approximativement correcte (PAC) remplace une question d'équivalence par un ensemble de questions aléatoires d'appartenance. Nous avons étudié comment la PAC version se comporte pour des machines qui sont obtenues en ``bruitant''un DFA et si l'algorithme réduit le bruit.Nous établissons que la réduction du bruit dépend fortement de la nature du bruit et de sa quantité.De plus, nous utilisons cet algorithme pour développer une approche de vérification des réseaux neuronaux récurrents (RNN).Un DFA est appris comme une abstraction d'un RNN puis analysé à l'aide de techniques de ``model checking''.Nous établissons deux avantages de cette approche : lorsque la propriété n'est pas vérifiée les contre-exemples exhibés sont de petite taille et susceptibles d'être généralisés en un patron d'erreur mettant en évidence la nature de la faute du RNN.

International audience; Par sa déclinaison omniprésente dans l’organisation économique et sociale, le concept de réseau apparaît comme un paradigme du monde contemporain. Les besoins en services divers (transports, énergie, consommation de biens manufacturiers, offre de soins, information et communication, etc.) engagent les usagers dans un entrelacement de réseaux qui sont autant de maillages de flux matériels et immatériels, au sein desquels l’utilisateur est consommateur de biens et de services issus des industries et des administrations, ou lui-même constituant de l’organisation (réseaux sociaux numériques).Cet ouvrage examine les invariants qui unifient les réseaux dans leur diversité, ainsi que les spécificités qui les différencient. Il offre une grille de lecture qui distingue un niveau générique où ces systèmes trouvent une interprétation commune, et un niveau spécifique où des méthodes d’analyse appropriées sont mobilisées.Trois études de cas, issues de domaines variés, illustrent de manière détaillée le propos de l’ouvrage.

Collisions and deadlocks are unwanted situations in many transport applications such as railway systems. Control synthesis methods can assure that a closed-loop system cannot lead to deadlock situations. Methods issued from the historical approach of Ramadge and Wonham allow dealing with this issue but encounter the problem of combinatorial explosion, that prevents its use on large systems. In the case of deadlock avoidance, the majority of approaches are based on the assumption of total controllability and observability. However, this assumption is not verified in all kinds of systems. This thesis proposes control synthesis methods that do not suffer from the combinatorial explosion. These methods are based on the formalism of Petri nets and uniquely concern classes of resource allocation systems. In a way to not resort to state exploration, these methods identify deadlock situations by resolving a mixed integer programming problem. These methods are then used for routing trains in a railway node. A systematic modeling approach of the trains' circulations in a railway node is developed. The model obtained is a Petri net for resources allocation system. To avoid collisions and deadlocks in the model, a control synthesis method, based on the theoretical background developed, is proposed; Les collisions et les blocages sont des situations que l'on souhaite éviter dans beaucoup d'application de transport. Les méthodes de synthèse de contrôleurs peuvent garantir qu'un système en boucle fermé ne puisse pas atteindre de telles situations. Les méthodes issues de l'approche historique de Ramadge et Wonham permettent de traiter cette problématique mais font face à l'explosion combinatoire, qui empêche leurs applications sur les systèmes de grandes tailles. Dans le cadre de l'évitement des blocages, la grande majorité des approches font l'hypothèse que le système est sous contrôlabilité et observabilité totales. Cependant, cette hypothèse n'est pas vérifiée pour tous les systèmes. Cette thèse propose des méthodes de synthèses de contrôleurs applicables sur des systèmes sous observabilité et contrôlabilité partielles sans souffrir de l'explosion combinatoire. Ces méthodes se basent sur le formalisme des Réseaux de Petri, et concernent uniquement des classes pour la modélisation de systèmes d'allocation de ressources. Pour ne pas avoir recours à l'exploration des états, ces méthodes identifient les situations de blocages grâce à la résolution d'un problème d'optimisation mixte en nombres entiers. Ces méthodes sont par la suite utilisées pour le routage des trains dans un nœud ferroviaire. Une méthode systématique de modélisation de la circulation des trains dans un nœud ferroviaire est proposée. Le modèle ainsi obtenu est un Réseau de Petri pour la modélisation des systèmes d'allocation de ressources. Pour éviter les collisions et les blocages au seins de ce modèle, une méthode de synthèse reposant sur les apports théoriques de cette thèse est appliquée

Collisions and deadlocks are unwanted situations in many transport applications such as railway systems. Control synthesis methods can assure that a closed-loop system cannot lead to deadlock situations. Methods issued from the historical approach of Ramadge and Wonham allow dealing with this issue but encounter the problem of combinatorial explosion, that prevents its use on large systems. In the case of deadlock avoidance, the majority of approaches are based on the assumption of total controllability and observability. However, this assumption is not verified in all kinds of systems. This thesis proposes control synthesis methods that do not suffer from the combinatorial explosion. These methods are based on the formalism of Petri nets and uniquely concern classes of resource allocation systems. In a way to not resort to state exploration, these methods identify deadlock situations by resolving a mixed integer programming problem. These methods are then used for routing trains in a railway node. A systematic modeling approach of the trains' circulations in a railway node is developed. The model obtained is a Petri net for resources allocation system. To avoid collisions and deadlocks in the model, a control synthesis method, based on the theoretical background developed, is proposed; Les collisions et les blocages sont des situations que l'on souhaite éviter dans beaucoup d'application de transport. Les méthodes de synthèse de contrôleurs peuvent garantir qu'un système en boucle fermé ne puisse pas atteindre de telles situations. Les méthodes issues de l'approche historique de Ramadge et Wonham permettent de traiter cette problématique mais font face à l'explosion combinatoire, qui empêche leurs applications sur les systèmes de grandes tailles. Dans le cadre de l'évitement des blocages, la grande majorité des approches font l'hypothèse que le système est sous contrôlabilité et observabilité totales. Cependant, cette hypothèse n'est pas vérifiée pour tous les systèmes. Cette thèse propose des méthodes de synthèses de contrôleurs applicables sur des systèmes sous observabilité et contrôlabilité partielles sans souffrir de l'explosion combinatoire. Ces méthodes se basent sur le formalisme des Réseaux de Petri, et concernent uniquement des classes pour la modélisation de systèmes d'allocation de ressources. Pour ne pas avoir recours à l'exploration des états, ces méthodes identifient les situations de blocages grâce à la résolution d'un problème d'optimisation mixte en nombres entiers. Ces méthodes sont par la suite utilisées pour le routage des trains dans un nœud ferroviaire. Une méthode systématique de modélisation de la circulation des trains dans un nœud ferroviaire est proposée. Le modèle ainsi obtenu est un Réseau de Petri pour la modélisation des systèmes d'allocation de ressources. Pour éviter les collisions et les blocages au seins de ce modèle, une méthode de synthèse reposant sur les apports théoriques de cette thèse est appliquée

We introduce the notion of level-regularity for Mazurkiewicz trace languages and we consider recognizable trace rewriting systems with level-regular contexts (RTLsystem). We prove that an automaton for which the underlying graph is the rewriting graph of a RTL system and for which the sets of initial vertices and final vertices are level-regular (RTL automaton), is word-automatic. In particular, the first-order theory of a RTL automaton is decidable. Then, we prove that, enriched with thereachability relation, an automaton for which the underlying graph is the concurrent unfolding of a finite concurrent graph, and for which the sets of initial vertices and final vertices are level-regular, is RTL. In particular, the first-order theory with the reachability predicate of such an automaton is decidable. Besides, it is known that this property also holds for ground term rewriting graphs (GTR graph). We highlight various concurrent unfoldings of finite concurrent graphs that are not GTRgraphs. The infinite quarter grid tree is such an unfolding. The class of concurrent unfoldings of finite concurrent graphs is therefore a class of word-automatic graphs for which the first-order theory with the reachability predicate is decidable and that contains some non GTR graphs. We define the operations of level-length synchronization and level-length superposition of trace automata (automata for which vertices are Mazurkiewicz traces) and we prove that if a family F of trace automata is closed under these operations, then for any deterministic trace automaton H 2 F, the languages accepted by the deterministic trace automata belonging to F and that are length-reducible to H, form a Boolean algebra; the length of a trace being the length of its Foata normal form, a trace automaton G is length-reducible to a trace automaton H if there exists a length-preserving morphism from G to H. Then, we show that the family of trace suffix automata with level regular contexts, the extension of word suffix automata to Mazurkiewicz traces, satisfies these closure properties. We define a generalized Petri net as a trace suffix automaton over a dependence alphabet for which the dependence is reduced to the equality and we show that the subfamily of generalized Petri nets also satisfies the closure properties above. In particular, this yields various Boolean algebras of word languages accepted by deterministic generalized Petri nets.; Nous introduisons la notion de régularité par niveaux pour des langages de traces de Mazurkiewicz et nous considérons des systèmes reconnaissables de réécriture de traces, à contextes réguliers par niveaux (RTL). Nous prouvons qu’un automate dont le graphe sous-jacent est le graphe de réécriture d’un système RTL et dont les ensembles de sommets initiaux et finaux sont réguliers par niveaux (automate RTL), est mot-automatique. En particulier, la théorie du premier ordre d’un automate RTL est décidable. Ensuite, nous prouvons que, enrichi de la relation d’accessibilité, un automate dont le graphe sous-jacent est déplié concurrent d’un graphe fini concurrent et dont les ensembles de sommets initiaux et finaux sont réguliers par niveaux, est RTL. En particulier, la théorie du premier ordre avec accessibilité d’un tel automate est décidable. Par ailleurs, il est bien connu que la théorie du premier ordre avec accessibilité du graphe de réécriture suffixe d’un système de réécriture de termes clos (graphe GTR) est décidable. Nous mettons en évidence divers dépliés concurrents de graphes finis concurrents qui ne sont pas des graphes GTR. L’arbre du quart de la grille infinie est un exemple de tel déplié. La classe des dépliés concurrents des graphes finis concurrents constitue ainsi une classe de DAG mot-automatiques, dont la théorie du premier ordre avec accessibilité est décidable et qui contient des graphes non GTR. Nous définissons pour les automates de traces (automates dont les sommets sont des traces de Mazurkiewicz) deux opérations que sont la synchronisation par niveaux et la superposition par niveaux et nous montrons que si une famille F d’automates de traces est fermée pour ces opérations, alors pour tout automate déterministe H 2 F, les langages acceptés par les automates déterministes de F qui sont longueur-réductibles en H forment une algèbre de Boole ; la longueur d’une trace étant donnée par la longueur de sa forme normale de Foata, un automate de traces G est longueur-réductible dans un automate de traces H, s’il existe un morphisme de G dans H préservant la longueur. Ensuite, nous montrons que la classe des automates suffixes de traces à contextes réguliers par niveaux, qui n’est que l’extension aux traces de Mazurkiewicz des automates suffixes de mots, satisfait ces propriétés de fermeture. Nous appelons réseau de Petri généralisé un automate suffixe de traces sur un alphabet de dépendance pour lequel la dépendance est réduite à l’égalité. Nous montrons alors que la sous-famille des réseaux de Petri généralisés satisfait également les propriétés de fermeture ci-dessus. Cela conduit notamment à 5 diverses algèbres de Boole de langages acceptés par des réseaux de Petri généralisés déterministes.

The security of communications depends on security algorithms which are often based on heavy calculations, in particular within an embedded system in view of its other tasks. In such a context, security algorithms consume significant time and energy resources. Security then becomes a slider, a slider that one can move by choosing the right algorithms and parameters for the needs of the embedded system. Finding the right compromise between security, availability and autonomy of a wireless sensor network is difficult for an embedded systems designer. The objective of this thesis is to define the parameters on which it is possible to act to find an acceptable solution. A model in the form of Petri nets is offered to make these parameters interact and highlight their mutual influences.; La sécurité d'un moyen de communication dépend d’algorithmes de sécurité qui reposent sur des calculs souvent lourds, en particulier au sein d'un système embarqué par rapport à ses autres tâches. Dans un tel contexte, les algorithmes de sécurité consomment d'importantes ressources temporelles et énergétiques. La sécurité devient alors un curseur à faire varier grâce à des choix d'algorithmes et de paramètres adaptés aux besoins du système embarqué communicant. Trouver le bon compromis entre sécurité, disponibilité et autonomie d'un réseau de capteurs sans fil est délicat pour un concepteur d'objets connectés. L'objectif de cette thèse est de définir les paramètres sur lesquels il est possible de jouer pour trouver une solution acceptable. Un modèle sous forme de réseaux de Petri est proposé pour faire interagir ces paramètres et mettre en évidence leurs influences sur un réseau de capteur sans fil.

International audience; Ce papier présente une étude relative au développement de systèmes de production intelligents dans le contexte de l'industrie manufacturière. Nous montrons que de tels systèmes doivent être agile, c'est-à-dire capable de s'adapter rapidement à des contextes changeant comme une production particulière ou une panne. Dans cette étude nous modélisons le système de commande de ces systèmes par une approche en couches et générique. Nous distinguons plusieurs classes de modèles permettant de gérer chacun différentes catégories de flexibilité. L'objectif essentiel de l'étude est de fournir une méthode rigoureuse et systématique permettant de modéliser et de vérifier de manière efficace ce type de système.

International audience; Dans cet article, nous décrivons un travail préliminaire mené en 2019 et 2020, pour avancer dans la transcription automatique d’un diagramme unifilaire électrique en réseaux de Petri. Le but consiste à pouvoir simuler les modèles obtenus, afin d’estimer quantitativement les critères de sûreté de fonctionnement intéressant les clients industriels de ces réseaux électriques, comme par exemple le nombre de coupures d’énergie électrique dans une période donnée, ou encore la durée moyenne d’une séquence temporelle particulière (basculement de source). Une fois cette étape validée, il conviendra de développer une version industrielle de ces travaux, afin d’aider concrètement les exploitants de réseaux électriques à anticiper leurs besoins.

International audience; Des modèles de réseaux de Petri stochastiques à prédicats ont été développés puis intégrés dans un logiciel pour représenter des maintenances correctives et/ou préventives imparfaites selon les modèles de Brown Proschan et d'Arithmetic Reduction of Age model with infinite memory.

We introduce the notion of level-regularity for Mazurkiewicz trace languages and we consider recognizable trace rewriting systems with level-regular contexts (RTLsystem). We prove that an automaton for which the underlying graph is the rewriting graph of a RTL system and for which the sets of initial vertices and final vertices are level-regular (RTL automaton), is word-automatic. In particular, the first-order theory of a RTL automaton is decidable. Then, we prove that, enriched with thereachability relation, an automaton for which the underlying graph is the concurrent unfolding of a finite concurrent graph, and for which the sets of initial vertices and final vertices are level-regular, is RTL. In particular, the first-order theory with the reachability predicate of such an automaton is decidable. Besides, it is known that this property also holds for ground term rewriting graphs (GTR graph). We highlight various concurrent unfoldings of finite concurrent graphs that are not GTRgraphs. The infinite quarter grid tree is such an unfolding. The class of concurrent unfoldings of finite concurrent graphs is therefore a class of word-automatic graphs for which the first-order theory with the reachability predicate is decidable and that contains some non GTR graphs. We define the operations of level-length synchronization and level-length superposition of trace automata (automata for which vertices are Mazurkiewicz traces) and we prove that if a family F of trace automata is closed under these operations, then for any deterministic trace automaton H 2 F, the languages accepted by the deterministic trace automata belonging to F and that are length-reducible to H, form a Boolean algebra; the length of a trace being the length of its Foata normal form, a trace automaton G is length-reducible to a trace automaton H if there exists a length-preserving morphism from G to H. Then, we show that the family of trace suffix automata with level regular contexts, the extension of word suffix automata to Mazurkiewicz traces, satisfies these closure properties. We define a generalized Petri net as a trace suffix automaton over a dependence alphabet for which the dependence is reduced to the equality and we show that the subfamily of generalized Petri nets also satisfies the closure properties above. In particular, this yields various Boolean algebras of word languages accepted by deterministic generalized Petri nets., Nous introduisons la notion de régularité par niveaux pour des langages de traces de Mazurkiewicz et nous considérons des systèmes reconnaissables de réécriture de traces, à contextes réguliers par niveaux (RTL). Nous prouvons qu’un automate dont le graphe sous-jacent est le graphe de réécriture d’un système RTL et dont les ensembles de sommets initiaux et finaux sont réguliers par niveaux (automate RTL), est mot-automatique. En particulier, la théorie du premier ordre d’un automate RTL est décidable. Ensuite, nous prouvons que, enrichi de la relation d’accessibilité, un automate dont le graphe sous-jacent est déplié concurrent d’un graphe fini concurrent et dont les ensembles de sommets initiaux et finaux sont réguliers par niveaux, est RTL. En particulier, la théorie du premier ordre avec accessibilité d’un tel automate est décidable. Par ailleurs, il est bien connu que la théorie du premier ordre avec accessibilité du graphe de réécriture suffixe d’un système de réécriture de termes clos (graphe GTR) est décidable. Nous mettons en évidence divers dépliés concurrents de graphes finis concurrents qui ne sont pas des graphes GTR. L’arbre du quart de la grille infinie est un exemple de tel déplié. La classe des dépliés concurrents des graphes finis concurrents constitue ainsi une classe de DAG mot-automatiques, dont la théorie du premier ordre avec accessibilité est décidable et qui contient des graphes non GTR. Nous définissons pour les automates de traces (automates dont les sommets sont des traces de Mazurkiewicz) deux opérations que sont la synchronisation par niveaux et la superposition par niveaux et nous montrons que si une famille F d’automates de traces est fermée pour ces opérations, alors pour tout automate déterministe H 2 F, les langages acceptés par les automates déterministes de F qui sont longueur-réductibles en H forment une algèbre de Boole ; la longueur d’une trace étant donnée par la longueur de sa forme normale de Foata, un automate de traces G est longueur-réductible dans un automate de traces H, s’il existe un morphisme de G dans H préservant la longueur. Ensuite, nous montrons que la classe des automates suffixes de traces à contextes réguliers par niveaux, qui n’est que l’extension aux traces de Mazurkiewicz des automates suffixes de mots, satisfait ces propriétés de fermeture. Nous appelons réseau de Petri généralisé un automate suffixe de traces sur un alphabet de dépendance pour lequel la dépendance est réduite à l’égalité. Nous montrons alors que la sous-famille des réseaux de Petri généralisés satisfait également les propriétés de fermeture ci-dessus. Cela conduit notamment à 5 diverses algèbres de Boole de langages acceptés par des réseaux de Petri généralisés déterministes.

Alarm systems play an important role for the safe and efficient operation of modern industrial plants. However, in most of industrial alarm systems, alarm flows cannot always be correctly managed by the operators as they often turn into alarm floods, sequences of numerous alarms occurring in a short period of time. To reduce the alarm flows, this report focuses on detection of redundant alarms that could be removed. This objective is met by, first, looking for frequent adjacency in the alarm log. To identify them, the frequent pattern mining algorithm AprioriAll is adapted. Another way to find potentially redundant alarms is to look for systematic predecessors. To discover them, dominations and mutual dependencies contained in the alarm log are identified. To ease this analysis, the discovered relations are depicted in the form of Petri nets.Both those methods are then tested against an industrial alarm log made available by General Electric. The results show that both methods allow a reduction of the alarm flow, with the biggest reduction being during alarm floods.; Les systèmes d'alarmes jouent un rôle critique dans la bonne exploitation des installations industrielles modernes. Cependant, dans la plupart de ces systèmes, les alarmes ne sont pas toujours traitées correctement par les opérateurs car il y a régulièrement beaucoup trop d’alarmes à gérer, notamment lors des avalanches d’alarmes. Pour réduire le flux d'alarmes, notre approche consiste à détecter des redondances entre alarmes qui pourraient être supprimées. Pour atteindre cet objectif, nous recherchons dans un premier temps les adjacences fréquentes entre les alarmes contenues dans un historique. Ceci est réalisé en adaptant l’algorithme de recherche de motifs fréquents AprioriAll. Nous explorons également une seconde méthode consistant à trouver des précédences systématiques. Pour les découvrir, nous identifions les relations de domination et de mutuelle dépendance contenues dans l’historique des alarmes. Pour faciliter l’analyse experte, les relations découvertes sont traduites sous la forme d’un réseau de Pétri.Ces deux méthodes sont ensuite confrontées à un historique d’alarmes industriel fourni par General Electric. Les résultats obtenus montrent que nos deux méthodes permettent une réduction globale du flux d'alarmes qui est plus importante durant les avalanches.

Alarm systems play an important role for the safe and efficient operation of modern industrial plants. However, in most of industrial alarm systems, alarm flows cannot always be correctly managed by the operators as they often turn into alarm floods, sequences of numerous alarms occurring in a short period of time. To reduce the alarm flows, this report focuses on detection of redundant alarms that could be removed. This objective is met by, first, looking for frequent adjacency in the alarm log. To identify them, the frequent pattern mining algorithm AprioriAll is adapted. Another way to find potentially redundant alarms is to look for systematic predecessors. To discover them, dominations and mutual dependencies contained in the alarm log are identified. To ease this analysis, the discovered relations are depicted in the form of Petri nets.Both those methods are then tested against an industrial alarm log made available by General Electric. The results show that both methods allow a reduction of the alarm flow, with the biggest reduction being during alarm floods.; Les systèmes d'alarmes jouent un rôle critique dans la bonne exploitation des installations industrielles modernes. Cependant, dans la plupart de ces systèmes, les alarmes ne sont pas toujours traitées correctement par les opérateurs car il y a régulièrement beaucoup trop d’alarmes à gérer, notamment lors des avalanches d’alarmes. Pour réduire le flux d'alarmes, notre approche consiste à détecter des redondances entre alarmes qui pourraient être supprimées. Pour atteindre cet objectif, nous recherchons dans un premier temps les adjacences fréquentes entre les alarmes contenues dans un historique. Ceci est réalisé en adaptant l’algorithme de recherche de motifs fréquents AprioriAll. Nous explorons également une seconde méthode consistant à trouver des précédences systématiques. Pour les découvrir, nous identifions les relations de domination et de mutuelle dépendance contenues dans l’historique des alarmes. Pour faciliter l’analyse experte, les relations découvertes sont traduites sous la forme d’un réseau de Pétri.Ces deux méthodes sont ensuite confrontées à un historique d’alarmes industriel fourni par General Electric. Les résultats obtenus montrent que nos deux méthodes permettent une réduction globale du flux d'alarmes qui est plus importante durant les avalanches.

Urban rail traffic is subject to numerous disrupting events that drift it from its nominal behavior. In order to minimize the impact of these disturbances, rail operators rely on a set of techniques. Despite their efficiency, performances of theses techniques are rarely well studied, nor are they of proven optimality; a direct consequence of them being empirically built. It is in this particular context that comes our work to provide solutions that allow for the evaluation of such techniques and for the comparison of their relative performances in various scenarios. The proposed approach is based on variants of Petri nets as models, and on the Monte-Carlo method for the simulation of their execution. This combination has led to the development of SIMSTORS, a tool for the simulation of urban rail systems, and more generally, stochastic systems under dynamic rescheduling. Additionally, this thesis addresses the question of timetable realizability; that is whether or not a given timetable is indeed realizable by a system for which it was built. Indeed, a timetable is meant to drive the behavior of a system but there is no guarantee as to its realizability. We therefore propose a method for the verification of the realizability of timetables with a strictly positive probability.; Le trafic ferroviaire urbain est quotidiennement sujet à des perturbations qui le dévient de son comportement nominal. Afin de minimiser l'impact de ces perturbations, les opérateurs ferroviaires usent de diverses techniques. Nonobstant leur efficacité, les performances de ces techniques ne sont généralement pas bien étudiées ni sont-elles optimales, car élaborées empiriquement. C'est dans ce cadre-ci que vient cet ouvrage fournir des solutions qui permettent d'évaluer ces techniques de régulation et d'en comparer les performances dans des contextes variés. L’approche proposée se base sur des variantes de réseaux de Petri comme modèles et sur la méthode de Monte-Carlo pour en simuler l’exécution. Cette combinaison a donné naissance à SIMSTORS, un outil de simulation pour les systèmes ferroviaires urbains, et plus généralement, pour les systèmes stochastiques régulés. Additionnellement, nous nous intéressons dans cette thèse à la problématique de la réalisabilité des tables horaires qui pilotent le trafic ferroviaire. Ces tables décrivent le comportement temporel désiré des systèmes pour lesquels elles sont conçues. Or, la construction de ces tables ne garantit pas toujours sa réalisabilité, notamment dans un contexte stochastique. Ainsi, nous proposons ici une méthode permettant de vérifier si une table horaire est bien réalisable avec une probabilité strictement positive.

Several formal methods of supervisory control of discrete events systems (DES), based on Petri nets (PN) have been developed. However, they are partially structural because of the need to construct the marking graph, which is an automaton, to determine the states forbidden by the specification. Some of those methods are limited to a particular class of Petri nets. Our work focused on the labeled Petri nets (LPN), which offers a better structure for defining the languages and automata. Among the based methods based on Petri nets, the invariant place method (simple and efficient) is the most used, although it does not guarantee in the general an optimal solution. In order to overcome this problem, we have developed a completely structural method, without construction of the marking graph for ordinary labeled Petri nets. It consists in determining in a way structural, admissible constraints for the invariant method place. It is based on the structural condition of controllability of closed loop SED LPN states, got by synchronous product of the process and specification LPN. In addition, we have proved that the structural condition of controllability, defined by the marking condition of entrance places of an uncontrollable synchronous transition, is equivalent to the condition of controllability defined by the languages of the LPN. This condition defines the equation of a separator hyperplan which ensures separation of the admissible states from the forbidden states in the SED. Constraints derived from hyperplane separator are admissible and can be simplified systematically. They provide a one-to-one link between the theory of supervisory control of Ramadge and Wonham and the calculation of maximum permissive controller by the invariant place method. Although for some complex structures (great scale), the maximum permissive solution cannot be guarantee directly; our approach gave the optimal controller in the real case studies considered., Plusieurs méthodes formelles de commande par supervision des systèmes à événements discrets (SED) basées sur les réseaux de Petri (RdP) ont été développées. Cependant, elles sont partiellement structurelles à cause de la nécessité de construire le graphe de marquage, qui est un automate, pour déterminer les états interdits par la spécification. Certaines de ces méthodes sont limitées à une classe particulière de RdP. Notre travail s'est focalisé en particulier sur le RdP synchronisé (RdPS), qui offre une meilleure structure pour définir les langages et les automates. Parmi les méthodes basées sur les RdP, la méthode des invariants (simple et efficace) est la plus utilisée bien qu’elle ne garantisse pas en général une solution de contrôle optimale. Pour pallier ce problème, nous avons développé une méthode complètement structurelle, sans construction du graphe de marquage, pour les RdPS ordinaires ou généralisés. Elle consiste à déterminer de manière structurelle les contraintes admissibles pour la méthode des invariants. Elle est basée sur la condition de contrôlabilité structurelle des états du RdPS du SED en boucle fermée, obtenu par produit synchrone des RdPS du procédé et de la spécification. En outre, nous avons prouvé que la condition de contrôlabilité structurelle, définie par la condition de marquage des places d’entrée d’une transition synchrone incontrôlable, est équivalente à la condition de contrôlabilité définie par les langages du RdPS. Cette condition définit l’équation d’un hyperplan séparateur qui assure la séparation des états admissibles des états interdits dans le SED. Les contraintes dérivées de d’hyperplan séparateur sont admissibles et peuvent être simplifiées systématiquement. Elles permettent de faire un lien biunivoque entre la théorie de commande par supervision de Ramadge et Wonham et la méthode des invariants pour le calcul d’un contrôleur optimal au sent maximal permissif. Même si pour certaines structures très complexes (à grande échelle), la solution maximale permissive ne peut être garantie directement, notre approche a donné le contrôleur optimal dans les études de cas réels considérés.

International audience; Une étape du Rapid Control Prototyping peut consister à exécuter une version simulée d'un système de commande en lien avec un environnement réel. Dans ce cadre, le simulateur doit assurer une exécution en temps réel de la simulation de la commande afin de permettre un fonctionnement opérationnel. Cet article propose une mise en œuvre matérielle d'un simulateur à événements discrets qui, si elle ne garantit pas encore le temps réel, permet d'accélérer fortement la simulation pour tendre vers cet objectif. Il s'agit d'un travail en cours s'inscrivant dans notre volonté d'assurer un flot complet de génération d'un système depuis des modèles dans une approche d'ingénierie dirigée par les modèles.

National audience; Nous présentons dans cet article la conception d'une plateforme de simulation distribuée de modèles DEVS (Discrete Event System Specification) basée sur l'exécu-tion de réseaux de Petri temporisés qui communiquent au travers d'une connexion réseau. Dans notre proposition , l'exécution des réseaux de Petri est déployée sur une architecture distribuée composée de noeuds logiciels PC et/ou matériels FPGA (Field-Programmable Gate Array) par une mise en oeuvre des réseaux de Petri en C et en VHDL. En outre, ce travail s'inscrit dans la perspective future de pouvoir connecter les modèles avec des équipe-ments réels. Mots-clés : Simulation distribuée, Cosimulation logi-cielle/matérielle, Réseaux de Petri. Abstract: In this article, we present the design of a distributed DEVS (Discrete Event System Specification) model simulation platform based on the execution of timed Petri nets that communicate through a network connection. In our proposal, the execution of the Petri nets is deployed on a distributed architecture made of software PC and/or hardware FPGA (Field-Programmable Gate Array) nodes using a C and a VHDL implementation of Petri nets. In addition, this work is part of the future perspective of being able to connect models with real equipments.

The HILECOP methodology has been developed for the formal design of critical complex digital systems; it therefore covers the entire design process, ranging from modeling to code generation for implementation on the hardware target (FPGA type electronic component), via formal validation. However, if the formal model, the Petri nets in this case, is inherently asynchronous, it is nevertheless executed synchronously on the target. In fact, the usual analysis approaches are not adapted in the sense that they construct state graphs that do not conform to the real state evolution within the target. In order to gain confidence in the validity of the results of the formal analysis, this work aims to capture the so-called non-functional characteristics, to reify them on the model and finally to consider their impact through the analysis.In other words, the aim is to improve the expressiveness of the model and the relevance of the analysis, considering aspects such as clock synchronization, effective parallelism, the risk of blocking induced by the expression of an event (condition) and a time window of occurrence, without omitting the management of exceptions.To deal with all these aspects, we have proposed a new method of analysis for extended generalized synchronous executed time Petri nets, transforming them into an analysable equivalent formalism. This formalism is associated with a formal semantics integrating all the particular aspects of the execution and dédicated state space construction algorithm: the Synchronous Behavior Graph.Our work has been applied to an industrial case, more precisely to the validation of the behavior of the digital part of a neuro-stimulator.; La méthodologie HILECOP a été élaborée pour la conception formelle de systèmes numériques complexes critiques ; elle couvre donc l'intégralité du processus, allant de la modélisation à la génération de code pour l’implantation sur la cible matérielle (composant électronique de type FPGA), en passant par la validation formelle. Or, si le modèle formel, les réseaux de Petri en l'occurrence, est par essence asynchrone, il est néanmoins exécuté de manière synchrone sur la cible. De fait, les approches d'analyse usuelles ne sont pas adaptées au sens où elles construisent des graphes d'états non conformes à l'évolution d'états réelle au sein de la cible. Dans l'objectif de gagner en confiance quant à la validité des résultats de l’analyse formelle, ces travaux visent à capturer les caractéristiques dites non-fonctionnelles, à les réifier sur le modèle et enfin à considérer leur impact à travers l’analyse. En d’autres termes, l’objectif est d’améliorer l’expressivité du modèle et la pertinence de l'analyse, en considérant des aspects comme la synchronisation d'horloge, le parallélisme effectif, le risque de blocage induit par l'expression conjointe d'un événement (condition) et d'une fenêtre temporelle d'occurrence, sans omettre la gestion des exceptions. Pour traiter tous ces aspects, nous avons proposé une nouvelle méthode d'analyse pour les réseaux de Petri temporels généralisés étendus interprétés exécutés en synchrone, en les transformant vers un formalisme équivalent analysable. Ce formalisme est associé avec une sémantique formelle intégrant toutes les aspects particuliers de l'exécution et un algorithme de construction d'un graphe d'états spécifique : le Graphe de Comportement Synchrone. Nos travaux ont été appliqués à un cas industriel, plus précisément à la validation du comportement de la partie numérique d'un neuro-stimulateur.

With works such as Kinoautomat by Radúz Činčera, SAM - Sound Activated Mobile by Edward Ihnatowicz, and Glowflow by Myron Krueger, artists have deployed, as early as the 1960s, art installations engaging novel situations of collective co-located interaction, i.e involving multiple or even many spectators interacting in the same place via and with a digital apparatus. The number of those works has continued to increase since the beginning of the 21st century, taking advantage of the new opportunities offered by advances in real-time computer vision technologies and the advent of ubiquitous computing marked by the multiplication and interoperability of mobile computing devices. While experiences in this area are more and more frequent, they have not yet been the subject of structured analysis and, even less, of proposals for dedicated tools and design methods. How can we, nowadays, conceive such interactive art installations whose intrinsic complexity involves questions of the technical, social, cognitive and aesthetic order? This dissertation draws on previous work in the fields of human-computer interaction (HCI), computer-supported cooperative work (CSCW), and interactive arts research with the aim of increasing our knowledge of the challenges faced both by art practitioners and participants in such collective interactive installations, and, beyond, the designers of apparatus in a promising future. A set of tools and guidelines are proposed when designing collective co-located interactions for digital art installations. First a classification system is developed centered on the most decisive aspects that allow the emergence of a collective experience. Two distinct approaches are then explored to find the bases of a graphical modeling language for the design and analysis of such apparatus. Build on top of Petri nets, the second approach supports modeling the spatial and material resources of an installation, as well as the human-machine, human-human and human-machine-human interactions. The investigations conducted for this research have required laying particular emphasis on the conditions - whether spatial, material, or human - which affect the ability for participants to co-construct a common aesthetic experience in the absence of orchestration or a preannounced goal to be achieved. While this singular approach primarily concerns interactive arts, it may be relevant to a wide range of research communities, including, and foremost, that of HCI, as well as CSCW, New Interfaces for Musical Expression (NIME), interaction design, and even culture, museography in particular., À l'instar d'œuvres telles que Kinoautomat de Radúz Činčera, SAM - Sound Activated Mobile d'Edward Ihnatowicz et Glowflow de Myron Krueger, des artistes ont développé, dès les années 1960, des installations artistiques engageant des situations d'interaction collective co-localisée inédites, c'est-à-dire impliquant plusieurs voire de nombreux spectateurs interagissant dans le même lieu via et avec un dispositif informatique. Le nombre de ces travaux ne cesse d'augmenter depuis le début du 21ème siècle, profitant des nouvelles opportunités offertes par les avancées dans les technologies de vision par ordinateur en temps réel et par l'avènement de l'informatique ubiquitaire marquée par la multiplication et l'interopérabilité des appareils informatiques mobiles. Si les expériences en la matière sont de plus en plus fréquentes, elles n'ont jusqu'à ce jour fait l'objet d'aucune analyse structurée et, encore moins, de propositions d'outils et de méthodes de conception dédiés. Comment, aujourd'hui, concevoir de tels dispositifs artistiques interactifs dont la complexité intrinsèque implique des questions aussi bien de l'ordre technique, social, cognitif qu'esthétique ? Cette thèse met à contribution des travaux antérieurs dans les domaines de l'interaction homme-machine (IHM), du travail coopératif assisté par ordinateur (TCAO) et des arts interactifs dans le but d'accroître notre connaissance quant aux défis auxquels sont confrontés à la fois les artistes et les participants de telles installations et, au-delà, les concepteurs de ces dispositifs en devenir. Un ensemble d'outils et de lignes directrices sont proposés pour la conception de systèmes d'interaction collective co-localisée pour les installations d'art numérique. Est d'abord développé un système de classification centré sur les aspects les plus décisifs permettant l'émergence d'une expérience collective. Deux approches différentes sont ensuite explorées pour trouver les bases d'un langage de modélisation graphique pour l'analyse et la conception de tels dispositifs. S'appuyant sur les réseaux de Petri, la deuxième approche permet de modéliser aussi bien les ressources spatiales et matérielles d'une installation, que les interactions homme-machine, humain(s)-humain(s) et humain(s)-machine(s)-humain(s). Les investigations menées pour cette recherche ont nécessité de mettre un accent particulier sur les conditions - qu'elles soient spatiales, matérielles ou humaines - qui affectent la capacité pour les participants de telles installations de co-construire une expérience esthétique commune en l'absence d'orchestration ou d'un objectif pré-annoncé à atteindre. Si cette approche singulière concerne en premier lieu les arts interactifs, elle peut revêtir également un caractère pertinent pour d'autres communautés de recherche, y compris et en premier lieu, celle de l'IHM, ainsi que celles du TCAO, des Nouvelles interfaces pour l'expression musicale (NIME), du design d'interaction ou encore de la culture, en particulier de la muséographie.

With the aim of increasing the modelling capability of Petri nets, wesuggest that models involve parameters to represent the weights of arcs, or the number of tokensin places. We consider the property of coverability of markings. Two general questions arise,the universal and the existential one: “Is there a parameter value for which the property issatisfied?” and “Does the property hold for all possible values of the parameters”. We showthat these issues are undecidable in the general case. Therefore, we also define subclasses ofparameterised nets, depending on whether the parameters are used on places, input or outputarcs of transitions. For some classes, we prove that universal and existential coverability becomedecidable, making these classes more usable in practice. To complete this study, we prove thatthose problems are ExpSpace-complete. We also address a problem of parameter synthesis,that is computing the set of values for the parameters such that a given marking is coverablein the instantiated net. Restricting parameters to only input weights (preT-PPNs) provides adownward-closed structure to the solution set. We therefore invoke a result for the representationof upward closed set from Valk and Jantzen. The condition to use this procedure is equivalentto decide the universal coverability. We also propose an adaptation of this reasoning to thecase of parameters used only as output weights (postT-PPNs). In this case, the condition touse this procedure can be reduced to the decidability of the existential coverability. Finally,we broaden this study by establishing decision frontiers through the study of existential anduniversal reachability.; Afin de permettre une modélisation plus souple des systèmes, nous proposons d’étendre les réseaux de Petri par des paramètres discrets représentant le poids des arcsou le nombre de jetons présents dans les places. Dans ce modèle, tout problème de décision peutêtre décliné sous deux versions, une universelle, demandant si la propriété considérée est vraiequelles que soient les valeurs que prennent les paramètres et une existentielle, qui s’interroge surl’existence d’une valeur pour les paramètres telle que la propriété soit satisfaite. Concernantla couverture, nous montrons que ces deux problèmes sont indécidables dans le cas général.Nous introduisons donc des sous classes syntaxiques basées sur la restriction des paramètres auxplaces, aux arcs en sortie ou aux arcs en entrée des transitions. Dans ces différents cas, nousmontrons que la couverture existentielle et universelle sont décidables et EXPSPACE-complètes.Nous étudions alors le problème de la synthèse de paramètres qui s’intéresse à calculer l’ensembledes valeurs de paramètres telles que la propriété considérée soit vraie. Sur les sous classes introduites, concernant la couverture, nous montrons que les ensembles solutions à la synthèseont des structures fermée supérieurement (cas des arcs de sortie) et fermée inférieurement (casdes arcs d’entrée). Nous prouvons alors que ces ensembles se calculent par un algorithme dela littérature, proposé par Valk et Jantzen, dont les conditions d’application se réduisent auxproblèmes de décision étudiés précédemment. Enfin nous étudions les frontières de décision ennous intéressant aux versions paramétrées de l’accessibilité pour ces sous classes.

With the aim of increasing the modelling capability of Petri nets, wesuggest that models involve parameters to represent the weights of arcs, or the number of tokensin places. We consider the property of coverability of markings. Two general questions arise,the universal and the existential one: “Is there a parameter value for which the property issatisfied?” and “Does the property hold for all possible values of the parameters”. We showthat these issues are undecidable in the general case. Therefore, we also define subclasses ofparameterised nets, depending on whether the parameters are used on places, input or outputarcs of transitions. For some classes, we prove that universal and existential coverability becomedecidable, making these classes more usable in practice. To complete this study, we prove thatthose problems are ExpSpace-complete. We also address a problem of parameter synthesis,that is computing the set of values for the parameters such that a given marking is coverablein the instantiated net. Restricting parameters to only input weights (preT-PPNs) provides adownward-closed structure to the solution set. We therefore invoke a result for the representationof upward closed set from Valk and Jantzen. The condition to use this procedure is equivalentto decide the universal coverability. We also propose an adaptation of this reasoning to thecase of parameters used only as output weights (postT-PPNs). In this case, the condition touse this procedure can be reduced to the decidability of the existential coverability. Finally,we broaden this study by establishing decision frontiers through the study of existential anduniversal reachability.; Afin de permettre une modélisation plus souple des systèmes, nous proposons d’étendre les réseaux de Petri par des paramètres discrets représentant le poids des arcsou le nombre de jetons présents dans les places. Dans ce modèle, tout problème de décision peutêtre décliné sous deux versions, une universelle, demandant si la propriété considérée est vraiequelles que soient les valeurs que prennent les paramètres et une existentielle, qui s’interroge surl’existence d’une valeur pour les paramètres telle que la propriété soit satisfaite. Concernantla couverture, nous montrons que ces deux problèmes sont indécidables dans le cas général.Nous introduisons donc des sous classes syntaxiques basées sur la restriction des paramètres auxplaces, aux arcs en sortie ou aux arcs en entrée des transitions. Dans ces différents cas, nousmontrons que la couverture existentielle et universelle sont décidables et EXPSPACE-complètes.Nous étudions alors le problème de la synthèse de paramètres qui s’intéresse à calculer l’ensembledes valeurs de paramètres telles que la propriété considérée soit vraie. Sur les sous classes introduites, concernant la couverture, nous montrons que les ensembles solutions à la synthèseont des structures fermée supérieurement (cas des arcs de sortie) et fermée inférieurement (casdes arcs d’entrée). Nous prouvons alors que ces ensembles se calculent par un algorithme dela littérature, proposé par Valk et Jantzen, dont les conditions d’application se réduisent auxproblèmes de décision étudiés précédemment. Enfin nous étudions les frontières de décision ennous intéressant aux versions paramétrées de l’accessibilité pour ces sous classes.

Bacteria have evolved many types of genetically induced mechanisms to face different types of stresses and to adapt to new environments. Competence for natural transformation is one such process that promotes horizontal gene transfer. If phylogenetically distant species share conserved uptake and processing apparatus, competence regulatory circuits are not universal but adapted to every species' lifestyle. In Gram-positive bacteria, Streptococcus pneumoniae and Bacillus subtilis regulatory cascades are the best documented. If many mathematical models have been established to study different aspects of competence regulation in B. subtilis, only one population-scaled model has been developed for S. pneumoniae, a decade ago, based on hypotheses that are challenged by new experimental data. We develop, in S. pneumoniae, a knowledge-based model of the competence regulation at cell level that integrates the enriched biological knowledge acquired to date. The structural consistency of the network topology is confirmed using Petri net formalism. The network is further turned into a set of ordinary differential equations to study its dynamics behavior. Protein kinetics are estimated using time-series luminescence data and other parameter estimations are constrained according to available knowledge. We point out some gap in competence shut-off knowledge, and, after testing alternative models, we predict the requirement of a yet unknown late com gene product inhibiting the action of ComW, the ?x factor activator. We also bring new insights into this regulatory cascade by predicting the system components that might be involved in specific experimental behavior. Our model consolidates the experimental knowledge acquired on competence regulation in S. pneumoniae. Moreover, it can be applied to the other streptococci species belonging to the mitis and anginosus groups since they shared the same regulatory circuit. In the population, the competence shift happens first in a subpopulation of cells and spreads into the whole population through cell to cell contact. Allowing simulation of individual cell behavior, our model will provide a brick for the design of a population-scale model composed of heterogeneous cells.; Afin de faire face à différents types de stress et s'adapter à de nouveaux environnements, les bactéries ont développé de nombreux mécanismes génétiquement régulés. La compétence pour la transformation naturelle est un processus qui favorise le transfert horizontal de gènes. Si les espèces phylogénétiquement éloignées partagent des mécanismes conservés d'intégration et de remaniement de l'ADN, les circuits de régulation de la compétence ne sont toutefois pas universels mais adaptés au mode de vie de chaque espèce. Chez les bactéries Gram-positives, les cascades de régulation de Streptococcus pneumoniae et Bacillus subtilis sont les mieux documentées. Si de nombreux modèles mathématiques ont été établis pour étudier différents aspects de la régulation des compétences chez B. subtilis, un seul modèle à échelle de population a été développé pour S. pneumoniae, il y a plus de dix ans, sur la base d'hypothèses contestées par de nouvelles données expérimentales. Nous avons développé, chez S. pneumoniae, un modèle fondé sur la connaissance de la régulation de la compétence qui intègre les éléments biologiques essentiels connus à ce jour. La cohérence structurelle de la topologie du réseau est confirmée par le formalisme des réseaux de Petri. Le réseau est ensuite transformé en un ensemble d'équations différentielles ordinaires pour étudier son comportement dynamique. La cinétique des protéines a été estimée en utilisant des données de luminescence et l'estimation des paramètres a été contrainte à partir des connaissances disponibles. Après avoir testé des modèles alternatifs, nous avons proposé l'existence d'un produit de gène tardif supplémentaire pouvant inhiber l'action de ComW, l'activateur du facteur sx. Nous apportons également un nouvel éclairage sur cette cascade de régulation en prédisant la cinétique de composantes du système qui pourraient être impliquées dans des comportements spécifiques. Ce modèle consolide les connaissances expérimentales acquises sur la régulation de la compétence chez S. pneumoniae. De plus, il peut être appliqué aux autres espèces de streptocoques appartenant aux groupes mitis et anginosus puisqu'ils partagent le même circuit régulateur. À l'échelle populationnelle, la transition vers l'état de compétence se produit d'abord dans une sous-population de cellules et se propage ensuite dans toute la population par contact physique cellule à cellule. En permettant la simulation du comportement d'une cellule individuelle, le modèle pourra servir de module dans la conception d'un modèle d'une population bactérienne composée de cellules hétérogènes.

System biology aims at understanding and analyzing biological systems usingmathematical and computational models. The explosion of the number of experimentaldata leads to larger and larger models. In order to be able to easily analyzethem and quickly simulate them, it is necessary to be able to simplify them.In this thesis, we propose simplification methods for biochemical reaction networks.These methods are sufficiently rich to be able to simplify an importantnumber of networks from biological applications. They are contextual, allowingto consider a network as a sub-module of a larger model, and to simplify it withoutmodifying the behavior of the global model. Finally, our simplifications aresound, meaning that they preserve the semantics of the networks. Firstly, we areinterested in a non deterministic semantics, based on the capability to convergeto some attractors of the network. Then we study some simplifications for thedeterministic semantics, allowing for instance to remove intermediate species atsteady-state. Finally, we are interested by the confluence of this simplification, aswell as the relation between the elimination of intermediate species and the computationof the elementary modes of a network.; La biologie des systèmes cherche à comprendre et analyser des systèmes biologiquesà l’aide de modèles mathématiques et informatiques. L’explosion desdonnées expérimentales entraîne des modèles de plus en plus grands. Afin de pouvoirles analyser facilement ou les simuler rapidement, il est alors nécessaire depouvoir les simplifier.Dans cette thèse, nous proposons des méthodes de simplifications de réseauxde réactions biochimiques. Ces méthodes sont suffisamment riches pour pouvoirsimplifier un grand nombre de réseaux provenant d’applications biologiques.Elles sont contextuelles, permettant de considérer un réseau comme un sous moduled’un modèle plus grand, et de le simplifier sans modifier le comportementdu modèle global. Enfin, nos simplifications sont correctes, c’est-à-dire qu’ellespréservent la sémantique des réseaux. Dans un premier temps, nous nous intéressonsà une sémantique non déterministe, basée sur la possibilité de convergervers les attracteurs du réseau. Nous étudions ensuite des simplifications pour lasémantique déterministe, permettant par exemple de supprimer des espèces intermédiairesà l’équilibre. Enfin, nous nous intéressons à la confluence d’une tellesimplification, ainsi qu’au lien entre l’élimination des espèces intermédiaires et lecalcul des modes élémentaires d’un réseau.

Real-time systems must conform to requirements of correctness and safety, which requires testing them. In this thesis, we propose a method that allows to force an execution of a real-time system so as to reach a chosen state. This technique can be used to test real-time systems in situations where the chosen state could be hard to reach when dealing with the input sequence of the system alone. One example of an application could be that of a state that triggers a redundancy mechanism when reached, the execution of which would be infrequent, but that still requires testing. In this use case, it is effectively fault injection in the system. This solution is based on an offline analysis of a set of behavioral models of the system, using the formalism of durational Kripke structures. The models of the system are obtained through a Model Driven Engineering approach, and present the behaviors of the tasks from the point of view of the real-time operating system. Using a parametrization, transformation and composition of the models, we perform a parametric analysis of the resulting Time Petri net. Thanks to the result of this analysis, we establish a set of delays to be added to the execution of the system so as to reach the chosen state. With the help of an embedded model of the different tasks of the system, and through the means of a controller embedded in the real-time operating system, we perform the runtime enforcement of the system so as to make it reach the chosen state, and possibly allow for testing the execution starting from this state. This thesis details the formalisms used to model the application, the way in which the models are modified and analyzed to obtain the execution delays, as well as the implementation in a real-time operating system: TrampolineRTOS.; Les systèmes temps réel doivent répondre à des contraintes d’exactitude et de sureté de fonctionnement, ce qui nécessite de pouvoir les tester. Dans ces travaux de thèse, nous proposons une méthode permettant de forcer une exécution d’un système temps réel de manière à atteindre un état choisi. Cette technique peut permettre le test de systèmes temps réel dans des situations où l’état choisi pourrait être compliqué à atteindre en ne manipulant que les données d’entrée du système. Un exemple d’application pourrait être celui d’un état déclenchant un redondant, et dont l’exécution serait peu fréquente, mais que l’on souhaite néanmoins tester. Dans ce cas d’utilisation, il s’agit effectivement de l’injection de fautes dans le système. Cette solution est basée sur une analyse hors-ligne d’un ensemble de modèles comportementaux du système, utilisant le formalisme des structures de Kripke à durée. Les modèles du système sont issu d’une démarche IDM, et présentent le comportement des tâches du point de vue du système d’exploitation temps réel. À l’aide d’une paramétrisation, transformation et composition des modèles, nous effectuons une analyse paramétrée du réseau de Petri temporel résultant. Grâce au résultat de cette analyse, nous déterminons un ensemble de délais à ajouter à l’exécution du système afin de forcer le système à atteindre l’état choisi. En utilisant un modèle embarqué des différentes tâches, et par le biais d’un contrôleur intégré au système d’exploitation temps réel, nous effectuons le forçage en ligne du système afin de permettre l’atteinte de l’état choisi, et éventuellement le test de l’exécution découlant de cet état. Ce travail de thèse détaille les formalismes utilisés pour modéliser l’application, la manière dont ils sont modifiés et analysés pour obtenir les délais d’exécution, ainsi que l’implémentation dans un système d’exploitation temps réel : TrampolineRTOS.

Real-time systems must conform to requirements of correctness and safety, which requires testing them. In this thesis, we propose a method that allows to force an execution of a real-time system so as to reach a chosen state. This technique can be used to test real-time systems in situations where the chosen state could be hard to reach when dealing with the input sequence of the system alone. One example of an application could be that of a state that triggers a redundancy mechanism when reached, the execution of which would be infrequent, but that still requires testing. In this use case, it is effectively fault injection in the system. This solution is based on an offline analysis of a set of behavioral models of the system, using the formalism of durational Kripke structures. The models of the system are obtained through a Model Driven Engineering approach, and present the behaviors of the tasks from the point of view of the real-time operating system. Using a parametrization, transformation and composition of the models, we perform a parametric analysis of the resulting Time Petri net. Thanks to the result of this analysis, we establish a set of delays to be added to the execution of the system so as to reach the chosen state. With the help of an embedded model of the different tasks of the system, and through the means of a controller embedded in the real-time operating system, we perform the runtime enforcement of the system so as to make it reach the chosen state, and possibly allow for testing the execution starting from this state. This thesis details the formalisms used to model the application, the way in which the models are modified and analyzed to obtain the execution delays, as well as the implementation in a real-time operating system: TrampolineRTOS.; Les systèmes temps réel doivent répondre à des contraintes d’exactitude et de sureté de fonctionnement, ce qui nécessite de pouvoir les tester. Dans ces travaux de thèse, nous proposons une méthode permettant de forcer une exécution d’un système temps réel de manière à atteindre un état choisi. Cette technique peut permettre le test de systèmes temps réel dans des situations où l’état choisi pourrait être compliqué à atteindre en ne manipulant que les données d’entrée du système. Un exemple d’application pourrait être celui d’un état déclenchant un redondant, et dont l’exécution serait peu fréquente, mais que l’on souhaite néanmoins tester. Dans ce cas d’utilisation, il s’agit effectivement de l’injection de fautes dans le système. Cette solution est basée sur une analyse hors-ligne d’un ensemble de modèles comportementaux du système, utilisant le formalisme des structures de Kripke à durée. Les modèles du système sont issu d’une démarche IDM, et présentent le comportement des tâches du point de vue du système d’exploitation temps réel. À l’aide d’une paramétrisation, transformation et composition des modèles, nous effectuons une analyse paramétrée du réseau de Petri temporel résultant. Grâce au résultat de cette analyse, nous déterminons un ensemble de délais à ajouter à l’exécution du système afin de forcer le système à atteindre l’état choisi. En utilisant un modèle embarqué des différentes tâches, et par le biais d’un contrôleur intégré au système d’exploitation temps réel, nous effectuons le forçage en ligne du système afin de permettre l’atteinte de l’état choisi, et éventuellement le test de l’exécution découlant de cet état. Ce travail de thèse détaille les formalismes utilisés pour modéliser l’application, la manière dont ils sont modifiés et analysés pour obtenir les délais d’exécution, ainsi que l’implémentation dans un système d’exploitation temps réel : TrampolineRTOS.

This PhD thesis deals with fault diagnosis of discrete-event systems modeled as finite state automata with some extensions to bounded Petri net models. The developed contributions can be classified regarding two pioneering approaches from the literature: the diagnoser-based technique and the twin-plant based technique. Regarding the diagnoser-based technique, we propose a new diagnoser variant with some interesting features that allow us to reformulate a necessary and sufficient condition for diagnosability of permanent faults and propose a systematic procedure for checking such a condition without building any intermediate model. An on-the-fly algorithm, for simultaneously constructing the diagnoser and verifying diagnosability is then developed. The established diagnoser is then extended to deal with fault diagnosis of intermittent faults. A Hybrid version (in the sense of combining enumerative and symbolic representations) of our diagnoser is also established in order to deal with fault diagnosis of labeled bounded Petri nets. The developed approaches are implemented in dedicated tools and evaluated through benchmarks with respect to the reference approaches in the domain.Regarding twin-plant based technique, our contribution consists in elaborating a model-checking framework that extends the Cimatti's work for the actual verification of various diagnosability concepts pertaining to permanent and intermittent failures based on the twin-plant structure. The main idea is to reformulate and express the diagnosability issues as temporal logics and then to tackle them using the model-checking engines.; L'objet de cette thèse porte sur le diagnostic des systèmes à évènements discrets modélisés par des automates à états finis, avec une extension vers les réseaux de Petri bornés et étiquetés. Les différentes contributions de ce travail peuvent être présentées selon deux volets, au regard des approches pionnières existantes dans la littérature: le diagnostic à base de diagnostiqueur, et le diagnostic à base de twin-plant. Sur le premier volet, i.e., le diagnostic à base de diagnostiqueur, nous proposons une variante du diagnostiqueur avec une nouvelle structure qui nous permet de: (i) formuler une nouvelle condition nécessaire et suffisante pour l'analyse de la diagnosticabilité des fautes permanentes, (ii) développer une procédure systématique pour l'analyse de la diagnosticabilité (iii) établir un algorithme à-la-volée pour construire le diagnostiqueur et analyser la diagnosticabilité en parallèle. Une extension de notre diagnostiqueur pour traiter des fautes intermittentes. Une version hybride de notre diagnostiqueur, pour analyser la diagnosticabilité des réseaux de Petri bornés et étiquetés. Sur le deuxième volet, i.e., le diagnostic à base de twin-plant, nous proposons de nouvelles techniques pour l'analyse de diagnosticabilité de fautes permanentes et intermittentes dans le cadre de vérification par model-checking. Ainsi, la performance des techniques de model-checking et des outils associés peut être exploitée pour traiter des questions de diagnostic.

In recent years Systems Biology has become a rich field of study, trying to encompass all the information that has become available thanks to the new high-throughput techniques of biologists.Fifteen years ago, a fundamental breakthrough was the publication of Kurt Kohn’s map of the cell cycle control in mammals. Its similarity with electronic circuits was crucial in both making it impossible for humans to comprehend fully, and in prompting the use of formal methods.Since then however, the networks built by biologists and modellers have continued growing bigger, filled with more and more mechanistic details, especially recently acquired post-transcriptional information, but lacking most of precise kinetic data. Because analysis techniques providing dynamical insights mostly rely on complete kinetic information, what was challenging for the human ten years ago is now a challenge even for computers,In this manuscript we will try to give an account of our work of the last twelve years, centered around the question of model. We will define more precisely what this object is, formally, and try to handle the challenges raised by the ever growing amount of data, and corresponding size of models developed in Systems Biology. Our main focus will be the links between the structure and dynamics of those models, seen as means to use several formal methods, like Constraint Programming, to reason on their dynamics. Because of the size issue we will also discuss the question of model reduction, and the related relationships between models, formalisms and interpretations.The discrete nature of the structure underlying a model might seem opposed to the continuous dynamics often associated via differential equations to that model. Nevertheless, we hope to demonstrate that the gap between those two views is quite artificial, and that recent results offer very promising perspectives to bridge it.; La Biologie des Systèmes est depuis peu devenue un domaine de recherche florissant qui tente de tirer parti de toutes les informations que les techniques à haut débit des biologistes ont rendues disponibles.Il y a une quinzaine d’années, la publication de la carte du contrôle du cycle cellulaire des mammifères par Kurt Kohn a été une avancée fondamentale. Sa similarité avec un circuit électronique est cruciale dans l’impossibilité pour des humains de l’appréhender complètement mais aussi dans l’idée d’utiliser pour cela des méthodes formelles.Cependant, depuis cette carte, les réseaux construits par les biologistes et modélisateurs ont continué à croître, enrichis de détails mécanistes de plus en plus précis, en particulier des informations post-transcriptionnelles acquises récemment, mais sans données cinétiques précises. Or les méthodes d’analyse qui fournissent des informations dynamiques s’appuient principalement sur une information cinétique complète, par conséquent, ce qui était un défi pour l’humain il y a dix ans l’est devenu pour l’ordinateur aussi.Dans ce manuscrit nous allons tenter de donner une idée de notre travail des douze dernières années, centré autour de la notion de modèle. Nous allons définir plus précisément, et formellement, cet objet, et essayer de répondre aux défis liés au foisonnement des données et à la croissance des modèles de Biologie des Systèmes. Notre approche est fondée sur les liens entre structure et dynamique d’un tel modèle, ces liens permettant d’utiliser de nombreuses méthodes formelles, comme par exemple la programmation par contraintes, pour raisonner sur la dynamique de ces objets. Le problème de la taille nous amènera par ailleurs à envisager les questions de réduction de modèle, mais aussi de liens entre modèles, formalismes et interprétations.La nature discrète de la structure qui sous-tend un modèle peut sembler opposée à la continuité de la dynamique qui lui est souvent associée via des équations différentielles. Cependant nous espérons démontrer que cette séparation est essentiellement artificielle, et que les résultats récents offrent des perspectives prometteuses de la réduire.

Without any doubt, modern multimodal transportation systems are vital to the ecological sustainability and the economic prosperity of urban agglomerations, and in doing so to the quality of life of their many inhabitants. Moreover it is known that a well-functioning interoperability of the different modes and lines in such networked systems is key to their acceptance given the fact that (i) many if not most trips between different origin/destination pairs require transfers, and (ii) costly infrastructure investments targeting the creation of more direct links through the construction of new or the extension of existing lines are not open to debate. Thus, a better understanding of how the different modes and lines in these systems interact through passenger transfers is of utmost importance. However, acquiring this understanding is particularly tricky in degraded situations where some or all transportation services cannot be provided as planned due to e.g. some passenger incident, and/or where the demand for these scheduled services deviates from any statistical long term-plannings. Here, the development for and integration of sophisticated mathematical models into the operation of such systems may provide remedy, where model-predictive supervision seems to be one very promising area of application which we consider here. Model-predictive supervision can take several forms. In this work, we focus on the model-based impact analysis of different actions, such as the delayed departure of some vehicle from a stop, applied to the operation of the considered transportation system upon some downgrading situation occurs which lacks statistical data. For this purpose, we introduce a new stochastic hybrid automaton model, and show how this mathematically profound model can be used to forecast the passenger numbers in and the vehicle operational state of this transportation system starting from estimations of all passenger numbers and an exact knowledge of the vehicle operational state at the time of the incident occurrence. Our new automaton model brings under the same roof, all passengers who demand fixed-route transportation services, and all vehicles which provide them. It explicitly accounts for all capacity-limits and the fact that passengers do not necessarily follow efficient paths which must be mapped to some simple to understand cost function. Instead, every passenger has a trip profile which defines a fixed route in the infrastructure of the transportation system, and a preference for the different transportation services along this route. Moreover, our model does not abstract away from all vehicle movements but explicitly includes them in its dynamics, which latter property is crucial to the impact analysis of any vehicle movement-related action. In addition our model accounts for uncertainty; resulting from unknown initial passenger numbers and unknown passenger arrival flows. Compared to classical modelling approaches for hybrid automata, our Petri net-styled approach does not require the end user to specify our model's many differential equations systems by hand. Instead, all these systems can be derived from the model's predominantly graphical specification in a fully automated manner for the discrete time computation of any forecast. This latter property of our model in turn reduces the risk of man-made specification and thus forecasting errors. Besides introducing our new model, we also develop in this report some algorithmic bricks which target two major bottlenecks which are likely to occur during its forecast-producing simulation, namely the numerical integration of the many high-dimensional systems of stochastic differential equations and the combinatorial explosion of its discrete state. Moreover, we proof the computational feasibility and show the prospective benefits of our approach in form of some simplistic test- and some more realistic use case.; Les réseaux de transport multimodaux modernes sont essentiels pour la durabilité écologique et l’aisance économique des agglomérations urbaines, par conséquent aussi pour la qualité de vie de leurs habitants. D’ailleurs, le bon fonctionnement sur le plan de la compatibilité entre les différents services et lignes est essentiel pour leur acceptation, étant donné que (i) la plupart des trajets nécessitent des changements entre les lignes et que (ii) des investissements coûteux, dans le but de créer des liens plus directs avec la construction de nouvelles lignes ou l’extension de lignes existantes, ne sont pas à débattre. Une meilleure compréhension des interactions entre les modes et les lignes dans le contexte des transferts de passagers est ainsi d’une importance cruciale. Toutefois, comprendre ces transferts est singulièrement difficile dans le cas de situations inhabituelles comme des incidents de passagers et/ou si la demande dévie des plans statistiques à long terme. Ici le développement et l’intégration de modèles mathématiques sophistiqués peuvent remédier à ces inconvénients. À ce propos, la supervision via des modèles prévoyants représente un champ d’application très prometteur, analysée ici. La supervision selon des modèles prévoyants peut prendre différentes formes. Dans le présent travail, nous nous intéressons à l’analyse de l’impact basé sur des modèles de différentes actions, comme des départs en retard de certains véhicules après un arrêt, appliqué sur le fonctionnement du réseau de transport et sa gestion de situations de stress qui ne font pas partie des données statistiques. C’est pourquoi nous introduisons un nouveau modèle, un automate hybride avec une dynamique probabiliste, et nous montrons comment ce modèle profondément mathématique peut prédire le nombre de passagers dans et l’état de fonctionnement du véhicule en question du réseau de transport, d’abord par de simples estimations du nombre de tous les passagers et la connaissance exacte de l’état du véhicule au moment de l’incident. Ce nouvel automate réunit sous un même regard les passagers demandeurs de services de transport à parcours fixes ainsi que les véhicules capables de les assurer. Il prend en compte la capacité maximale et le fait que les passagers n’empruntent pas nécessairement des chemins efficaces, dont la représentation sous la forme d’une fonction de coût facilement compréhensible devient nécessaire. Chaque passager possède son propre profil de voyage qui définit un chemin fixe dans l’infrastructure du réseau de transport, et une préférence pour les différents services de transport sur son chemin. Les mouvements de véhicules sont inclus dans la dynamique du modèle, ce qui est essentiel pour l’analyse de l’impact de chaque action liée aux mouvements de véhicule. De surcroît, notre modèle prend en compte l’incertitude qui résulte du nombre inconnu de passagers au début et de passagers arrivant au fur et à mesure. Comparé aux modèles classiques d’automates hybrides, notre approche inspirée du style des réseaux de Pétri ne requiert pas le calcul de ces équations différentielles à la main. Ces systèmes peuvent être dérivés de la représentation essentiellement graphique d’une manière automatique pour le calcul en temps discret d’une prévision. Cette propriété de notre modèle réduit le risque de précisions faites par des humains et les erreurs qui en résulteraient. Après avoir introduit notre nouveau modèle, nous développons dans ce rapport également quelques éléments constitutifs sous la forme d'algorithmes qui visent les deux types d'impasses qui sont probables d'occurir pendant la simulation faisant un pronostic, c-à-d l'intégration numérique des systèmes de haute dimension d'équations différentielles et l'explosion combinatoire de son état discret. En plus, nous prouvons la faisabilité des calculs et nous montrons les bénéfices prospectifs de notre approche dans la forme de quelques tests simplistes et quelques cas plus réalistes.

Without any doubt, modern multimodal transportation systems are vital to the ecological sustainability and the economic prosperity of urban agglomerations, and in doing so to the quality of life of their many inhabitants. Moreover it is known that a well-functioning interoperability of the different modes and lines in such networked systems is key to their acceptance given the fact that (i) many if not most trips between different origin/destination pairs require transfers, and (ii) costly infrastructure investments targeting the creation of more direct links through the construction of new or the extension of existing lines are not open to debate. Thus, a better understanding of how the different modes and lines in these systems interact through passenger transfers is of utmost importance. However, acquiring this understanding is particularly tricky in degraded situations where some or all transportation services cannot be provided as planned due to e.g. some passenger incident, and/or where the demand for these scheduled services deviates from any statistical long term-plannings. Here, the development for and integration of sophisticated mathematical models into the operation of such systems may provide remedy, where model-predictive supervision seems to be one very promising area of application which we consider here. Model-predictive supervision can take several forms. In this work, we focus on the model-based impact analysis of different actions, such as the delayed departure of some vehicle from a stop, applied to the operation of the considered transportation system upon some downgrading situation occurs which lacks statistical data. For this purpose, we introduce a new stochastic hybrid automaton model, and show how this mathematically profound model can be used to forecast the passenger numbers in and the vehicle operational state of this transportation system starting from estimations of all passenger numbers and an exact knowledge of the vehicle operational state at the time of the incident occurrence. Our new automaton model brings under the same roof, all passengers who demand fixed-route transportation services, and all vehicles which provide them. It explicitly accounts for all capacity-limits and the fact that passengers do not necessarily follow efficient paths which must be mapped to some simple to understand cost function. Instead, every passenger has a trip profile which defines a fixed route in the infrastructure of the transportation system, and a preference for the different transportation services along this route. Moreover, our model does not abstract away from all vehicle movements but explicitly includes them in its dynamics, which latter property is crucial to the impact analysis of any vehicle movement-related action. In addition our model accounts for uncertainty; resulting from unknown initial passenger numbers and unknown passenger arrival flows. Compared to classical modelling approaches for hybrid automata, our Petri net-styled approach does not require the end user to specify our model's many differential equations systems by hand. Instead, all these systems can be derived from the model's predominantly graphical specification in a fully automated manner for the discrete time computation of any forecast. This latter property of our model in turn reduces the risk of man-made specification and thus forecasting errors. Besides introducing our new model, we also develop in this report some algorithmic bricks which target two major bottlenecks which are likely to occur during its forecast-producing simulation, namely the numerical integration of the many high-dimensional systems of stochastic differential equations and the combinatorial explosion of its discrete state. Moreover, we proof the computational feasibility and show the prospective benefits of our approach in form of some simplistic test- and some more realistic use case.; Les réseaux de transport multimodaux modernes sont essentiels pour la durabilité écologique et l’aisance économique des agglomérations urbaines, par conséquent aussi pour la qualité de vie de leurs habitants. D’ailleurs, le bon fonctionnement sur le plan de la compatibilité entre les différents services et lignes est essentiel pour leur acceptation, étant donné que (i) la plupart des trajets nécessitent des changements entre les lignes et que (ii) des investissements coûteux, dans le but de créer des liens plus directs avec la construction de nouvelles lignes ou l’extension de lignes existantes, ne sont pas à débattre. Une meilleure compréhension des interactions entre les modes et les lignes dans le contexte des transferts de passagers est ainsi d’une importance cruciale. Toutefois, comprendre ces transferts est singulièrement difficile dans le cas de situations inhabituelles comme des incidents de passagers et/ou si la demande dévie des plans statistiques à long terme. Ici le développement et l’intégration de modèles mathématiques sophistiqués peuvent remédier à ces inconvénients. À ce propos, la supervision via des modèles prévoyants représente un champ d’application très prometteur, analysée ici. La supervision selon des modèles prévoyants peut prendre différentes formes. Dans le présent travail, nous nous intéressons à l’analyse de l’impact basé sur des modèles de différentes actions, comme des départs en retard de certains véhicules après un arrêt, appliqué sur le fonctionnement du réseau de transport et sa gestion de situations de stress qui ne font pas partie des données statistiques. C’est pourquoi nous introduisons un nouveau modèle, un automate hybride avec une dynamique probabiliste, et nous montrons comment ce modèle profondément mathématique peut prédire le nombre de passagers dans et l’état de fonctionnement du véhicule en question du réseau de transport, d’abord par de simples estimations du nombre de tous les passagers et la connaissance exacte de l’état du véhicule au moment de l’incident. Ce nouvel automate réunit sous un même regard les passagers demandeurs de services de transport à parcours fixes ainsi que les véhicules capables de les assurer. Il prend en compte la capacité maximale et le fait que les passagers n’empruntent pas nécessairement des chemins efficaces, dont la représentation sous la forme d’une fonction de coût facilement compréhensible devient nécessaire. Chaque passager possède son propre profil de voyage qui définit un chemin fixe dans l’infrastructure du réseau de transport, et une préférence pour les différents services de transport sur son chemin. Les mouvements de véhicules sont inclus dans la dynamique du modèle, ce qui est essentiel pour l’analyse de l’impact de chaque action liée aux mouvements de véhicule. De surcroît, notre modèle prend en compte l’incertitude qui résulte du nombre inconnu de passagers au début et de passagers arrivant au fur et à mesure. Comparé aux modèles classiques d’automates hybrides, notre approche inspirée du style des réseaux de Pétri ne requiert pas le calcul de ces équations différentielles à la main. Ces systèmes peuvent être dérivés de la représentation essentiellement graphique d’une manière automatique pour le calcul en temps discret d’une prévision. Cette propriété de notre modèle réduit le risque de précisions faites par des humains et les erreurs qui en résulteraient. Après avoir introduit notre nouveau modèle, nous développons dans ce rapport également quelques éléments constitutifs sous la forme d'algorithmes qui visent les deux types d'impasses qui sont probables d'occurir pendant la simulation faisant un pronostic, c-à-d l'intégration numérique des systèmes de haute dimension d'équations différentielles et l'explosion combinatoire de son état discret. En plus, nous prouvons la faisabilité des calculs et nous montrons les bénéfices prospectifs de notre approche dans la forme de quelques tests simplistes et quelques cas plus réalistes.

International audience; The mechatronic systems are hybrid, dynamic, interactive and reconfigurable. Therefore their dysfunctional modeling is very difficult. Multi-physical interactions between components have impacts on the degradation or on system failures, leading thus to more uncertainty in reliability evaluation.The work presented in this paper aims to improve the integration of multi-domain interactions in the reliability assessment of mechatronic systems.After a presentation of the state of the art of mechatronic systems reliability estimation methods, we propose to represent multi domain interactions by influential factors in the dysfunctional model.We generally use proportional hazard models; in the case of an interaction represented by a temperature stress, Arrhenius model is used.; Les systèmes mécatroniques sont à la fois hybrides, dynamiques, interactifs et reconfigurables, ce qui entraîne des difficultés dans la modélisation dysfonctionnelle. Les potentielles interactions multi-physiques entre les composants peuvent avoir des impacts sur les dégradations ou sur les dysfonctionnements du système. Tous ces éléments à prendre en compte rendent incertain le modèle d’évaluation de la fiabilité.Le travail de recherche présenté dans cet article a pour but d’améliorer la prise en compte des interactions multi-domaines dans l’évaluation de la fiabilité des systèmes mécatroniques.A partir d’un état de l’art des méthodes d’évaluation de la fiabilité des systèmes mécatroniques, nous proposons des améliorations permettant une prise en compte quantitative des interactions par l’intégration de facteurs d’influence représentant des interactions multi domaines.Cette intégration est effectuée de manière générale à partir d’un modèle à hasards proportionnels et, dans le cas d’une interaction avec pour facteur de stress la température, en utilisant la loi d’Arrhenius.

Petri nets and their extensions are a well-known formalism for modeling the specification of discrete events systems real-time. For these systems, the demands of verification and validation are essential to ensure their smooth functioning because the least error can lead to catastrophic consequences. To analyze the behavior of the system, it is common to construct the state graph (or state space) which lists exhaustively the different accessible states. This graph allows to check the generic properties such as boundedness, accessibility, termination, vivacity, the absence of blocking, etc. But building this state space is confronted with the problem of combinatorial explosion of the number of states related to the complexity and concurrence of the system. One of the alternatives to contain this combination is to keep only partial orders between events. Unfolding is a partial order adapted to technical verification, diagnosis and planning. This thesis contributes to the study of the unfolding of Petri nets and, in particular, his contributes to the unfolding of Petri nets with reset arcs. Moreover, the unfolding explains the possible executions of the system which are, by definition, the processes. This is specifically the branching processes that differ from conventional processes. Thus, we propose an algebra adapted to the branching process from unfolding of Petri nets; Les réseaux de Petri et leurs extensions constituent un formalisme très connu pour la modélisation de la spécification des systèmes à évènements discrets temps réel. Pour ces systèmes, les exigences de vérification et de validation sont indispensables pour garantir leur bon fonctionnement car la moindre erreur peut entrainer des conséquences catastrophiques. Pour analyser le comportement du système, il est courant de construire le graphe d'états (ou espace d'états) qui énumère de façon exhaustive les différents états accessibles. Ce graphe permet de vérifier des propriétés génériques comme le caractère borné, l'accessibilité, la terminaison, la vivacité, l'absence de blocage, etc. Mais la construction de cet espace d'états est confrontée au problème d'explosion combinatoire du nombre d'états lié à la complexité et à la concurrence du système. L'une des alternatives pour contenir cette combinatoire est de conserver uniquement les ordres partiels entre les évènements. Le dépliage est une technique d'ordre partiel adaptée à la vérification, au diagnostic et à la planification. Cette thèse contribue à l'étude du dépliage des réseaux de Petri et, plus particulièrement, apporte une contribution au dépliage des réseaux de Petri avec des arcs de reset. De plus, le dépliage explicite les exécutions possibles du système qui sont, par définition, des processus. Il s'agit plus précisément des processus de branchement qui diffèrent des processus classiques. Ainsi, nous proposons une algèbre adaptée aux processus de branchement issus du dépliage des réseaux de Petri.

Petri nets and their extensions are a well-known formalism for modeling the specification of discrete events systems real-time. For these systems, the demands of verification and validation are essential to ensure their smooth functioning because the least error can lead to catastrophic consequences. To analyze the behavior of the system, it is common to construct the state graph (or state space) which lists exhaustively the different accessible states. This graph allows to check the generic properties such as boundedness, accessibility, termination, vivacity, the absence of blocking, etc. But building this state space is confronted with the problem of combinatorial explosion of the number of states related to the complexity and concurrence of the system. One of the alternatives to contain this combination is to keep only partial orders between events. Unfolding is a partial order adapted to technical verification, diagnosis and planning. This thesis contributes to the study of the unfolding of Petri nets and, in particular, his contributes to the unfolding of Petri nets with reset arcs. Moreover, the unfolding explains the possible executions of the system which are, by definition, the processes. This is specifically the branching processes that differ from conventional processes. Thus, we propose an algebra adapted to the branching process from unfolding of Petri nets; Les réseaux de Petri et leurs extensions constituent un formalisme très connu pour la modélisation de la spécification des systèmes à évènements discrets temps réel. Pour ces systèmes, les exigences de vérification et de validation sont indispensables pour garantir leur bon fonctionnement car la moindre erreur peut entrainer des conséquences catastrophiques. Pour analyser le comportement du système, il est courant de construire le graphe d'états (ou espace d'états) qui énumère de façon exhaustive les différents états accessibles. Ce graphe permet de vérifier des propriétés génériques comme le caractère borné, l'accessibilité, la terminaison, la vivacité, l'absence de blocage, etc. Mais la construction de cet espace d'états est confrontée au problème d'explosion combinatoire du nombre d'états lié à la complexité et à la concurrence du système. L'une des alternatives pour contenir cette combinatoire est de conserver uniquement les ordres partiels entre les évènements. Le dépliage est une technique d'ordre partiel adaptée à la vérification, au diagnostic et à la planification. Cette thèse contribue à l'étude du dépliage des réseaux de Petri et, plus particulièrement, apporte une contribution au dépliage des réseaux de Petri avec des arcs de reset. De plus, le dépliage explicite les exécutions possibles du système qui sont, par définition, des processus. Il s'agit plus précisément des processus de branchement qui diffèrent des processus classiques. Ainsi, nous proposons une algèbre adaptée aux processus de branchement issus du dépliage des réseaux de Petri.

This article focuses on the representation of Common Cause Failures (CCF) in large distributed systems whose they occur either in operation or in the solicitation modes. The notion of “oriented CCF” proposed here extends the Atwood model. It takes into account three root causes of failures: hardware, software and human factor. The oriented CCF are modelled using coloured Petri nets. The sensitivity studies have identified the input data having the most influence on the probability of failure on demand (PFD) of the system., Cet article s’intéresse à la représentation des Défaillances de Cause Commune (DCC) dans les systèmes distribués de grande taille et dont leur occurrence peut se produire soit en fonctionnement, soit à la sollicitation. La notion de « DCC orientée » proposée étend le modèle d’Atwood. Elle prend en compte trois causes profondes de défaillances : matérielles, logicielles et facteur humain. Les DCC orientées sont modélisées à l’aide des Réseaux de Petri colorés. Les études de sensibilité réalisées ont permis d’identifier les données d’entrée ayant le plus d’influence sur la probabilité de défaillance à la sollicitation (PFD) du système.

L'un des aspects fondamentaux des systèmes informatiques modernes, et en particulier des systèmes critiques, est la possibilité d'exécuter plusieurs processus, partageant des ressources communes, de façon simultanée. De par leur nature concurrentielle, le bon fonctionnement de ces systèmes n'est assuré que lorsque leurs comportements ne dépendent pas d'un ordre d'exécution prédéterminé. En raison de cette caractéristique, il est particulièrement difficile de s'assurer qu'un système concurrent ne possède pas de faille. Dans cette thèse, nous étudions la vérification formelle, une approche algorithmique qui vise à automatiser la vérification du bon fonctionnement de systèmes concurrents en procédant par une abstraction vers des modèles mathématiques. Nous considérons deux de ces modèles, les réseaux de Petri et les systèmes d'addition de vecteurs, et les problèmes de vérification qui leur sont associés. Nous montrons que le problème d'accessibilité pour les systèmes d'addition de vecteurs (avec états) à deux compteurs est PSPACE-complet, c'est-à-dire complet pour la classe des problèmes solubles à l'aide d'une quantité polynomiale de mémoire. Nous établissons ainsi la complexité calculatoire précise de ce problème, répondant à une question demeurée ouverte depuis plus de trente ans. Nous proposons une nouvelle approche au problème de couverture pour les réseaux de Petri, basée sur un algorithme arrière guidé par une caractérisation logique de l'accessibilité dans les réseaux de Petri continus. Cette approche nous a permis de mettre au point un nouvel algorithme qui s'avère particulièrement efficace en pratique, tel que démontré par notre implémentation logicielle nommée QCover. Nous complétons ces résultats par une étude des systèmes de transitions bien structurés qui constituent une abstraction générale des systèmes d'addition de vecteurs et des réseaux de Petri. Nous considérons le cas des systèmes de transitions bien structurés à branchement infini, une classe qui inclut les réseaux de Petri possédant des arcs pouvant consommer ou produire un nombre arbitraire de jetons. Nous développons des outils mathématiques facilitant l'étude de ces systèmes et nous délimitons les frontières au-delà desquelles la décidabilité des problèmes de terminaison, de finitude, de maintenabilité et de couverture est perdue., One fundamental aspect of computer systems, and in particular of critical systems, is the ability to run simultaneously many processes sharing resources. Such concurrent systems only work correctly when their behaviours are independent of any execution ordering. For this reason, it is particularly difficult to ensure the correctness of concurrent systems. In this thesis, we study formal verification, an algorithmic approach to the verification of concurrent systems based on mathematical modeling. We consider two of the most prominent models, Petri nets and vector addition systems, and their usual verification problems considered in the literature. We show that the reachability problem for vector addition systems (with states) restricted to two counters is PSPACE-complete, that is, it is complete for the class of problems solvable with a polynomial amount of memory. Hence, we establish the precise computational complexity of this problem, left open for more than thirty years. We develop a new approach to the coverability problem for Petri nets which is primarily based on applying forward coverability in continuous Petri nets as a pruning criterion inside a backward coverability framework. We demonstrate the effectiveness of our approach by implementing it in a tool named QCover. We complement these results with a study of well-structured transition systems which form a general abstraction of vector addition systems and Petri nets. We consider infinitely branching well-structured transition systems, a class that includes Petri nets with special transitions that may consume or produce arbitrarily many tokens. We develop mathematical tools in order to study these systems and we delineate the decidability frontier for the termination, boundedness, maintainability and coverability problems., Réalisé en cotutelle avec l'École normale supérieure de Cachan – Université Paris-Saclay

Cross docking is an efficient and dynamic logistic process that directly transfers goods from a supplier to a customer. This thesis addresses the door assignment and resource management problem with truck time windows constraints for a specific cross dock. The problems are formulated as mixed integer programming (MIP) models. The objective is to minimize the weighted sum of the total travel distance and cost which includes labor cost and penalty cost. A heuristic based on genetic algorithm (GA) is developed to solve the problems. Two gene repair methods are proposed to repair infeasible solutions. The computational results show that genetic algorithms outperforms the solution of MIP model with CPLEX in a given CPU time, for medium and large size instances, and that the second gene repair method outperforms the first one. In order to describe the behavior and gather information on the cross dock, a model based on Petri net is built to study the cross docks and simulations are carried out with Tina. The simulation results for different resource number lead us to obtain the relevant times to improve the original time windows, the makespan at each work station, the free time interval in the cross dock and the free resource number at each time period, which provide relevant information on the resource management. Besides, according to the simulation results, the original MIP formulations are improved. Then we propose a new MIP formulation, which determine not only door assignment, but also resources at each time period at each work station. Computational results reveal that the new MIP model control resources in cross dock more efficiently and outperforms the first model.; La gestion d’une plate-forme selon une stratégie de cross dock est un processus logistique efficace et dynamique qui vise à transférer directement les produits d'un fournisseur à un client. Cette thèse aborde les problèmes d'affectation aux portes et de gestion des ressources sous contraintes de fenêtres du temps dans un cross dock spécifique. Les problèmes sont formulés comme des modèles de programmation mathématique mixte (MIP). L’objectif est de minimiser la somme de la distance parcourue dans l’entrepôt et du coût qui contient les coûts liés aux ressources et un coût de pénalité. Une heuristique basée sur les algorithmes génétiques est proposée pour résoudre ce problème. Deux méthodes de réparation des gènes sont décrites pour rendre les solutions irréalisables réalisables. Les résultats montrent que l’algorithme génétique surpasse la résolution du modèle MIP à l’aide du solveur CPLEX en un temps donné, pour des instances de taille moyenne et de grande taille. Afin de décrire le comportement et de recueillir des informations pertinentes sur la gestion en cross docks, nous proposons un modèle basé sur réseau de Pétri. Un modèle par réseau de Pétri est construit et la simulation est réalisée avec le logiciel Tina. Par simulation, avec différents nombres de ressources, nous obtenons des temps pertinents pour améliorer les fenêtres de temps originales, le makespan de chacun des postes de travail, l'intervalle de temps libre dans le cross dock et la quantité de ressources disponible à chaque période de temps, ce qui peut fournir des conseils utiles à la gestion des ressources. A partir des résultats de la simulation, la formulation MIP est améliorée.

The deadlock control and liveness-enforcement are mostly implemented based on siphons in most existing work using structural theory. Our previous work has revealed a kind of intrinsically live structures in a class of generalized Petri nets called systems of simple sequential processes with weighted resources allocation (WS 3 PR). The liveness-enforcement is achieved by analyzing the structure including weight information and reconfiguring the initial marking of resource places without considering the initial token counts in idle process places. This work extends it to a more general class than WS 3 PR. Instead of siphons, a new concept of structural objects is defined to carry weight information and reflect the circular waits of resources. The numerical relationship between initial markings of resource places and weights of arcs is investigated to yield an intrinsically live structure-based liveness-enforcing method that requires no external monitors. The work provides an insight into structures of generalized Petri nets and a new revenue to achieve the desired deadlock control. Several examples are used to illustrate the proposed method.

International audience; More than a multi-technology fusion, mechatronic systems are becoming more and more complex, these systems can be reconfigured with changes in the environment and states of the functional units, evaluating and improving the reliability of mechatronic system requires to take into account the reconfigurable aspect. This point has become a major challenge for reliability engineers during the design phase. Therefore their dysfunctional modeling is very difficult. This communication presents an original proposed methodology for evaluating the reliability of mechatronic system with taking account the reconfigurable aspect. This reliability model integrates the change of the configuration related to the external and internal conditions.; Plus qu’une fusion multi-technologique, les systèmes mécatroniques deviennent de plus en plus complexes, ces systèmes peuvent être reconfigurés avec des changements dans l’environnement et les états des unités fonctionnelles. Evaluer et améliorer la fiabilité d’un système mécatronique en prenant en compte cet aspect reconfigurable est devenu un défi majeur pour les fiabilistes lors de phase de conception. Dans cette communications, nous proposons une méthodologie originale, d’évaluation de fiabilité des systèmes mécatroniques avec la prise en compte l’aspect reconfigurable, nous abordons un modèle fiabiliste qui intègre le changement de la configuration liée à la fois aux conditions externes et internes d’un système mécatronique.

Ces travaux s'intéressent à la modélisation des Défaillances de Cause commune (DCC) et l’évaluation des probabilités des DCC dans des systèmes complexes programmés en Réseaux de Petri coloré, hiérarchiques et stochastiques. L’objectif de cette étude est de mettre à jour le modèle des DCC sur CPN Tools grâce aux retours d’expérience générés par AREVA, principalement pour les DCC d’origine logicielle sur lesquelles on dispose de peu d’informations. Plusieurs études de sensibilité ont été menées afin d’identifier les paramètres qui influencent le plus la disponibilité du système.Le second objectif de cette étude est de montrer qu’il est possible de transférer les modèles actuels sur le logiciel PyCATSHOO, représentant des Automates Stochastiques Hybrides, et ce dans un but d’optimisation des performances. Un cas test a été défini afin de comparer les performances de ces deux logiciels.Cette étude permet d’étendre les connaissances sur le phénomène des DCC qui sont un grand enjeu de la sûreté de fonctionnement et de la disponibilité des systèmes critiques.

In this work, we present different control synthesis approaches based on Petri nets and the theory of regions. This theory has some limitations in supervisory control. Indeed, the design on the PN controller, if it exists, is not an easy task due to the resolution complexity and the combinatorial explosion of states in the generated reachability graph. In addition, the linear system of the theory of regions may contain convex combinations of its equations making the theory insoluble. This work aims to simplify the computational complexity of the theory of regions by reducing the number of equations of the linear system and decreasing the computation time of PN controllers. Consequently, new concepts of minimal cuts and canonic markings are introduced in order to apply the theory of regions on specific zones of the graph and not on the whole reachability graph. Finally, two new approaches are developed to synthesize PN controllers without generating the reachability graph, Dans ce mémoire, nous présentons différentes approches de synthèse de contrôleurs réseaux de Petri en se basant sur la théorie des régions. Cette théorie présente quelques limites dans la synthèse de contrôle. En effet, la synthèse du contrôleur RdP, s’il existe, n’est pas du tout une tâche facile vue sa complexité de calcul et l’explosion combinatoire des états dans le graphe de marquage. De plus, le système linéaire de la théorie des régions à résoudre peut contenir des combinaisons convexes entre ces équations ce qui rend la théorie insoluble pour calculer les superviseurs RdP. Ce travail vise à simplifier la complexité de calcul de la théorie des régions en réduisant le nombre d’équations du système linéaire de la théorie des régions d’une part, et d’autre part en minimisant le temps de calcul des contrôleurs RdP. De nouveaux concepts de coupes minimales et de marquages canoniques ont été introduits afin d’appliquer la théorie des régions sur des zones précises du graphe et non pas sur la totalité du graphe de marquage. Finalement, deux autres nouvelles approches ont été développées pour synthétiser des contrôleurs RdP sans générer le graphe de marquage

This PhD thesis deals with fault diagnosis of discrete-event systems modeled as finite state automata with some extensions to bounded Petri net models. The developed contributions can be classified regarding two pioneering approaches from the literature: the diagnoser-based technique and the twin-plant based technique. Regarding the diagnoser-based technique, we propose a new diagnoser variant with some interesting features that allow us to reformulate a necessary and sufficient condition for diagnosability of permanent faults and propose a systematic procedure for checking such a condition without building any intermediate model. An on-the-fly algorithm, for simultaneously constructing the diagnoser and verifying diagnosability is then developed. The established diagnoser is then extended to deal with fault diagnosis of intermittent faults. A Hybrid version (in the sense of combining enumerative and symbolic representations) of our diagnoser is also established in order to deal with fault diagnosis of labeled bounded Petri nets. The developed approaches are implemented in dedicated tools and evaluated through benchmarks with respect to the reference approaches in the domain.Regarding twin-plant based technique, our contribution consists in elaborating a model-checking framework that extends the Cimatti's work for the actual verification of various diagnosability concepts pertaining to permanent and intermittent failures based on the twin-plant structure. The main idea is to reformulate and express the diagnosability issues as temporal logics and then to tackle them using the model-checking engines., L'objet de cette thèse porte sur le diagnostic des systèmes à évènements discrets modélisés par des automates à états finis, avec une extension vers les réseaux de Petri bornés et étiquetés. Les différentes contributions de ce travail peuvent être présentées selon deux volets, au regard des approches pionnières existantes dans la littérature: le diagnostic à base de diagnostiqueur, et le diagnostic à base de twin-plant. Sur le premier volet, i.e., le diagnostic à base de diagnostiqueur, nous proposons une variante du diagnostiqueur avec une nouvelle structure qui nous permet de: (i) formuler une nouvelle condition nécessaire et suffisante pour l'analyse de la diagnosticabilité des fautes permanentes, (ii) développer une procédure systématique pour l'analyse de la diagnosticabilité (iii) établir un algorithme à-la-volée pour construire le diagnostiqueur et analyser la diagnosticabilité en parallèle. Une extension de notre diagnostiqueur pour traiter des fautes intermittentes. Une version hybride de notre diagnostiqueur, pour analyser la diagnosticabilité des réseaux de Petri bornés et étiquetés. Sur le deuxième volet, i.e., le diagnostic à base de twin-plant, nous proposons de nouvelles techniques pour l'analyse de diagnosticabilité de fautes permanentes et intermittentes dans le cadre de vérification par model-checking. Ainsi, la performance des techniques de model-checking et des outils associés peut être exploitée pour traiter des questions de diagnostic.

In this work, we present different control synthesis approaches based on Petri nets and the theory of regions. This theory has some limitations in supervisory control. Indeed, the design on the PN controller, if it exists, is not an easy task due to the resolution complexity and the combinatorial explosion of states in the generated reachability graph. In addition, the linear system of the theory of regions may contain convex combinations of its equations making the theory insoluble. This work aims to simplify the computational complexity of the theory of regions by reducing the number of equations of the linear system and decreasing the computation time of PN controllers. Consequently, new concepts of minimal cuts and canonic markings are introduced in order to apply the theory of regions on specific zones of the graph and not on the whole reachability graph. Finally, two new approaches are developed to synthesize PN controllers without generating the reachability graph, Dans ce mémoire, nous présentons différentes approches de synthèse de contrôleurs réseaux de Petri en se basant sur la théorie des régions. Cette théorie présente quelques limites dans la synthèse de contrôle. En effet, la synthèse du contrôleur RdP, s’il existe, n’est pas du tout une tâche facile vue sa complexité de calcul et l’explosion combinatoire des états dans le graphe de marquage. De plus, le système linéaire de la théorie des régions à résoudre peut contenir des combinaisons convexes entre ces équations ce qui rend la théorie insoluble pour calculer les superviseurs RdP. Ce travail vise à simplifier la complexité de calcul de la théorie des régions en réduisant le nombre d’équations du système linéaire de la théorie des régions d’une part, et d’autre part en minimisant le temps de calcul des contrôleurs RdP. De nouveaux concepts de coupes minimales et de marquages canoniques ont été introduits afin d’appliquer la théorie des régions sur des zones précises du graphe et non pas sur la totalité du graphe de marquage. Finalement, deux autres nouvelles approches ont été développées pour synthétiser des contrôleurs RdP sans générer le graphe de marquage

In order to achieve responsiveness, flexibility, cost reduction and increased productivity, companies searching for solutions to conventional manufacturing control in terms of robustness, adaptability, rapid configuration and an efficient use of resources. The Holonic and Service-oriented Architectures have been proposed as solutions for the conception of such kind of systems, the former ( in the manufacturing), providing flexibility at the control level, the latter ( in the computer science) at a process level. The combination of both has been recognized as a very attractive solution for the design of the Next Generation Manufacturing Systems. However, the integration of the concept of services needs new models to adapt to the manufacturing context, specifically for process planning and scheduling. This work proposes a product driven Service Oriented Holonic Manufacturing System architecture (SoHMS) as a methodology for modeling flexible production systems with a set of models and prescriptive methodologies for its specification. As models, we contribute with a manufacturing service model (MService) and a computational Flexible Petri-Net based Process Model; an orchestration protocol and strategies for the Integrated Process Planning and Scheduling of such processes for the effective and efficient exploration of solutions while dealing with the problem of combinatorial complexity; as well as the holonic models and protocols forming the SoHMS architecture. As methodologies, we propose a framework for: conceiving manufacturing services and processes specifications, the creation of an application service-ontology, and a methodology for modeling flexible petri- net models.; Pour atteindre des objectifs en termes de réactivité, flexibilité, réduction des coûts et augmentation de laproductivité, les entreprises sont à la recherche de solutions remplaçant les systèmes de contrôlemanufacturiers conventionnels afin de gagner en robustesse, adaptabilité, configuration rapide etmaximisation de l’utilisation des ressources. Les Architectures Holoniques et Orientées-Services ont étéproposées en tant que solutions de conception pour de tels types de systèmes, le premier dans le domainemanufacturier fournissant de la flexibilité au niveau contrôle, le dernier en informatique au niveau processus.La combinaison de ces deux architectures a été reconnue comme une solution encore plus attractive pour laconception des systèmes de production de prochaine génération. .Cependant, l’intégration du concept de services nécessite de nouveaux modèles pour s’adapter au contextemanufacturier et lui octroyer de la flexibilité, particulièrement pour la planification et l’ordonnancement auniveau processus.Ce travail propose une architecture pour Système de Production Holonique Orienté-Services (ServiceOriented Holonic Manufacturing System (SOHMS)), piloté autour des produits, en tant que méthodologiepour modéliser les systèmes de production flexibles en utilisant un ensemble de modèles et méthodologiespour sa spécification. Au niveau des modèles, notre contribution se porte sur un modèle de service adapté àla production, un modèle flexible de processus basé sur les Réseaux de Petri, un protocole d’orchestration etdes stratégies pour l’ordonnancement et la planification intégrés de ces processus (Integrated ProcessPlanning and Scheduling) afin d’explorer efficacement les solutions offertes tout en évitant une explosioncombinatoire, et des modèles et protocoles holoniques permettant de former une architecture SOHMS. Auniveau méthodologique, nous proposons un framework permettant de concevoir des services de productionet des spécifications de processus, la création d’une ontologie de services d’application et une méthodologiepour modéliser les gammes sous forme de Réseaux de Petri.Le SOHMS résultant est un système ayant la possibilité de créer des plans de production flexibles adaptablesen fonction des aléas survenant sur le système, ayant la capacité d’intégrer rapidement et facilement desnouvelles ressources et compétences et sachant proposer des solutions faisables de production avant l’arrivéeaux points de décision correspondants.

In order to achieve responsiveness, flexibility, cost reduction and increased productivity, companies searching for solutions to conventional manufacturing control in terms of robustness, adaptability, rapid configuration and an efficient use of resources. The Holonic and Service-oriented Architectures have been proposed as solutions for the conception of such kind of systems, the former ( in the manufacturing), providing flexibility at the control level, the latter ( in the computer science) at a process level. The combination of both has been recognized as a very attractive solution for the design of the Next Generation Manufacturing Systems. However, the integration of the concept of services needs new models to adapt to the manufacturing context, specifically for process planning and scheduling. This work proposes a product driven Service Oriented Holonic Manufacturing System architecture (SoHMS) as a methodology for modeling flexible production systems with a set of models and prescriptive methodologies for its specification. As models, we contribute with a manufacturing service model (MService) and a computational Flexible Petri-Net based Process Model; an orchestration protocol and strategies for the Integrated Process Planning and Scheduling of such processes for the effective and efficient exploration of solutions while dealing with the problem of combinatorial complexity; as well as the holonic models and protocols forming the SoHMS architecture. As methodologies, we propose a framework for: conceiving manufacturing services and processes specifications, the creation of an application service-ontology, and a methodology for modeling flexible petri- net models.; Pour atteindre des objectifs en termes de réactivité, flexibilité, réduction des coûts et augmentation de laproductivité, les entreprises sont à la recherche de solutions remplaçant les systèmes de contrôlemanufacturiers conventionnels afin de gagner en robustesse, adaptabilité, configuration rapide etmaximisation de l’utilisation des ressources. Les Architectures Holoniques et Orientées-Services ont étéproposées en tant que solutions de conception pour de tels types de systèmes, le premier dans le domainemanufacturier fournissant de la flexibilité au niveau contrôle, le dernier en informatique au niveau processus.La combinaison de ces deux architectures a été reconnue comme une solution encore plus attractive pour laconception des systèmes de production de prochaine génération. .Cependant, l’intégration du concept de services nécessite de nouveaux modèles pour s’adapter au contextemanufacturier et lui octroyer de la flexibilité, particulièrement pour la planification et l’ordonnancement auniveau processus.Ce travail propose une architecture pour Système de Production Holonique Orienté-Services (ServiceOriented Holonic Manufacturing System (SOHMS)), piloté autour des produits, en tant que méthodologiepour modéliser les systèmes de production flexibles en utilisant un ensemble de modèles et méthodologiespour sa spécification. Au niveau des modèles, notre contribution se porte sur un modèle de service adapté àla production, un modèle flexible de processus basé sur les Réseaux de Petri, un protocole d’orchestration etdes stratégies pour l’ordonnancement et la planification intégrés de ces processus (Integrated ProcessPlanning and Scheduling) afin d’explorer efficacement les solutions offertes tout en évitant une explosioncombinatoire, et des modèles et protocoles holoniques permettant de former une architecture SOHMS. Auniveau méthodologique, nous proposons un framework permettant de concevoir des services de productionet des spécifications de processus, la création d’une ontologie de services d’application et une méthodologiepour modéliser les gammes sous forme de Réseaux de Petri.Le SOHMS résultant est un système ayant la possibilité de créer des plans de production flexibles adaptablesen fonction des aléas survenant sur le système, ayant la capacité d’intégrer rapidement et facilement desnouvelles ressources et compétences et sachant proposer des solutions faisables de production avant l’arrivéeaux points de décision correspondants.

National audience; Cet article présente un environnement de génération de règles de coordination à partir de réseaux de Petri colorés. L’environnement proposé est basé sur un langage dédié appelé cpnDSL. À partir d’une spécification cpnDSL décrivant un système donné, des règles de coordination correctes par construction et directement exécutables dans l’environement LINC sont générées. Un modèle vérifiable pour valider le comportement du système et un modèle graphique pour permettre la discussion entre les différents membres du projet sont également générés. Une étude de cas issue du domaine du transport est présentée pour illustrer l’approche proposée.

L'objectif de cette communication est de représenter les études permettant une meilleure maîtrise des risques et de la fiabilité. Les points faibles sont mis en évidence, ces études de sûreté de fonctionnement doivent être menées au plus tôt dans la phase de conception, afin de réduire les coûts et le nombre de prototypes nécessaires à la validation du système. L'estimation de la fiabilité prévisionnelle, d'un système mécatronique est modélisée par une analyse qualitative et quantitative grâce aux Réseaux de Pétri stochastiques, et pour l'estimation de la fiabilité opérationnelle et expérimentale, l'intégration des Réseaux Bayésiens et un recueil d'expérience sont bien présents comme un outil performant, portant d'autres travaux pour l'optimisation des essaies accélérés.

In the last decades, very great research and development efforts have been made to develop and promote electric vehicles (EVs). Most efforts have been made to further develop the power engine of these vehicles and batteries technologies. However, one of the major obstacles to the large deployment of EVs is the uncertainty of drivers to get a suitable and vacant place at a charging station (CS). In this manuscript, we focus on the charging process modelling using formal approaches based on discrete event system tools namely (max,+) algebra and Petri nets. In addition, an optimization approach based on linear programming is proposed to optimally assign and reroute EVs to the suitable CSs and schedule their charging operations. In order to predict, manage and handle charging needs of EVs, a dedicated model based on a predictive function is introduced. The aim is to predict the average charging rate and time while considering the inter-arrival of charging requests and the state of charging of EVs. Using this approach, charging operations could be planned while minimizing waiting times of EVs and avoiding queuing situations within CSs. Simulation results showed that the proposed approaches allow assigning adequately and optimally EVs to CSs while satisfying all process constraints., Au cours des dernières décennies, de grands efforts en recherche et développement ont été faits pour développer et promouvoir les véhicules électriques (VEs). La plupart de ces recherches portent essentiellement sur le développement des moteurs électriques de ces véhicules et des technologies de batteries de recharge. Cependant, un des obstacles majeurs pour le déploiement des VEs à grande échelle réside dans l'incertitude d’assister et de guider les conducteurs de ce type de véhicule d’une façon appropriée pour atteindre les stations de recharge tout en satisfaisant leurs souhaits (points de recharge disponibles, moins d’attente possible, proposition d’autres points d’intérêts : restaurant, shopping, etc.). Afin de remédier à ce manque, nous proposons dans ce travail de thèse une approche distribuée et adaptative orientée modèles pour la gestion de l'énergie pour la recharge des VEs. Pour ce faire, nous nous somme focalisés sur la modélisation des processus de recharge en utilisant une approche formelle basée sur des outils de systèmes à événements discrets, à savoir l'algèbre (max, +) et les réseaux de Petri. Les modèles développés ont permis d’étudier, d’analyser et d’évaluer le comportement du système de recharge. De plus, une approche d'optimisation basée sur la programmation linéaire est proposée afin d’affecter et d’orienter d'une façon optimale les VEs vers les stations de recharge appropriées et ordonnancer leurs opérations de recharge. Afin de prédire le taux et la durée de recharge moyens des VEs compte tenu des dates d’arrivée des demandes de recharge et l'état de recharge de chaque véhicule, une approche dédiée basée sur une fonction prédictive est proposée. En utilisant cette approche, les opérations de recharge pourraient être planifiées en minimisant les temps d'attente des VEs au sein des stations de recharge et en assurant un taux de recharge acceptable pour chaque demande. Les résultats d’analyse et de simulations obtenus ont montré que les approches de modélisation, d’optimisation et de prédiction proposées permettent d’affecter de façon adéquate et optimale les VEs aux stations de recharge tout en satisfaisant toutes les contraintes du processus de recharge.