Depuis la fin des années 80, s'exprime dans le monde industriel la nécessité de nouvelles organisations et de réseaux d'entreprises plus propices à une meilleure productivité. Ces nouvelles structures qui sont supposées améliorer la performance industrielle demandent que soient analysées et maîtrisées les relations d'échange interentreprises. En effet, la conception des produits, leur fabrication et leur conditionnement, leur commercialisation et leur distribution sont le fait, non plus d'entreprises isolées et autarciques, mais de réseaux d'entreprises de plus en plus complexes, pouvant prendre de surcroît différentes formes. C'est dans ce contexte, que le concept d'Architecture Industrielle apparaît et se définit comme le regroupement d'entreprises dont les relations ont un caractère durable. Parmi ces différentes architectures, nous nous intéresserons ici à celles qui mettent en relation des donneurs d'ordres et des fournisseurs. À ces ensembles d'entreprises, regroupées autour d'un objectif désormais commun, correspond un besoin de coordination de l'ensemble des actions réparties chez les différents partenaires. Nous nous sommes intéressés dans nos travaux à une formalisation de la conduite entre entreprises basée sur les notions de prise de décision distribuée et de coopération, notions qui s'opposent à la structuration hiérarchisée encore récemment dominante dans de nombreux secteurs industriels. L'ensemble de ce mémoire s'organise en quatre chapitres. Dans une première partie, nous caractérisons l'aide à la décision et le pilotage distribué des flux interentreprises. Les deux chapitres suivants constituent le coeur de notre travail. Nous y présentons notre démarche qui se fonde sur une modélisation de l'Architecture Industrielle et sur une formalisation de la coopération par un ensemble de négociations bilatérales. Enfin, le dernier chapitre reprend l'ensemble de notre démarche à travers un exemple issu du monde industriel.

Le but de la thèse est de développer une nouvelle approche de surveillance des systèmes à événements discrets. La méthode proposée est basée sur la surveillance du temps de service en utilisant l'automate temporisé comme outil de modélisation.<br />Partant d'un système commandé, le premier objectif est la surveillance des différentes activités de ce système afin d'améliorer sa disponibilité. Ceci se traduit par la minimisation du nombre d'arrêts qui pénalisent la production, en suivant en temps réel, l'état de fonctionnement des différents capteurs du système. Ainsi pour chaque tâche, la surveillance du temps écoulé entre deux événements (l'instant où la commande a donné l'ordre de démarrer une tâche et l'instant où le capteur indique la fin d'exécution de la tâche) permet de détecter au plutôt d'éventuelles défaillances. La deuxième phase correspond au diagnostic qui consiste en la détermination des causes du problème observé.<br />Jusqu'à présent les approches de surveillance utilisent un modèle de référence basé sur la connaissance à priori de toutes les situations interdites du système. Le modèle de surveillance proposé présente un réel avantage. En effet, la détection d'éventuelles défaillances ne nécessite pas une liste exhaustive de toutes les défaillances possibles du système. En fonction de la catégorie du système de production et de la nature des tâches à surveiller nous introduisons une tolérance sur la durée de la tâche à surveiller. Ainsi, la notion de fonctionnement en ‘ mode dégradé' est introduite. Au-delà de cette tolérance, le système sera effectivement dans un état de ‘défaillance'. Différents exemples illustrent la démarche proposée. Ils permettent de montrer la puissance d'une telle approche. De plus, un algorithme permettant le calcul du seuil optimal de tolérance est proposé, ainsi que l'évaluation des performances du système de surveillance.

