Cette thèse s'inscrit dans le cadre de la théorie des systèmes linéaires dans les dioïdes. Cette théorie concerne la sous-classe des systèmes à événements discrets modélisables par les Graphes d'Événements Temporisés (GET). La dynamique de ces graphes peut être représentée par des équations récurrentes linéaires sur des structures algébriques particulières telles que l'algèbre (max,+) ou l'algèbre (min,+).Ce mémoire est consacré à l'analyse de performances des systèmes dynamiques qui peuvent être modélisés graphiquement par des Graphes d'Événements Temporisés Généralisés (GETG). Ces derniers, contrairement au GET, n'admettent pas une représentation linéaire dans l'algèbre (min,+). Pour pallier à ce problème de non linéarité, nous avons utilisé une approche de modélisation définie sur un dioïde d'opérateurs muni de deux lois internes : loi additive correspondant à l'opération (min), et loi multiplicative équivalente à la loi de composition usuelle. Le modèle d'état obtenu, est utilisé pour évaluer les performances des GETG. Pour cela, nous avons proposé une nouvelle méthode qui a pour but de linéariser le modèle mathématique régissant l'évolution dynamique du modèle graphique, dans le but d'obtenir un modèle (min,+) linéaire. La deuxième partie de cette thèse est consacrée au problème qui consiste à déterminer les ressources à utiliser dans une ligne de production, en vue d'atteindre des performances souhaitée. Ceci est équivalent à déterminer le marquage initial de la partie commande du GETG.

Si l'utilisation de voix et vidéo sur ip fonctionne correctement sur un réseau WiFi avec un seul point d'accès, les performances en terme de qualité de service sont altérées sur un réseau WiFi maillé où chaque point d'accès sert de relais aux suivants. En effet, le partage d'un même canal radio sur de grandes surfaces par plusieurs noeuds qui ne se captent pas toujours permet difficilement d'établir des communications nécessitant de la qualité de service. La difficulté d'une analyse par expérimentation, due à la difficulté d'observation des communications, a orienté l'étude vers la simulation. En l'absence de simulateurs existants adéquats au vu d'un réseau maillé qui est un concept récent, l'objet de cette thèse est la création, l'étude et l'exploitation d'un simulateur, basé sur des réseaux de Petri, permettant la simulation de communications sur un réseau maillé WiFi. Les améliorations apportées par cette étude ont pour but d'être implémentées sur un matériel existant afin d'offrir un service de transport de voix et de vidéo sur un réseau WiFi maillé. Les premières simulations réalisées à l'aide de cet outil ont fait apparaître des pertes de paquets et des altérations de la gigue due à l'état des files d'attente d'émission de certains noeuds. Après avoir identifié des leviers accessibles sur le matériel existant sur lequel peuvent être effectivement apportées des améliorations tout en restant dans le cadre de la norme, une approche automatique et réseaux a mis en évidence des stratégies d'améliorations possibles de la qualité de service nécessaire pour des communications audio et vidéo.

