Au cours des dernières décennies, la complexité croissante des systèmes de production et de leur commande a rendu crucial le besoin d’utiliser les méthodes formelles pour faire face aux problèmes relatifs au contrôle, à la fiabilité, au diagnostic des fautes et à l’utilisation optimale des ressources dans les installations de production. Cela concerne en particulier les systèmes automatisés de production (SAP), caractérisés par des cycles technologiques complexes qui doivent s’adapter à des conditions changeantes. Les SAP modernes sont des sous-systèmes interconnectés tels que des machines à commande numérique, des stations d'assemblage , des véhicules guidés automatisés (AGV), des cellules robotisées, des convoyeurs et des systèmes de contrôle par ordinateur. Les fabricants utilisent des machines automatisées et des contrôleurs pour assurer des produits de qualité plus rapidement et plus efficacement. Aussi, ces systèmes automatisés peuvent fournir des informations essentielles pour aider les gestionnaires à prendre les bonnes décisions. Cependant, en raison de la grande flexibilité des SAP, des défaillances telles qu’un mauvais assemblage ou le dépôt d’une pièce dans un tampon inapproprié peuvent se produire lors du fonctionnement du système. De tels dysfonctionnements diminuent la productivité du système générant ainsi des pertes économiques et des effets perturbateurs sur le système. En conséquence, le problème de l’optimisation des performances des SAP est impératif.Cette thèse se focalise sur l’évaluation et l’optimisation des performances des systèmes de production automatisés via le modèle des réseaux de Pétri temporisés. / In the last decades, there has been a constant increase in the awareness of company management about the importance of formal techniques in industrial settings to address problems related to monitoring and reliability, fault diagnosis, and optimal use of resources, during the management of plants. Of particular relevance in this setting are the so-called Automated Manufacturing Systems (AMSs), which are characterized by complex technological cycles that must adapt to changing demands. Modern AMSs are interconnected subsystems such as numerically controlled machines, assembly stations, automated guided vehicles, robots, conveyors and computer control systems. Manufacturers are using automated machines and controls to produce quality products faster and more efficiently. Meanwhile, these automated systems can provide critical information to help managers make good business decisions. However, due to the high flexibility of AMSs, failures such as a wrong assembly or a part put in a wrong buffer may happen during the operation of the system. Such failures may decrease the productivity of the system which has an economical consequence and can cause a series of disturbing issues. As a result, the performance optimization in AMSs are imperative. This thesis focuses on the performance evaluation and performance optimization of automated manufacturing systems using timed Petri nets models.

Sistemas de controle de edifícios inteligentes têm evoluído consideravelmente e a sua confiabilidade também tem melhorado. Mesmo assim, falhas são inevitáveis em sistemas concebidos, construídos e operados pelo homem e uma abordagem alternativa envolve a minimização das conseqüências das falhas. Isto é possível através da reconfiguração do sistema que se faz realocando funções de controle e escolhendo outras formas de interação entre os processos. Apesar disso, na literatura ainda não existe muito material que trate da modelagem de processos em que desde a sua concepção as falhas são consideradas. Assim, propõe-se neste trabalho o desenvolvimento de um procedimento para a modelagem de sistemas de controle considerando além das especificações funcionais, em situação normal, a ocorrência de falhas. Em função da base teórica existente e ferramentas disponíveis a abordagem proposta adota o conceito de sistemas a eventos discretos, holon e a técnica de rede de Petri e suas extensões para descrever a estrutura e o funcionamento deste sistema de controle. Um exemplo de aplicação é aqui apresentado para ilustrar as principais características deste procedimento. / Control systems of intelligent buildings have evolved and its reliability has evidently improved. However, faults are inevitable in systems conceived, constructed and operated by humans and an alternative approach is the minimization of the faults consequences. This is possible through the reconfiguration of the system, i.e., re-allocating control functions and choosing other forms of interaction between the processes. Despite this, there are few publications that deal with the modeling of processes where since its conception the faults are considered. Thus, this work proposes the development of a procedure for the modeling of control systems considering beyond the functional specifications in normal situation, the occurrence of faults. Based on the existing theoretical base and available tools the proposal adopts the concept of discrete event system, holon and Petri net technique with its extensions to describe the structure and the operation of these control systems. An application example is here presented to illustrate the principal characteristics of this proceeding.

