Os sistemas de manufatura há muito vêm sendo objeto de interesse por profissionais e pesquisadores devido à busca de melhores técnicas visando o aumento da produtividade bem como pelo aumento da competitividade empresarial ao longo dos anos. Dentre seus componentes, o sistema de movimentação de materiais merece atenção especial pois, apesar de não aumentar o valor do produto, é responsável por manter o fluxo de materiais entre máquinas, células de manufatura, centros de custos ou mesmo entre empresas, que é imprescindível para qualquer sistema produtivo. Neste contexto, o presente trabalho propõe uma metodologia para a modelagem de sistemas flexíveis de movimentação de materiais e partes em ambiente fabril, focando-se em sistemas cuja movimentação possa ser realizada por VATs (Veículos Autônomos de Transporte). Considerando-se o sistema de movimentação de materiais como sendo um sistema a eventos discretos (SEDs), pode-se empregar técnicas derivadas das Redes de Petri como o PFS (Production Flow Schema) e o E-MFG (Enhanced Mark Flow Graph) na modelagem de tais sistemas. Para tanto, foram introduzidos conceitos de orientação a objetos ao E-MFG de forma a ampliar sua capacidade de modelagem, possibilitando a migração de um paradigma de modelagem orientada a processos para um de modelagem híbrida orientada a processos e a objetos. Como estudo de caso, apresenta-se a modelagem de uma simplificação do sistema de movimentação de materiais da Mercedes Benz do Brasil, situada em São Bernardo do Campo, São Paulo, para a qual se aplica a metodologia proposta. / Manufacturing systems have been object of interest of many professionals and researchers through the years due to the search of better methods for raising goods productivity and managerial competitiveness. Among its components, the material movement system deserves special attention because even not increasing the product value, it is responsible for keeping the flow of materials between machines, manufacturing cells, cost centers and also between companies, which is indispensable for any productive system. In this context, this work proposes a methodology for modeling flexible systems for materials and parts movement in the industrial environment, focusing on systems whose movement can be performed by AGVs (Autonomous Guided Vehicles). Considering the materials movement system as a Discrete Event System (DES), techniques derived from Petri Nets as PFS (Production Flow Schema) and E-MFG (Enhanced Mark Flow Graph) can be used for modeling those systems. To this purpose, concepts of object orientation are introduced to E-MFG in order to increase its modeling capacity, allowing the migration from the process oriented modeling paradigm to an hybrid object and process oriented modeling. A simplification of the materials movement system of the plant of "Mercedes Benz do Brasil", which is located in São Bernado do Campo, São Paulo, was used as a study case to illustrate the methodology presented.

De nos jours, la mise au point de logiciels ou de systèmes fiables est de plus en plus difficile. Les nouvelles technologies impliquent de plus en plus d'interactions entre composants complexes, dont l'analyse et la compréhension deviennent de plus en plus délicates. Pour pallier ce problème, les domaines de la vérification et de la validation ont connu un bond significatif avec la mise au point de nouvelles méthodes, réparties en deux grandes familles : la vérification formelle et la simulation. Longtemps considérées comme à l'opposée l'une de l'autre, les recherches récentes essaient de rapprocher ces deux grandes familles de méthodologies. Dans ce cadre, les travaux de cette thèse proposent une nouvelle approche pour intégrer la simulation dites à évènements discrets aux méthodes formelles. L'objectif est d'améliorer les méthodes formelles existantes, en les combinant à la simulation, afin de leur permettre de détecter des erreurs qu'elles ne pouvaient déceler avant, notamment sur des systèmes temporisés. Cette approche nous a conduit à la mise au point d'un nouveau langage formel, le DEv-PROMELA. Ce nouveau langage, créé à partir du PROMELA et du formalisme DEVS, est à mi-chemin entre un langage de spécifications formelles vérifiables et un formalisme de simulation. En combinant alors un model-checking traditionnel et une simulation à évènements discrets sur le modèle exprimé dans ce nouveau langage, il est alors possible de détecter et de comprendre des dysfonctionnements qu'un model-checking seul ou qu'une simulation seule n'auraient pas permis de trouver. Ce résultat est notamment illustré à travers les différents exemples étudiés dans ces travaux. / Nowadays, making reliable software and systems is become harder. New technologies imply more and more interactions between complex components, whose the analysis and the understanding are become arduous.To overcome this problem, the domains of verification and validation have known a significant progress, with the emergence of new automatic methods that ensure reliability of systems. Among all these techniques, we can find two great families of tools : the formal methods and the simulation. For a long time, these two families have been considered as opposite to each other. However, recent work tries to reduce the border between them. In this context, this thesis proposes a new approach in order to integrate discrete-event simulation in formal methods. The main objective is to improve existing model-checking tools by combining them with simulation, in order to allow them detecting errors that they were not previously able to find, and especially on timed systems. This approach led us to develop a new formal language, called DEv-PROMELA. This new language, which relies on the PROMELA and on the DEVS formalism, is like both a verifiable specifications language and a simulation formalism. By combining a traditional model-checking and a discrete-event simulation on models expressed in DEv-PROMELA, it is therefore possible to detect and to understand dysfunctions which could not be found by using only a formal checking or only a simulation. This result is illustrated through the different examples which are treated in this work.