Cette thèse cherche à résoudre en pratique le problème de couverture dans les réseaux de Petri et les systèmes de canaux à pertes (LCS). Ces systèmes sont intéressants à étudier car ils permettent de modéliser facilement les systèmes concurrents et les systèmes distribués. Le problème de couverture dans un système de transitions consiste à savoir si on peut, à partir d’un état initial arriver à un état plus grand qu’un état cible. La résolution de ce problème dans les systèmes de transitions bien structurés (WSTS) sera le sujet d’études de la première partie. Les réseaux de Petri et les LCS sont des WSTS. On donnera dans la première partie une méthode générale pour le résoudre rapidement en pratique. Cette méthode utilise des invariants de couverture, qui sont des sur-approximations de l’ensemble des états couvrables. La seconde partie sera consacrée aux réseaux de Petri. Elle présentera diverses comparaisons théoriques et pratiques de différents invariants de couverture. Nous nous intéresserons notamment à la combinaison de l’invariant classique de l’inéquation d’état avec une analyse de signe simple. Les LCS seront le sujet d’études de la troisième partie. On présentera une variante de l’inéquation d’état adaptée aux LCS ainsi que deux invariants qui retiennent des propriétés sur l’ordre dans lequel les messages sont envoyés. La thèse a mené à la création de deux outils, ICover et BML, pour résoudre le problème de couverture respectivement dans les réseaux de Petri et dans les LCS. / The goal of this thesis is to solve in practice the coverability problem in Petri nets and lossy channel systems (LCS). These systems are interesting to study because they can be used to model concurrent and distributed systems. The coverability problem in a transition system is to decide whether it is possible, from an initial state, to reach a greater state than a target state. In the first part, we discuss how to solve this problem for well-structured transition systems (WSTS). Petri nets and LCS are WSTS. In the first part, we present a general method to solve this problem quickly in practice. This method uses coverability invariants, which are over-approximations of the set of coverable states. The second part studies Petri nets.We present comparisons of coverability invariants, both in theory and in practice. A particular attention will be paid on the combination of the classical state inequation and a simple sign analysis. LCS are the focus of the third part. We present a variant of the state inequation for LCS and two invariants that compute properties for the order in which messages are sent. Two tools, ICover and BML, were developed to solve the coverability problem in Petri nets and LCS respectively.

L'identification des interactions survenant au niveau moléculaire joue un rôle crucial pour la compréhension du vivant. L'objectif de ce travail a consisté à développer des méthodes permettant de modéliser et de prédire ces interactions pour le métabolisme et la régulation de la transcription. Nous nous sommes basés pour cela sur la modélisation de ces systèmes sous la forme de graphes et d'automates. Nous avons dans un premier temps développé une méthode permettant de tester et de prédire la distribution du flux au sein d'un réseau métabolique en permettant la formulation d'une à plusieurs contraintes. Nous montrons que la prise en compte des données biologiques par cette méthode permet de mieux reproduire certains phénotypes observés in vivo pour notre modèle d'étude du métabolisme énergétique du parasite Trypanosoma brucei. Les résultats obtenus ont ainsi permis de fournir des éléments d'explication pour comprendre la flexibilité du flux de ce métabolisme, qui étaient cohérentes avec les données expérimentales. Dans un second temps, nous nous sommes intéressés à une catégorie particulière d'ARN non codants appelés sRNAs, qui sont impliqués dans la régulation de la réponse cellulaire aux variations environnementales. Nous avons développé une approche permettant de mieux prédire les interactions qu'ils effectuent avec d'autres ARN en nous basant sur une prédiction des interactions, une analyse par enrichissement du contexte biologique de ces cibles, et en développant un système de visualisation spécialement adapté à la manipulation de ces données. Nous avons appliqué notre méthode pour l'étude des sRNAs de la bactérie Escherichia coli. Les prédictions réalisées sont apparues être en accord avec les données expérimentales disponibles, et ont permis de proposer plusieurs nouvelles cibles candidates. / The identification of the interactions occurring at the molecular level is crucial to understand the life process. The aim of this work was to develop methods to model and to predict these interactions for the metabolism and the regulation of transcription. We modeled these systems by graphs and automata.Firstly, we developed a method to test and to predict the flux distribution in a metabolic network, which consider the formulation of several constraints. We showed that this method can better mimic the in vivo phenotype of the energy metabolism of the parasite Trypanosoma brucei. The results enabled to provide a good explanation of the metabolic flux flexibility, which were consistent with the experimental data. Secondly, we have considered a particular class of non-coding RNAs called sRNAs, which are involved in the regulation of the cellular response to environmental changes. We developed an approach to better predict their interactions with other RNAs based on the interaction prediction, an enrichment analysis, and by developing a visualization system adapted to the manipulation of these data. We applied our method to the study of the sRNAs interactions within the bacteria Escherichia coli. The predictions were in agreement with the available experimental data, and helped to propose several new target candidates.