Cette thèse se situe dans le contexte des réseaux de communication temps-réel et son objectif est de proposer une architecture de communication pour la sous-couche MAC, qui définit des mécanismes pour assurer les contraintes temporelles du trafic temps-réel. Tout d'abord, une classification des protocoles MAC temps-réel existants, en mettant en exergue l'aspect ordonnancement de flux de messages ou ordonnancement de stations, est effectuée. En particulier, le protocole "jeton temporisé" et des mécanismes de la norme "ISA SP-50 / IEC-65C" sont détaillés. Ensuite, des contributions sur les mécanismes d'ordonnancement et les mécanismes protocolaires sont développées, à la fois en termes conceptuels et en termes de réflexions sur les normes existantes: proposition d'un algorithme non-préemptif ED avec, en particulier, une extension des conditions classiques d'ordonnançabilité; définition d'un algorithme de changement de mode de fonctionnement pour un système ordonnancé par l'algorithme RM; définition d'un protocole appelé "jeton temporisé régulier" qui améliore les performances temps-réel du protocole "jeton temporisé"; définition des conditions d'ordonnançabilité du trafic apériodique urgent dans le réseau FIP et proposition de deux profils de fonctionnement temps-réel pour le réseau Profibus. Enfin, nous proposons, modélisons avec le modèle "Réseaux de Petri Temporisés Stochastiques" et évaluons une architecture de communication pour la sous-couche MAC de réseaux locaux temps-réel. Cette architecture met en ¿uvre, de manière centralisée, un ordonnancement conjoint des trafics périodique et apériodique temps-réel, sur la base d'un algorithme non-préemptif pour le trafic périodique et d'une technique de jeton temporisé pour le trafic apériodique temps-réel. L'analyse permet, d'une part, d'évaluer l'ordonnancement en termes de taux d'utilisation permis et des limites de l'ordonnançabilité et, d'autre part, de montrer tout l'intérêt des modèles "Réseaux de Petri Temporisés Stochastiques" pour représenter et évaluer automatiquement l'ordonnançabilité d'un ensemble de configurations de flux de messages.

La complexité temporelle, logique et sémantique des systèmes multimédias et hypermédias rend nécessaire l'utilisation de techniques formelles permettant de spécifier ces systèmes et de vérifier, en préalable à leur conception, leurs propriétés logiques et temporelles. Cette thèse introduit une nouvelle technique de modélisation de systèmes multimédias et hypermédias basée sur le formalisme des réseaux de Pétri étendus par le temps. Ce modèle appelé Réseaux de Petri à Flux Temporels (RdPFT) permet de spécifier l'indéterminisme temporel intrinsèque aux systèmes distribués multimédias en associant un intervalle temporel aux arcs sortant des places d'un réseau de Petri. Les RdPFT introduisent de plus une sémantique formelle de la synchronisation en environnement faiblement synchrone. Cette sémantique formelle, définie à l'aide de 9 types de règles de tir pouvant être sélectivement associées aux transitions d'un RdPFT, permet de maîtriser l'indéterminisme de synchronisation introduit par la variabilité temporelle des traitements. Ainsi, les RdPFT permettent de modéliser de façon complète, précise et aisée les contraintes de synchronisation des systèmes multimédias. Cette thèse considère également la classe des RdPFT construits à l'aide des opérateurs de l'algèbre temporelle de Allen. Cette classe, appelée Réseaux de Petri Structurés à Flux Temporels (RdPSFT), permet une vérification aisée des propriétés temporelles d'un système multimédia et offre de plus des bases formelles pour la représentation abstraite des structures logiques et temporelles d'un système multimédia. Finalement cette thèse introduit une extension des RdPFT, appelée Réseaux de Petri Hiérarchisés à Flux Temporels (RdPHFT). Cette extension, bénéficiant de tous les acquis théoriques des RdPFT, permet de modéliser à l'aide d'un formalisme unificateur les composants d'un système hypermédia et introduit une sémantique formelle de la notion de synchronisatio n hypermédia. De plus les RdPHFT offrent un support méthodologique permettant une spécification modulaire et hiérarchisée des systèmes hypermédias, et plus généralement des systèmes "à contraintes temporelles"