Most of the past research on the problem of deadlock avoidance for complex resource allocation systems (RAS) has acknowledged the fact that the computation of the maximally permissive (optimal) deadlock avoidance policy (DAP) possesses super-polynomial complexity for most RAS classes, and therefore, it has resorted to solutions that trade off maximal permissiveness for computational tractability. In this work, we distinguish between the off-line and the on-line computation that is required for the effective implementation of the maximally permissive DAP, and we seek to develop representations of this policy that will require minimal on-line computation. The particular representation that we adopt is that of a compact classifier that will effect the underlying dichotomy of the reachable state space into safe and unsafe subspaces. Through a series of reductions of the derived classification problem, we are also able to attain extensive reductions in the computational complexity of the off-line task of the construction of the sought classifier. In a first study of the aforementioned problem, we restrict our attention to a particular RAS class that is motivated by an ongoing project called Gadara. This particular RAS class accepts the separation of the safe and unsafe subspaces of its instantiations through a set of linear inequalities. We propose design procedures that will construct a classifier employing the minimum possible number of linear inequalities, and we formally establish their "completeness", i.e., their ability to provide an effective classifier for every instance of the considered RAS class. We also offer heuristics that, if necessary, can alleviate the computational effort that is necessary for the construction of the sought classifier. We extend the aforementioned results to encompass more general RAS classes, where the sought dichotomy might not be represented by a set of linear inequalities. To this end, we propose new parametric and non-parametric classification schemes for this more complex case, and establish formally their completeness. We also provide effective and computationally efficient procedures for the synthesis of the sought classifiers. A bottleneck in the developments described above is defined by the fact that they presuppose the availability of the enumerations of the RAS safe and unsafe subspaces. To address this obstacle, we propose a novel approach for the deployment of the maximally permissive DAP for RAS, that is based on the identification and the efficient storage of a critical subset of states of the underlying RAS state space. In particular, the proposed algorithm provides those critical states, while avoiding the complete enumeration of the RAS state space. Furthermore, we extend the existing theory on maximally permissive deadlock avoidance, so that it can handle RAS with reader/writer (R/W) locks. A key challenge that is posed by this new RAS class stems from the fact that the underlying state space is not necessarily finite. We effectively address this obstacle by taking advantage of special structure that exists in the set of unsafe states and enables a finite representation of this set through its minimal elements. Finally, we would like to mention that numerical experimentation demonstrates the efficacy of the proposed approaches, and establishes their ability to support the deployment of maximally permissive DAP for RAS with very large structure and state spaces. To the best of our knowledge, these experiments also establish the ability of the proposed methodology to effectively compute tractable implementations of the maximally permissive DAP for problem instances significantly beyond the capacity of any other approach currently available in the literature. Moreover, this is the first work to address the RAS with R/W locks.

La méthode des invariants est une des plus utilisées méthodes de synthèse pour les SED modélisés par des réseaux de Petri (RdP). Cependant, elle ne garantit pas en général une solution optimale dans la présence de l'incontrôlabilité. Dans ce travail nous proposons une solution à ce problème pour les RdP généralisés. Premièrement, nous proposons une solution d'identification des contraintes admissibles pour les RdP saufs non-conservatifs. La méthode repose sur une définition des contraintes contenant des marquages complémentés. Ceux-ci sont après éliminés en exploitant les composants conservatifs des RdP. Deuxièmement, nous avançons une technique de détermination des contraintes admissibles pour les RdP généralisés. La méthode est basée sur une vision spatiale de l'espace d'états du modèle. Les contraintes sont dérivées de l'équation d'hyperplan affin qui sépare les régions interdite- et autorisée- de cet espace. Nous proposons un algorithme pour le calcul du contrôleur optimal minimal. / The place-invariants method is one of the most popular controller synthesis approaches for Petri net (PN) modeled DES. Unfortunately, the observance of the constraints is not certain in the presence of uncontrollable transitions. This thesis offers a solution to this problem for ordinary and generalized PNs. We begin by studying safe non-conservative PNs, and devising a constraint-determination technique that will always provide a set of admissible constraints for this type of model. The approach stems from the general definition of forbidden states --- that of marking vectors. In the second part of our work, we present an admissible constraint-determination technique for generalized PNs. The method is based on a special view of the system's state space. The constraints are derived from the equation of the affine hyper-plane separating the authorized- and forbidden- regions of this space. We propose an algorithm that allows the identification of the minimal maximally permissive controller.