Lintégration progressive de lélectronique dans les secteurs automobile et avionique a amélioré le confort et les services rendus. Toutefois, cela a complexifié la conception des systèmes pilotés par calculateurs (systèmes mécatroniques, calculateurs de vol, etc.), ce qui rend difficile la maîtrise de leur fiabilité. Par ailleurs, la phase de conception doit être rapide et peu coûteuse (le moins de prototypes possible, le plus tard possible) avec un niveau de sécurité garantie. De plus, les ressources en moyens matériels étant limitées, pour des raisons de coûts et de mise en Suvre, les concepteurs évitent au maximum les redondances matérielles. Des études de Sûreté de Fonctionnement réalisées dès la phase de conception permettent une meilleure maîtrise des risques et de la fiabilité des systèmes conçus. En effet, les points faibles qui sont mis en évidence lors de lévaluation du niveau de sûreté des systèmes conçus permettent aux concepteurs de spécifier des stratégies de pilotage et des modes de reconfiguration avant les premiers essais sur un prototype réel. Les systèmes pilotés par calculateurs combinant des technologies mécaniques, hydrauliques, électroniques et informatiques sont hybrides: la dynamique continue est associée à la partie énergétique et la dynamique discrète est liée à la commande numérique et à lexistence dévénements discrets (défaillances, dépassements de seuils). Létude de la sûreté de fonctionnement de tels systèmes doit nécessairement tenir compte des interactions existantes entre leurs paramètres physiques (température, pression, vitesse&) et le dysfonctionnement de leurs composants. Les méthodes classiques de la sûreté de fonctionnement, comme les arbres de défaillances sont insuffisantes pour de tels systèmes complexes et hybrides car ils sont dynamiques. La sûreté de ces systèmes doit tenir compte du temps et de lordre dapparition des événements. La rareté de ces scénarios expose les méthodes basées seulement sur la simulation. au problème dexplosion combinatoire. Il existe en effet des techniques daccélération de la simulation, largement utilisées avec succès, dans lingénierie nucléaire notamment. Mes travaux de thèse sont placés dans le cadre de la fiabilité dynamique. Lobjectif est de réaliser une analyse qualitative de la sûreté de fonctionnement des systèmes pilotés par calculateurs pour extraire des scénarios menant à des états redoutés. Il sagit de caractériser ces scénarios au plus tôt dans la phase de conception, ce qui permet dévaluer leurs probabilités doccurrence pour valider larchitecture du système. Nous proposons une approche basée sur la logique linéaire et les Réseaux de Petri Prédicats Transitions Différentiels Stochastiques (RdP PTDS) qui garantissent le respect de la nature hybride de ces systèmes. Cette approche tient partiellement compte de laspect continu du système et plus particulièrement des seuils associés à certaines transitions dans le modèle RdP. Cela permet de déterminer plus précisément les conditions exactes de loccurrence de lévénement redouté : ce qui pousse le système à quitter son fonctionnement normal et à évoluer vers létat redouté. Loriginalité de notre approche est que lordre doccurrence des événements est pris en compte et les scénarios incohérents vis-à-vis de la dynamique continue du système sont éliminés. Notre approche est également orientée vers la vérification de certaines propriétés des systèmes pilotés par calculateur. Ces propriétés peuvent êtres de type temporel (la durée maximale dun scénario ou la durée entre deux commandes) ou de type accessibilité entre deux états. Lautomatisation de toutes les étapes de notre approche nous a paru indispensable dans le cas des systèmes complexes où le risque derreur humaine est très important. C'est pourquoi, j développé un outil ESA_PetriNet (Extraction & Scenarios Analyser by PetriNet model) qui permet dextraire les scénarios critiques qui mènent vers létat redouté à partir du n modèle Réseau de Petri temporel et de vérifier certaines propriétés des systèmes pilotés par calculateurs. null