Le développement et l’application des langages formels sont un défi à long terme pour la science informatique. Un enjeu particulier est l’acceptation par l’industrie. Cette thèse présente une approche pour la modélisation et la vérification des postes d’aiguillage français. La première question est la modélisation du système d’enclenchement par les réseaux de Petri colorés (RdPC). Un cadre de modélisation générique et compact est introduit, dans lequel les règles d’enclenchement sont modélisées dans une structure hiérarchique, tandis que les installations sont modélisées dans une perspective géographique. Ensuite, un patron de modèle est présenté. C’est un modèle paramétré qui intègre les règles nationales françaises qui peut être appliquée pour différentes gares. Puis, un concept basé sur l’événement est présenté dans le processus de modélisation des parties basses des postes d’aiguillage. La deuxième question est la transformation des RdPCs en machines B, qui va aider les concepteurs sur la route de l’analyse à application. Tout d’abord, une méthodologie détaillée, s’appuyant sur une table de correspondance, du RdPCs non-hiérarchiques vers les notations B est présentée. Ensuite, la hiérarchie et la priorité des transitions du RdPC sont successivement intégrées dans le processus de mapping, afin d’enrichir les possibilités de types de modèles en entrées de la transformation. Les machines B produites par la transformation permettent la preuve automatique intégrale par l’Atelier B. L’ensemble de ces travaux, chacun à leur niveau, contribuent à renforcer l’efficacité d’un cadre global d’analyse sécuritaire / Development and application of formal languages are a long-standing challenge within the computer science domain. One particular challenge is the acceptance of industry. This thesis presents some model-based methodologies for modelling and verification of the French railway interlocking systems (RIS). The first issue is the modellization of interlocking system by coloured Petri nets (CPNs). A generic and compact modelling framework is introduced, in which the interlocking rules are modelled in a hierarchical structure while the railway layout is modelled in a geographical perspective. Then, a modelling pattern is presented, which is a parameterized model respecting the French national rules. It is a reusable solution that can be applied in different stations. Then, an event-based concept is brought into the modelling process of low-level part of RIS to better describe internal interactions of relay-based logic. The second issue is the transformation of coloured Petri nets into B machines, which can help designers on the way from analysis to implementation. Firstly, a detailed mapping methodology from non-hierarchical CPNs to abstract B machine notations is presented. Then the hierarchy and the transition priority of CPNs are successively integrated into the mapping process, in order to enrich the adaptability of the transformation. This transformation is compatible with various types of colour sets and the transformed B machines can be automatically proved by Atelier B. All these works at different levels contribute towards a global safe analysis framework