Submitted by Renata Lopes (renatasil82@gmail.com) on 2017-04-25T11:55:26Z No. of bitstreams: 1 wolmararaujoneto.pdf: 9045744 bytes, checksum: 685167b5aabc68d680681643c44b7a4e (MD5) / Approved for entry into archive by Adriana Oliveira (adriana.oliveira@ufjf.edu.br) on 2017-04-25T12:12:34Z (GMT) No. of bitstreams: 1 wolmararaujoneto.pdf: 9045744 bytes, checksum: 685167b5aabc68d680681643c44b7a4e (MD5) / Made available in DSpace on 2017-04-25T12:12:34Z (GMT). No. of bitstreams: 1 wolmararaujoneto.pdf: 9045744 bytes, checksum: 685167b5aabc68d680681643c44b7a4e (MD5) Previous issue date: 2014-08-25 / CNPq - Conselho Nacional de Desenvolvimento Científico e Tecnológico / A presente dissertação tem como objetivo principal desenvolver uma metodologia capaz de auxiliar no projeto e implementação de controles para sistemas a eventos discretos (SED) de forma a otimizar a modelagem, documentação e implantação da planta estudada. Para tanto a definição tradicional de autômato foi alterado para incluir um novo subconjunto de estados obrigatórios, isto é, estados que o sistema deve passar antes de chegar a um estado marcado. Seguindo a modelagem tradicional, cada subsistema é modelado através desta nova abordagem. Em uma segunda etapa, uma nova iteração de análise de cada subsistema é realizada para restringir situações indesejadas do sistema. Com esta fase finalizada os subsistemas são mesclados através de uma técnica tradicional de autômatos em paralelo. O sistema final resultante é apresentado a um otimizador, baseado em PROLOG, que busca a melhor sequência de eventos obedecendo a todas as restrições modeladas e termine no estado marcado informado pelo projeto. Este resultado fornece a Rede de Petri ideal do sistema e sua programação em GRAFCET. Tais métodos serão testados em componentes de um sistema de manufatura flexível real. / The present master thesis has as its main goal to develop a methodology able to assist in design and implementation of discrete event system (DES) controllers in order to optimize the modeling, documentation and deployment of plant in study. To do so the automaton traditional concept was changed to include a new subset of mandatory states, i.e. states that the system should pass before reach a marked state. Following the traditional modeling, each subsystem is modeled using this new approach. In a second step, a new iteration of analysis of each subsystem is performed to restrain system’s unwanted situations. At the end of this step the subsystems are composed by a traditional parallel automatons technique. The resulting system is presented to an optimizer, based in PROLOG, which searches the best event sequence obeying to all modeled restrictions and ends in the marked state defined in design. This result provides the ideal Petri Net of the system and its GRAFCET programming. Such methods will be tested in a flexible real manufacturing system.

Les travaux présentés dans ce mémoire de thèse représentent une contribution au problème de diagnostic des Systèmes à Evénements Discrets (SEDs). L'objectif de ce travail est dans un premier temps une proposition d'une démarche de diagnostic en exploitant l'aspect temporel caractérisant l'occurrence des événements. Pour cela, le système est modélisé par des graphes temporels appartenant au formalisme des automates temporisés. L'approche est conçue selon une architecture décentralisée afin d'éviter toute explosion combinatoire dans la construction des modèles. Elle a permis la détection et localisation des défauts abruptes survenant sur les équipements notamment en combinant des conditions d'autorisation d'événements et des fonctions de non-occurrence d'événements.Dans un second temps, les défauts graduels issus du process sont considérés. Pour cela, les contraintes temporelles exprimant les dates d'occurrence des événements dans les Templates et les Chroniques sont modélisées par des distributions de probabilités (DPs). Celles-ci sont utilisées afin de caractériser un fonctionnement normal, dégradé ou défaillant de chaque sous-système avec un certain degré de certitude. Cette identification du fonctionnement est représentée par la valeur d'un indicateur de dégradation. / The work presented in this thesis represents a contribution to the problem of diagnosis in discrete event systems (DES). The objective of our work consists in a proposition for a diagnostic approach by exploiting the temporal aspect which characterizing the occurrence of events. For this, the system is modeled by temporal graphs belonging to the timed automata formwork. The approach is designed according to the decentralized architecture to avoid any combinatorial explosion in the construction of the models. It has allowed the detection and isolation of abrupt faults occurring on equipment by combining the enablement conditions of events and the Boolean functions for the non-occurrence of events.Secondly, gradual faults coming from the process its self are considerate. For this, time constraints expressing the dates of occurrence of events in the Templates and Chronicles are modeled by probability distributions (PDs). These are used to characterize normal, degraded or failed functioning of each subsystem with a degree of certainty. Identification of this functioning mode is represented by the value of a degradation indicator.