Les travaux proposés dans cette thèse s'intéressent à la commande et la surveillance d'une classe particulière de systèmes de production : les systèmes manufacturiers à contraintes de temps de séjour. Nous supposons dans l'étude que les ressources ont déjà été affectées et que l'ordre des opérations est déjà fixé par le module de planification/ordonnancement. Les hypothèses de fonctionnement répétitif avec et sans postes d'assemblage sont adoptées. De manière assez classique pour ce type de problématique, le formalisme utilisé est celui des Réseaux de Petri P-temporels pour l'étude des instants de débuts et de fins des opérations.Une étude de la robustesse des ateliers manufacturiers à contraintes de temps a été développée. La robustesse est abordée avec et sans modification de la commande relative à la robustesse active et à la robustesse passive respectivement, face aux perturbations temporelles. Un algorithme de calcul d'une borne supérieure de la robustesse passive est présenté. De plus, trois stratégies de commande robuste face aux perturbations temporelles ont été développées.Par ailleurs, l'incertitude dans les systèmes de production manufacturière à été étudié. Notre contribution dans ce cadre porte sur l'intégration des résultats concernant la robustesse dans la génération de symptômes et la classification des comptes rendus associés aux différentes opérations en utilisant la logique floue.Partant d'un système commandé, nous avons présenté en détail une démarche à suivre pour la mise en œuvre d'un modèle de surveillance en se basant sur les chroniques et les arbres de défaillance flous. Cette démarche est appliquée à un atelier de production laitière

Les travaux présentés dans cette thèse constituent une contribution à la modélisation, à l'analyse et à la commande des systèmes de transport public par l'adaptation des réseaux de Petri (RdP) et algèbre des dioïdes. Nous étudions en particulier la gestion optimisée des correspondances par une planification des horaires d'un réseau de transport en commun. Nous développons dans ce sens des modèles capables d'apporter des solutions aux problèmes d'amélioration de la qualité de service de transport en commun, par les minimisations des temps de correspondance et des ressources matérielles utilisées. Notre travail est effectué en considérant deux études de cas de fonctionnement des bus au niveau des arrêts de correspondance où des échanges de passagers sont susceptibles de se produire. Un fonctionnement synchronisé pour lequel nous utilisons un modèle graphe d'événements temporisés (GET) et un modèle (max, +) linéaire stationnaire qui lui est associé. Un fonctionnement non-synchronisé modélisé par un graphe d'événements temporisés avec retrait dynamique de jetons (GETRDJ). Ce dernier modèle graphique, possédant des conflits structurels, a une description analytique dans l'algèbre (max, +) de forme linéaire non-stationnaire. La résolution mathématique du modèle obtenu passe par une politique de résolution des conflits associés au modèle graphique. Nous proposons dans ce sens une politique de routage déterminée a priori prenant en compte les caractéristiques du système. Cette politique permet d'une part, d'arbitrer les conflits sur le modèle graphique, et d'autre part, de résoudre le modèle mathématique. L'analyse des solutions obtenues ainsi que les éléments propres de la matrice caractéristique du modèle (max, +) permet de déterminer les différents temps de correspondance des voyageurs et d'estimer ainsi les performances du système étudié. Dans le souci de minimiser les temps de correspondance des voyageurs et améliorer la qualité de service, nous proposons une politique de commande de ces réseaux de bus. Deux approches sont alors proposées. La première permet de synthétiser une commande basée sur les techniques développées dans le cadre de la théorie de la résiduation dans les dioïdes. La seconde est fondée sur des résultats de simulation qui permettent d'obtenir une commande à partir des optima globaux des fonctions objectifs. Les résultats obtenus sont validés sur une partie du réseau de transport en commun de la ville de Montbéliard.