Cette thèse propose un modèle formel et une méthodologie, permettant la conception formelle de documents hypermédias portables, qui couvre toutes les étapes essentielles du cycle de développement des documents hypermédias. Nous avons défini un modèle formel permettant la spécification et l'analyse des documents. L'implémentation est supportée par la traduction de la spécification analysée en une représentation physique interprétable par un système de présentation. Nous avons aussi développé des outils mettant en oeuvre cette méthodologie. Le modèle formel proposé est une extension du modèle Réseaux de Pétri Hiérarchiques à Flux Temporel (RdPHFT), qui permet une spécification formelle unifiée et précise de la synchronisation logique et temporelle des systèmes hypermédias distribués. Le modèle RdPHFT n'a pas pour objectif la description complète de documents hypermédias. Cette thèse propose une version interprétée du modèle RdPHFT, appelée RdPHFT-I, qui étend le modèle RdPHFT afin de permettre la spécification complète de documents hypermédias. A la suite et à l'aide du modèle RdPHFT-I, nous proposons une méthodologie de prototypage de documents hypermédias dans laquelle la spécification et l'analyse des documents sont faites à l'aide du modèle RdPHFT-I et l'implantation est supportée : soit par la production automatique de représentations MHEG, soit par la production d'applications Java. MHEG est une norme internationale de représentation des informations multimédias et hypermédias permettant le transfert de ces informations dans un système ouvert. Java est un langage de programmation d'applications multimédias fournissant un code portable de l'application. En résumé, la principale contribution de ce travail est d'avoir proposé et mis en oeuvre une méthodologie permettant de contrôler la qualité et de maîtriser la complexité des systèmes hypermédias, à partir d'un cycle de vie permettant de générer directement un docume nt hypermédia à partir d'une spécification formelle analysée.

Cette thèse traite l'étude de la fiabilité et de la durabilité des systèmes photovoltaïques (PV). Face à l'absence de retour d'expériences, réaliser une telle étude sous-entend, à la fois, de proposer des procédures expérimentales de qualification basées sur des essais accélérés conduits sur les composants critiques des systèmes PV, et de développer des outils de simulation de la fiabilité de l'assemblage de ces composants constituant un système considéré complexe. Ainsi dans un premier temps, nous nous sommes consacrés à l'étude de la fiabilité des modules PV. Une méthodologie originale basée sur les essais de dégradation accélérée nous a permis d'estimer la fiabilité de ces composants sous leurs deux modes prédominants de défaillance que sont la corrosion et la décoloration de l'encapsulant. L'originalité réside dans la prise en compte des variabilités des conditions environnementales et sur le couplage des essais accélérés et de dégradation. Un outil a été développé à cet effet. Dans un second temps, nous nous sommes placés à l'échelle des systèmes PV. Nous avons proposé de simuler certains paramètres caractérisant leur sûreté de fonctionnement en s'appuyant sur une représentation du système avec ces différents modes de fonctionnement et de dysfonctionnement (défaillances et dégradation) à l'aide de plusieurs Réseaux de Petri Stochastiques imbriqués sur plusieurs niveaux afin de se situer, pour chaque composant, aux échelles pour lesquelles les modes de défaillance pouvaient être saisis et formulés. Notre travail de thèse permet finalement de donner les bases méthodologiques et les outils de simulations pour qualifier et garantir la durée de vie de systèmes PV.

Thèse numérisée par la Division de la gestion de documents et des archives de l'Université de Montréal

La technologie de workflow, tendant à automatiser les processus d'entreprise et à fournir un support pour leur gestion, est aujourd'hui un secteur actif de recherche. C'est dans ce contexte que se situent ces travaux de thèse qui portent aussi bien sur la modélisation des processus workflow que sur leur vérification. Ces processus, pouvant être contraints par des ressources partagées ou encore par des durées de traitement, doivent être vérifiés avant d'être confiés aux systèmes de gestion de workflow qui vont les exécuter. Nous nous sommes intéressés par la vérification de la propriété de cohérence (soundness) des réseaux de workflow (WF-net) : sous-classes des réseaux de Petri (RdPs) modélisant les processus workflow.Dans ce cadre, en explorant la théorie structurelle des RdPs, nous avons identifié des sous-classes de WF-nets pour lesquelles la cohérence peut être vérifiée et caractérisée efficacement. Nous nous sommes focalisés en outre sur l'extension de ces sous-classes en tenant compte de la présence de ressources partagées et sur la propriété de cohérence en présence d'un nombre arbitraire d'instances prêtes à s'exécuter. Dans cette partie, nous avons dû automatiser le calcul des siphons minimaux dans un RdP. Pour ce faire, nous avons choisi un algorithme de la littérature et l'amélioré par la recherche et la contraction de circuits alternés.Ensuite, nous avons abordé la modélisation et la vérification de processus workflow tenant compte des contraintes temporelles. Nous avons en premier lieu proposé un modèle de TWF-net (WF-net Temporisé). Pour ce modèle, nous avons défini la propriété de cohérence temporelle et proposé une condition nécessaire et suffisante pour la vérifier. En deuxième lieu, nous avons relaxé les contraintes temporelles adoptées par la proposition d'un modèle temporel visant des processus à contraintes temporelles variant dans des intervalles de temps. Nous avons défini formellement le modèle de ITWF-net (Interval Timed WF-net) et donné sa sémantique. Par ailleurs, nous avons développé et testé un prototype de modélisation et de simulation des ITWF-nets.La dernière partie de cette thèse a concerné la vérification formelle des processus workflow par SPIN model checker. Nous avons dû en premier lieu traduire la spécification des workflows adoptée vers Promela : le langage de description des modèles à vérifier par SPIN. En second lieu, nous avons exprimé les propriétés de cohérence en Logique Linéaire Temporelle (LTL) et utilisé SPIN pour tester si chaque propriété est satisfaite par le modèle Promela du WF-net en question. Enfin, nous avons exprimé les propriétés de k-cohérence pour les WF-nets modélisant plusieurs instances et de (k,R)-cohérence pour les processus workflow concurrents et qui possèdent des ressources partagées.