Les travaux effectués durant cette thèse portent sur la spécification, l'analyse et l'application de systèmes a événements discrets pour la modélisation de processus biologiques stochastiques en biologie des systèmes. Le point de départ de cette thèse est le langage de modélisation AltaRica, que nous étendons afin de permettre de décrire des événements temporisés selon des distributions de probabilités quelconques (dégénérées, discrètes et continues). Nous définissons ensuite la sémantique de ce langage en terme d'automates de mode stochastiques et présentons trois opérations de compositions permettant de modéliser des systèmes hiérarchiques avec événements synchronisés et partage de valeurs via un mécanisme de connexion. Nous donnons ensuite au automates de mode stochastiques une sémantique en termes de systèmes de transitions dont les transitions sont étiquetées par des distributions de probabilités et des probabilités de transitions instantanées. Nous caractérisons ensuite 6 sous classes de ces systèmes de transitions et donnons pour chacune de ces classes un algorithme de simulation ainsi qu'une mesure de probabilité sur les chemins finis. Nous montrons que pour certaines de ces classes, notre sémantique est conforme avec les mesures de probabilité de chemin usuellement associées aux chaînes de Markov a temps discret, a temps continu et aux processus semi-Markoviens généralisés. Nous abordons ensuite le problème de la réutilisation de modèles continus existant dans un système discret. Nous donnons une méthode d'abstraction permettant de représenter un ensemble de trajectoires bornées ou non d'un modèle continu sous forme d'un système de transition stochastique fini. A travers des exemples tirés de la littérature, nous montrons que notre abstraction préserve les propriétés "qualitatives" (par exemple oscillations, hystérie) des modèles continus et qu'une comparaison entre trajectoires basée sur leurs représentations en termes de systèmes de transitions permet de regrouper les trajectoires en fonction de comportements qualitatifs plus fins que ceux permis par la théorie des bifurcations. Finalement, nous étudions a l'aide de ces modèles des processus liés a la division cellulaire chez les levures. En particulier, nous définissons un modèle pour le vieillissement cellulaire dans une population de levure où le comportement individuel d'une cellule est régi par une équation différentielle ordinaire et où le processus de division est régi par un système de transition. Nous montrons a l'aide de ce modèle que la survie d'une population de levure de type Schizosaccharomyces Pombe, qui se divisent par une fission médiane, n'est possible que grâce a un mécanisme de distribution non symétrique des dégâts oxydatifs entre la progéniture et la cellule souche. Cette hypothèse fut validée expérimentalement lors d'une collaboration avec le laboratoire de micro-biologie de Göteborg. / A general goal of systems biology is to acquire a detailed understanding of the dynamics of living systems by relating functional properties of whole systems with the interactions of their constituents. Often this goal is tackled through computer simulation. A number of different formalisms are currently used to construct numerical representations of biological systems, and a certain wealth of models is proposed using ad hoc methods. There arises an interesting question of to what extent these models can be reused and composed, together or in a larger framework. In this thesis, we propose BioRica as a means to circumvent the difficulty of incorporating disparate approaches in the same modeling study. BioRica is an extension of the AltaRica specification language to describe hierarchical non-deterministic General Semi-Markov processes. We first extend the syntax and automata semantics of AltaRica in order to account for stochastic labeling. We then provide a semantics to BioRica programs in terms of stochastic transition systems, that are transition systems with stochastic labeling. We then develop numerical methods to symbolically compute the probability of a given finite path in a stochastic transition systems. We then define algorithms and rules to compile a BioRica system into a stand alone C++ simulator that simulates the underlying stochastic process. We also present language extensions that enables the modeler to include into a BioRica hierarchical systems nodes that use numerical libraries (e.g. Mathematica, Matlab, GSL). Such nodes can be used to perform numerical integration or flux balance analysis during discrete event simulation. We then consider the problem of using models with uncertain parameter values. Quantitative models in Systems Biology depend on a large number of free parameters, whose values completely determine behavior of models. Some range of parameter values produce similar system dynamics, making it possible to define general trends for trajectories of the system (e.g. oscillating behavior) for some parameter values. In this work, we defined an automata-based formalism to describe the qualitative behavior of systems’ dynamics. Qualitative behaviors are represented by finite transition systems whose states contain predicate valuation and whose transitions are labeled by probabilistic delays. We provide algorithms to automatically build such automata representation by using random sampling over the parameter space and algorithms to compare and cluster the resulting qualitative transition system. Finally, we validate our approach by studying a rejuvenation effect in yeasts cells population by using a hierarchical population model defined in BioRica. Models of ageing for yeast cells aim to provide insight into the general biological processes of ageing. For this study, we used the BioRica framework to generate a hierarchical simulation tool that allows dynamic creation of entities during simulation. The predictions of our hierarchical mathematical model has been validated experimentally by the micro-biology laboratory of Gothenburg