Les travaux présentés dans ce mémoire ont pour cadre la recherche de nouveaux services et protocoles de Transport, aptes à supporter le transfert de données multimédia en tenant compte des exigences applicatives en termes de hauts débits et de synchronisation. L'approche proposée repose sur la définition et le développement d'un nouveau concept: la connexion d'ordre partiel (POC - Partial Order Connection), établissant un lien conceptuel entre les modes de service/protocole orientés-connexion tels que TCP, et sans connexion tels que UDP. Une POC est une connexion de bout en bout permettant de définir et de mettre en œuvre tous les services et protocoles d'ordre partiel entre deux entités communicantes ; dans une POC, la délivrance des données à l'utilisateur récepteur peut être effectuée dans un ordre différent de l'ordre de soumission de ces données par l'utilisateur émetteur: la différence (acceptable) entre ces deux ordres résulte de la définition, par l'utilisateur, d'un ordre partiel de délivrance lors de l'ouverture de la connexion. Une formalisation des mécanismes correspondants est proposée au moyen de la technique de description formelle Estelle. Les caractéristiques intrinsèques des différents média d'un flux multimédia ont conduit ces dernières années au développement d'architectures de communication intégrant la prise en compte des contraintes applicatives à différents niveaux conceptuels, et notamment au niveau Transport du modèle OSI ; à partir d'une modélisation de ces contraintes utilisant le formalisme des réseaux de Petri (le modèle TSPN), l'auteur propose d'intégrer le concept de POC dans une architecture de Transport multimédia autorisant une prise en compte globale des contraintes d'ordre et de fiabilité d'un flux multimédia. Les mécanismes de gestion de l'ordre et de la fiabilité qui sont proposés permettent de définir un service de Transport multimédia offrant une hypothèse nouvelle aux utilisateurs vis à vis de la problématique de la synchronisation. Une étude de la faisabilité d'un protocole multimédia d'ordre partiel à l'aide des procédures XTP est finalement présentée: elle conclut en la possibilité d'une telle réalisation

Le travail proposé dans cette thèse s'intéresse aux ateliers manufacturiers à contraintes de temps de séjour. Nous supposons dans l'étude que les ressources ont déjà été affectées et que l'ordre des opérations est déjà fixé par le module de planification/ordonnancement. Les hypothèses de fonctionnement répétitif et d'absence de postes d'assemblage sont adoptées. De manière assez classique pour ce type de problématique, le formalisme utilisé est celui des Réseaux de Petri P-temporels pour l'étude des instants de débuts et de fins des opérations.<br /> <br />Une axiomatique rigoureuse a été développée pour la caractérisation analytique de propriétés de commandabilité. Plus précisément, la robustesse est abordée avec et sans modification de la commande relative à la robustesse active et à la robustesse passive respectivement, face aux perturbations temporelles. Un algorithme de calcul d'une borne inférieure de la robustesse passive est présenté. De plus, une condition suffisante pour l'existence de la robustesse active a été fournie.<br />Par ailleurs, l'observabilité de ces variations a été étudiée et particulièrement leur localisation. Dans une logique de surveillance de la qualité du produit, des résultats sur la détection et la localisation de violation de contraintes sont présentés.<br /><br />La situation de nos travaux, vis-à-vis d'une architecture générale de conduite d'atelier, s'est concrétisée par une proposition d'intégration de la connaissance analytique de la robustesse dans le filtrage des comptes rendus associés aux opérations. Cette contribution au niveau du module de surveillance/supervision constitue un des apports de la robustesse à envisager.

Cette thèse propose une méthode de détection et diagnostic basée cohérence pour les systèmes à événements discrets. La méthode prend en compte la possibilité d'erreurs dans les modèles utilisés comme référence du bon comportement du système. La détection est réalisée par la vérification de cohérence entre le comportement observé et le comportement décrit par les modèles du système. Dans la mesure où les modèles utilisés ne sont pas exempts d'erreurs, la perte de cohérence détectée peut correspondre à une réelle défaillance au niveau du procédé ou à une erreur dans les modèles. Pour distinguer ces deux cas, il est nécessaire de déterminer les sous-modèles communs. Chaque observation émanant du procédé apporte une information utile pour l'identification de la ou des types de configuration entre les modèles. L'identification est réalisée en ligne et repose sur le parcours d'un graphe décrivant exhaustivement l'ensemble des configurations des modèles. Enfin, le rétablissement de la cohérence avec les observations par modification des modèles constitue le principe du diagnostic