Les systèmes actuels deviennent chaque jour de plus en plus complexe; à la distribution s’ajoutent les contraintes temps réel. Les méthodes classiques en charge de garantir la sûreté de fonctionnement, comme le test, l’injection de fautes ou les méthodes formelles ne sont plus suffisantes à elles seules. Afin de pouvoir traiter les éventuelles erreurs lors de leur apparition dans un système distribué donné, nous désirons mettre en place un programme, surveillant ce système, capable de lancer une alerte lorsque ce dernier s’éloigne de ses spécifications ; un tel programme est appelé superviseur (ou moniteur). Le fonctionnement d’un superviseur consiste simplement à interpréter un ensemble d’informations provenant du système sous forme de message, que l’on qualifiera d’évènement, et d’en déduire un diagnostic. L’objectif de cette thèse est de mettre un place un superviseur distribué permettant de vérifier en temps réel des propriétés temporelles. En particulier nous souhaitons que notre moniteur soit capable de vérifier un maximum de propriétés avec un minimum d’information. Ainsi notre outil est spécialement conçu pour fonctionner parfaitement même si l’observation est imparfaite, c’est-à-dire, même si certains évènements arrivent en retard ou s’ils ne sont jamais reçus. Nous avons de plus cherché à atteindre cet objectif de manière distribuée pour des raisons évidentes de performance et de tolérance aux fautes. Nous avons ainsi proposé un protocole distribuable fondé sur l’exécution répartie d’un réseau de Petri temporisé. Pour vérifier la faisabilité et l’efficacité de notre approche, nous avons mis en place une implémentation appelée Minotor qui s’est révélée avoir de très bonnes performances. Enfin, pour montrer l’expressivité du formalisme utilisé pour exprimer les spécifications que l’on désire vérifier, nous avons détaillé un ensemble de propriétés sous forme de réseaux de Petri à double sémantique introduite dans cette thèse (l’ensemble des transitions étant partitionné en deux catégories de transitions, chacune de ces parties ayant sa propre sémantique). / Current systems are becoming every day more and more complex, being both distributed and real-timed. Conventional methods responsible for guaranteeing dependability, such as testing, fault injection or formal methods are no longer sufficient. In order to process any errors when they appear in a given distributed system, we want to implement a software monitoring it and capable of launching an alert when the system does not respect anymore its specification. Such a program is called monitor. A monitor interpret information received from the system as messages (these messages are called events) and propose a diagnosis. The objective of this thesis is to set in place a monitor for a distributed real-time verification of temporal properties. In particular we want our monitor to be able to check up a maximum of properties with a minimum of information. Thus, our tools are designed to work perfectly even if the observation is imperfect, that is to say, even if some events are late or never received. We have also managed to achieve this goal through a highly distributed protocol. To verify the feasibility and effectiveness of our approach, we have established an implementation called Minotor who was found to have very good performance. Finally, we detailed a set of properties, expressed in our formalism, to show it’s expressiveness.

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.