Submitted by Erika Demachki (erikademachki@gmail.com) on 2016-10-17T18:54:20Z No. of bitstreams: 2 Dissertação - Luciano Eduardo Braga dos Santos - 2016.pdf: 4527753 bytes, checksum: 8db193f1cca4949ecdcfe2e93d9399f2 (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) / Approved for entry into archive by Erika Demachki (erikademachki@gmail.com) on 2016-10-18T17:16:29Z (GMT) No. of bitstreams: 2 Dissertação - Luciano Eduardo Braga dos Santos - 2016.pdf: 4527753 bytes, checksum: 8db193f1cca4949ecdcfe2e93d9399f2 (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) / Made available in DSpace on 2016-10-18T17:16:29Z (GMT). No. of bitstreams: 2 Dissertação - Luciano Eduardo Braga dos Santos - 2016.pdf: 4527753 bytes, checksum: 8db193f1cca4949ecdcfe2e93d9399f2 (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Previous issue date: 2016-06-17 / Fundação de Amparo à Pesquisa do Estado de Goiás - FAPEG / This work prop oses numerical metho d of simulation and optimization of waiting time in queues in hospital emergency. The case study is carried out in private hospital in the city of Goiania, Goias/Brazil. It is used to mo del discrete event systems as computational simulator and two optimization heuristics: the Brute Force algorithm and Genetic Algorithm. The optimization results are compared with the directives found in Resolution CFM 2077/2014, in an attempt to adapt the system to this resolution. With the results, it is observed that the simulation metho d and optimization metho ds are efficient to minimize queues at hospital emergency system. / Este trabalho prop˜oe m´eto do num´erico de simula¸c˜ao e otimiza¸c˜ao do temp o de esp era nas filas da emergˆencia hospitalar. O estudo de caso ´e realizado em hospital da rede particular, do munic´ıpio de Goiˆania. Utiliza-se a mo delagem de sistemas a eventos discretos como simulador computacional e dois m´eto dos heur´ısticos de otimiza¸c˜ao: o Algoritmo de For¸ca Bruta e o Algoritmo Gen´etico. Os resultados da otimiza¸c˜ao s˜ao comparados com as diretivas encontradas na Resolu¸c˜ao CFM no 2077/2014, na tentativa de adequar o sistema a esta resolu¸c˜ao. De posse dos resultados obtidos, observa-se que o m´etodo de simula¸c˜ao e os m´etodos de otimiza¸c˜ao s˜ao eficientes para minimiza¸c˜ao de filas em sistema de emergˆencia hospitalar.

Cette thèse s'intéresse à l'étude des problèmes de diagnostic des fautes sur les systèmes à événements discrets en utilisant les modèles réseau de Petri. Des techniques d'exploration incrémentale et à-la-volée sont développées pour combattre le problème de l'explosion de l'état lors de l'analyse de la diagnosticabilité. Dans le contexte atemporel, la diagnosticabilité de modèles RdP-L est abordée par l'analyse d'une série de problèmes K-diagnosticabilité. L'analyse de la diagnosticabilité est effectuée sur la base de deux modèles nommés respectivement FM-graph et FM-set tree qui sont développés à-la-volée. Un diagnostiqueur peut être dérivé à partir du FM-set tree pour le diagnostic en ligne. Dans le contexte temporel, les techniques de fractionnement des intervalles de temps sont élaborées pour développer représentation de l'espace d'état des RdP-LT pour laquelle des techniques d'analyse de la diagnosticabilité peuvent être utilisées. Sur cette base, les conditions nécessaires et suffisantes pour la diagnosticabilité de RdP-LT ont été déterminées. En pratique, l'analyse de la diagnosticabilité est effectuée sur la base de la construction à-la-volée d'une structure nommée ASG et qui contient des informations relatives à l'occurrence de fautes. D'une manière générale, l'analyse effectuée sur la base des techniques à-la-volée et incrémentale permet de construire et explorer seulement une partie de l'espace d'état, même lorsque le système est diagnosticable. Les résultats des simulations effectuées sur certains benchmarks montrent l'efficacité de ces techniques en termes de temps et de mémoire par rapport aux approches traditionnelles basées sur l'énumération des états / This PhD thesis deals with fault diagnosis of discrete event systems using Petri net models. Some on-the-fly and incremental techniques are developed to reduce the state explosion problem while analyzing diagnosability. In the untimed context, an algebraic representation for labeled Petri nets (LPNs) is developed for featuring system behavior. The diagnosability of LPN models is tackled by analyzing a series of K-diagnosability problems. Two models called respectively FM-graph and FM-set tree are developed and built on the fly to record the necessary information for diagnosability analysis. Finally, a diagnoser is derived from the FM-set tree for online diagnosis. In the timed context, time interval splitting techniques are developed in order to make it possible to generate a state representation of labeled time Petri net (LTPN) models, for which techniques from the untimed context can be used to analyze diagnosability. Based on this, necessary and sufficient conditions for the diagnosability of LTPN models are determined. Moreover, we provide the solution for the minimum delay ∆ that ensures diagnosability. From a practical point of view, diagnosability analysis is performed on the basis of on-the-fly building of a structure that we call ASG and which holds fault information about the LTPN states. Generally, using on-the-fly analysis and incremental technique makes it possible to build and investigate only a part of the state space, even in the case when the system is diagnosable. Simulation results obtained on some chosen benchmarks show the efficiency in terms of time and memory compared with the traditional approaches using state enumeration

Le projet de recherche présenté dans cette thèse a été réalisé avec la collaboration de la Direction de l'Ingénierie SNCF et le CReSTIC de l'Université de Reims Champagne-Ardenne (URCA). L'objectif de ce projet est de contribuer à l'amélioration des études de conception du contrôle/commande des projets d'électrification menées par les chargés d'études. Ce projet doit répondre à des objectifs humains, économiques et techniques exprimés par la SNCF, notamment appliqué au domaine des Equipements d'Alimentation des Lignes Electrifiées (EALE). Pour répondre à ces problématiques, une méthodologie pour les études d'automatisation est proposée. Elle intègre deux axes de recherche. Le premier axe est la génération automatique de livrables (codes, documents, schémas…). Celle-ci repose nécessairement sur une standardisation et une modélisation du « métier ». L'approche MDD (Model Driven Development) du génie logiciel et l'approche DSM (Domain Specific Modeling), apporte des éléments de solution reposant sur l'utilisation de « templates métiers ». Toutefois, il est fondamental de générer des livrables de qualité et du code API (Automates Programmables Industriels) sûr de fonctionnement. Le second axe de recherche s'intéresse à la commande sûre de fonctionnement. Trois approches de synthèse de la commande (la Supervisory Control Theory (SCT), la synthèse algébrique, la commande par contraintes logiques) permettant a priori de répondre à ces objectifs de sûreté sont présentées et discutées. La commande par contraintes logiques présente l'avantage majeur de séparer la sécurité (qui est vérifiée formellement hors ligne par model-checking) et le fonctionnel, et de pouvoir être utilisée avec des programmes API existants, ne remettant pas ainsi en cause la méthodologie de travail des chargés d'études. / The research project presented in this thesis has been realized with the collaboration of the Engineer Department of the SNCF and the CReSTIC of the University of Reims Champagne-Ardenne. The goal of this project is to contribute to the improvement of the control studies of the electrification projects realized by the design engineers. This project must meet human, economic and technical aims expressed by the SNCF applied to the field of the Power Supply Equipments of the Electrified Lines (EALE in french). To answer these problems, a methodology for the automation studies is proposed. It integrates two research orientations were studied. The first axis is the automatic generation the deliverables (codes, documents, diagrams…). This axis is based on standardization and modeling of the “work”. MDD (Model Driven Development) and DSM (Domain Specific Modeling) approaches, brings suggestions for solution based on the use of “work templates”. However, it is fundamental to generate quality deliverables and safe PLC (Programmable Logic Controller) code. The second research orientation is interested in safe control. Three approaches of control synthesis (Supervisory Control Theory (SCT), the algebraic synthesis, the control by logical constraints) permitting a priori to reach these aims of safety are presented and discussed. The major advantage of the control by logical constraints is to separate the safety (which is checked formally off line by model-checking) and the functional parts. It can be used with existing PLC programs, which doesn't change thus the working methodology of the design engineers.

No description available.

Em um cenário de aumento de competitividade, crescente expectativa por inovações do produto e necessidade de atender diferentes perfis de consumidores, o conceito de gerenciamento de cadeias de suprimentos globais (GSCM) surge como uma estratégia para coordenar mais eficazmente as atividades dispersas geograficamente dos sistemas produtivos. Na adoção do GSCM, as organizações devem lidar com rupturas que impactam no gerenciamento das suas atividades, tais como a interrupção de vias de transporte, pane no fornecimento de energia, desastres naturais e até ataques terroristas. Nesse contexto, o trabalho introduz um procedimento sistematizado para modelagem das cadeias de suprimentos visto como um sistema a eventos discretos e sua análise por simulação das atividades do GSCM baseada em técnicas formais como a rede de Petri (PN) e o Production Flow Schema (PFS). Um exemplo é também apresentado para ilustrar e comprovar as vantagens do método proposto na análise do GSCM. / In a context of increasing competition, rising of expectations for product innovations and need to satisfy different consumer needs, the concept of global supply chain management (GSCM) emerges as a strategy to more efficiently coordinate the geographically dispersed activities of production systems. Adopting GSCM, organizations have to deal with external disruptions that impact management activities, such as transport interruption, power supply failure, natural disasters and terrorist attacks. In this way, a systematized procedure for modeling supply chains as a discrete event system and simulation analysis of GSCM activities based on formal techniques, such as Petri net (PN) and Production Flow Schema (PFS) is introduced. An example is also presented to illustrate and confirm the advantages of the proposed method for GSCM analysis.

Em um cenário de aumento de competitividade, crescente expectativa por inovações do produto e necessidade de atender diferentes perfis de consumidores, o conceito de gerenciamento de cadeias de suprimentos globais (GSCM) surge como uma estratégia para coordenar mais eficazmente as atividades dispersas geograficamente dos sistemas produtivos. Na adoção do GSCM, as organizações devem lidar com rupturas que impactam no gerenciamento das suas atividades, tais como a interrupção de vias de transporte, pane no fornecimento de energia, desastres naturais e até ataques terroristas. Nesse contexto, o trabalho introduz um procedimento sistematizado para modelagem das cadeias de suprimentos visto como um sistema a eventos discretos e sua análise por simulação das atividades do GSCM baseada em técnicas formais como a rede de Petri (PN) e o Production Flow Schema (PFS). Um exemplo é também apresentado para ilustrar e comprovar as vantagens do método proposto na análise do GSCM. / In a context of increasing competition, rising of expectations for product innovations and need to satisfy different consumer needs, the concept of global supply chain management (GSCM) emerges as a strategy to more efficiently coordinate the geographically dispersed activities of production systems. Adopting GSCM, organizations have to deal with external disruptions that impact management activities, such as transport interruption, power supply failure, natural disasters and terrorist attacks. In this way, a systematized procedure for modeling supply chains as a discrete event system and simulation analysis of GSCM activities based on formal techniques, such as Petri net (PN) and Production Flow Schema (PFS) is introduced. An example is also presented to illustrate and confirm the advantages of the proposed method for GSCM analysis.

Cette thèse s’intéresse au diagnostic et à l’observation de systèmes linéaires à commutations et à l’application au convertisseur multicellulaire série. L’objectif est de proposer des solutions pour des sous-systèmes non-observables au sens classique et dont des fautes continues ou discrètes peuvent être présentes. Après la présentation d’un état de l’art sur les techniques d’observation et de diagnostic pourles systèmes à commutations, le mémoire est scindé en deux parties. La première partie propose, d’une part, une stratégie d’estimation des états discret et continu d’un système linéaire à commutation soumis à une entrée inconnue. Un observateur hybride basé sur la théorie des modes glissants d’ordre supérieur est développé. D’autre part, deux procédures de diagnostic sont présentées. La première combine un observateur hybride et un diagnostiqueur pour détecter une faute continue. Pour la seconde, un diagnostic actif est défini sur la base de la théorie du test afin de détecter et d’isoler une faute discrète. Dans la seconde partie de ce mémoire, les étapes de la réalisation d’un convertisseur multicellulaire sont détaillées. Ensuite, un chapitre est dédié à la validation des approches théoriques d’observation et de diagnostic sur le convertisseur à trois cellules. Un observateur est synthétisé afin d’estimer les tensions des capacités. Les deux procédures de diagnostic sont appliquées pour la détection d’une variation des valeurs des capacités et le diagnostic de cellules bloquées. Enfin, une commande binaire pour le convertisseur est proposée. L’application de cette stratégie permettra, par la suite, la commande tolérante aux fautes du convertisseur. / This thesis deals with the diagnosis and the observation of a large class of switched linear systems with an application to the multicellular converter. The objective is to provide solutions for non-observable subsystems in the classical sense which can be influenced by continuous or discrete faults. After presenting a state of the art for the observation and diagnostic techniques for switched systems, the report is divided into two parts. The first part provides, in one hand, a strategy for the discrete and continuous states estimation for linear switched system with unknown input. A hybridobserver based on higher order sliding mode is developed. On the other hand, two diagnostic procedures are presented. The first one combines a hybrid observer and a discrete diagnoser to detect a continuous fault. In the second one, an active diagnosis is defined based on the testing theory to detect and isolate a discrete fault. In the second part of this thesis, the different steps to create a multicellular converter are detailed. Then, a chapter is dedicated to the validation of the theoretical approaches for the observation and diagnosis of the three cells converter. An observer is designed to estimate the capacitor voltages. The two proposed diagnosis procedures are applied to detect a change in the capacitance values and to diagnose locked cells. Finally, a binary control for the converter is proposed. The implementation of this strategy will allow, in the future, the fault tolerant control of the converter.