O presente estudo apresenta a reorganização do projeto de trabalho de uma indústria produtora de equipamentos para compressão de GNV, apoiada pelo uso de sistemas a eventos discretos (SED). A empresa em questão, pioneira neste segmento na América Latina, viveu um súbito aumento na demanda de mercado que expôs fragilidades em seu sistema logístico. Problemas associados ao planejamento e controle de estoque e fluxo de materiais tornaram-se evidentes e deveriam ser resolvidos para que não prejudicassem o fluxo de vendas da empresa. Devido a complexidade existente no projeto produtivo, a simulação foi considerada como a maneira mais segura de planejar alterações nas práticas administrativas e produtivas, sem interferir na rotina da empresa. A modelagem realizada neste trabalho foi feita a partir da construção de uma cadeia de valor para o processo produtivo.Tal abordagem permitiu identificar diversos fatores que contribuíam diretamente à falta de eficiência da empresa tais como a ausência de um sistema logístico estruturado: interligação deficiente entre determinados setores administrativos e a manufatura, formação de estoques paralelos, perda excessiva por manuseio, retrabalho ou uso incorreto de componentes (hidden factory). A modelagem e a análise das propriedades dos modelos foram validadas por meio de um sistema de gestão integralizado (ERP) trabalhando com base em dados reais da empresa estudada. O estudo revelou oportunidades de melhoria baseado na reorganização da seqüência de fabricação e de abastecimento de materiais, aumento de produtividade através de realocação da mão-de-obra, organização do local de trabalho e padronização das atividades. As melhorias identificadas no estudo exploratório e na simulação foram consolidadas formando um sistema de gestão customizado para a empresa objeto do estudo. / This study presents the reorganization of the project work of an industry producing equipment for compressed natural gas (CNG), supported by the use of discrete event systems (DES). The company in question, a pioneer in this segment in Latin America, experienced a surge in market demand that has exposed weaknesses in their logistics system. Problems associated with planning and inventory control and material flow have become evident and should be resolved not to damage the flow of the companys sales. Because of the complexities that exist in productive project, the simulation was considered the safest way to plan changes in administrative and productive practices, without interfering with the routine. The modeling performed in this work was done from the construction of a value chain for the production process. This approach has identified several factors that contributed directly to the inefficiency of the company such as the absence of a structured logistics system: poor interconnection between certain administrative sectors and the manufacture, stockpiling, parallel loss by excessive handling, rework or incorrect use of components ("hidden factory"). The modeling and analysis of the properties of the models were validated by means of a management system (ERP) work based on real data of the studied company. The study revealed opportunities for improvement based on the reorganization of the sequence of manufacturing and supply materials, increased productivity through reallocation of labor, work, workplace organization and standardization activities. The improvements identified in the exploratory study and simulation were consolidated to form a customized management system to the company object of study.

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.

<p>A decentralized discrete-event system (DES) consists of supervisors that are physically distributed. Co-observability is one of the necessary and sufficient conditions for the existence of a decentralized supervisors that correctly solve the control problem. In this thesis we present a state-based definition of co-observability and introduce algorithms for its verification. Existing algorithms for the verification of co-observability do not scale well, especially when the system is composed of many components. We show that the implementation of our state-based definition leads to more efficient algorithms.</p> <p>We present a set of algorithms that use an existing structure for the verification of state-based co-observability (SB Co-observability). A computational complexity analysis of the algorithms show that the state-based implementation of algorithms result in quadratic complexity. Further improvements come from using a more compact way of representing finite-state machines namely Binary Decision Diagrams (BDD).</p> / Master of Science (MSc)