Presently information systems are increasingly penetrating to our daily life. Recently it is relevant to integrate the newest technologies. In that way traditional system becomes “smart” who are more economical, optimal, and self-sufficient. The biggest problem is to make a model of “smart” system. There were analyzed modeling methods, heating and cooling control systems in this job. Mathematical model for heating and cooling controller using timed Petri nets was presented. According to analyzed problems it was made verification with Matlab during experimental phase. There was made comparison evaluation of mathematical model made with timed Petri nets and fuzzy logic.

Master of Science / Industrial & Manufacturing Systems Engineering / David H. Ben-Arieh / Telemental health systems, a form of telemedicine, use electronic communication media to provide patients in remote locations access to psychological and psychiatric specialists. The structure of telemental health systems has a major impact on their performance. Discrete-event simulations offer useful results concerning capacities and utilization of specific resources. Simulation, however, cannot provide theoretical properties of analyzed systems. Petri net representations of systems can overcome this shortfall, offering a wide range of easily-analyzed and useful properties. Their ability to model resource conflict, parallel activities, and failure modes fits nicely with the reality of telemental health systems. Analysis of behavioral properties of Petri nets can provide meaningful information for system analysts. The most useful properties include net boundedness, liveness, and non-reachability of certain undesirable states. The thesis discusses methods to find all these properties. Specifically, it provides property-preserving net reductions to facilitate analysis of boundedness and liveness and describes an integer programming model to solve reachability and coverability problems. Moreover, this thesis outlines a simulation analysis of synchronous and asynchronous telemental health systems. The paper then describes a Petri net model of a generic telemental health delivery system. The paper subjects the model to an integer programming model and net reduction. The integer programming model indicated that the number of resources in the system remains static, full utilization of resources at a given time is possible, conflict over resources is possible, and improper work prioritization is possible within the model. Net reduction and analysis with open-source software showed that the model is bounded and live. These results can aid telemedicine system architects in diagnosing potential process issues. Additionally, the methods described in the paper provide an excellent tool for further, more granular analysis of telemedicine systems.

Maintenance models are critical for evaluation of the alternative maintenance policies for modern engineering systems. A poorly selected policy can result in excessive life-cycle costs as well as unnecessary risks for catastrophic failures of the system. Economic dependence refers to the difference between the cost of combining the maintenance of a number of components and the cost of performing the same maintenance actions individually. Maintenance that takes advantage of this difference is often called opportunistic. Large number of components and economic inter-dependence are two pervasive characteristics of modern engineering systems that make the modeling of their maintenance processes particularly challenging. Simulation is able to handle both of these characteristics computationally, but the complexity, especially from the model verification perspective, becomes overwhelming as the number of components increases. This research introduces a new procedure for maintenance models of multi-unit repairable systems with economic dependence among its components and under opportunistic maintenance policies. The procedure is based on the stochastic Petri net with aging tokens modeling framework and it makes use of a component-level model approach to overcome the state explosion of the model combined with a novel order-reduction scheme that effectively combines the impact of other components into a single distribution. The justification for the used scheme is provided, the accuracy is assessed, and applications for the systems of realistic complexity are considered.

In 1996, a concept was proposed by the UK Ministry of Defence with the intention of making the field of reliability more useful to the end user, particularly within the field of military aerospace. This idea was the Maintenance Free Operating Period (MFOP), a duration of time in which the overall system can complete all of its required missions without the need to undergo emergency repairs or maintenance, with a defined probability of success. The system can encounter component or subsystem failures, but these must be carried with no effect to the overall mission, until such time as repair takes place. It is thought that advanced technologies such as redundant systems, prognostics and diagnostics will play a major role in the successful use of MFOP in practical applications. Many types of system operate missions that are made up of several sequential phases. For a mission to be successful, the system must satisfactorily complete each of the objectives in each of the phases. If the system fails or cannot complete its goals in any one phase, the mission has failed. Each phase will require the system to use different items, and so the failure logic changes from phase to phase. Mission unreliability is defined as the probability that the system fails to function successfully during at least one phase of the mission. An important problem is the efficient calculation of the value of mission unreliability. This thesis investigates the creation of a modelling method to consider as many features of systems undergoing both MFOPs and phased missions as possible. This uses Petri nets, a type of digraph allowing storage and transit of tokens which represent system states. A simple model is presented, following which, a more complex model is developed and explained, encompassing those ideas which are believed to be important in delivering a long MFOP with a high degree of confidence. A demonstration of the process by which the modelling method could be used to improve the reliability performance of a large system is then shown. The complex model is employed in the form of a Monte-Carlo simulation program, which is applied to a life-size system such as may be encountered in the real world. Improvements are suggested and results from their implementation analysed.

Nous proposons dans cette thèse plusieurs contributions relatives à la vérification quantitative des systèmes. Cette discipline vise à évaluer les propriétés fonctionnelles et les performances d'un système. Une telle vérification requiert deux ingrédients : un modèle formel de représentation d'un système et une logique temporelle pour exprimer la propriété considérée. L'évaluation est alors faite par une méthode statistique ou numérique. La complexité spatiale des méthodes numériques, proportionnelle à la taille de l'espace d'états, les rend impraticables si les systèmes présentent une combinatoire importante. La méthode de comparaison stochastique basée sur les chaînes de Markov censurées réduit la mémoire occupée en restreignant l'analyse à un sous-ensemble des états de la chaîne originale. Dans cette thèse nous fournissons de nouvelles bornes dépendant de l'information disponible relative à la chaîne. Nous introduisons une nouvelle logique temporelle quantitative appelée Hybrid Automata Stochastic Logic (HASL), pour la vérification des processus stochastiques à événements discrets (DESP).HASL emploie les automates linéaires hybrides (LHA) pour sélectionner des préfixes de chemins d'exécution d'un DESP. LHA permet de collecter des informations élaborées durant la génération des chemins, fournissant ainsi à l'utilisateur un moyen d'exprimer des mesures sophistiquées. HASL supporte donc des raisonnements temporels mixés avec une analyse à base de récompenses. Nous avons aussi développé COSMOS, un outil qui implémente la vérification statistique de formules HASL pour des réseaux de Petri stochastiques. Les ateliers flexibles (FMS) ont souvent été modélisés par des réseaux de Petri. Cependant le modélisateur doit avoir une bonne connaissance de ce formalisme. Afin de faciliter cette modélisation nous proposons une méthodologie de modélisation compositionnelle orientée vers les applications qui ne requiert aucune connaissance des réseaux de Petri. / We propose in this thesis several contributions related to the quantitative verification of systems. This discipline aims to evaluate functional and performance properties of a system. Such a verification requires two ingredients: a formal model to represent the system and a temporal logic to express the desired property. Then the evaluation is done with a statistical or numerical method. The spatial complexity of numerical methods which is proportional to the size of the state space of the model makes them impractical when the state space is very large. The method of stochastic comparison with censored Markov chains is one of the methods that reduces memory requirements by restricting the analysis to a subset of the states of the original Markov chain. In this thesis we provide new bounds that depend on the available information about the chain. We introduce a new quantitative temporal logic named Hybrid Automata Stochastic Logic (HASL), for the verification of discrete event stochastic processes (DESP). HASL employs Linear Hybrid Automata (LHA) to select prefixes of relevant execution paths of a DESP. LHA allows rather elaborate information to be collected on-the-fly during path selection, providing the user with a powerful mean to express sophisticated measures. In essence HASL provides a unifying verification framework where temporal reasoning is naturally blended with elaborate reward-based analysis. We have also developed COSMOS, a tool that implements statistical verification of HASL formulas over stochastic Petri nets. Flexible manufacturing systems (FMS) have often been modelized by Petri nets. However the modeler should have a good knowledge of this formalism. In order to facilitate such a modeling we propose a methodology of compositional modeling that is application oriented and does not require any knowledge of Petri nets by the modeler.

Cette thèse traite de l'identification des systèmes à événements discrets (SED) automatisés dans un contexte industriel. En particulier, le travail aborde les systèmes formés par un processus et un automate programmable (AP) fonctionnant en boucle fermée - l'identification a pour but d’obtenir un modèle approximatif exprimé en réseaux de Petri interprétés (RPI) à partir du comportement externe observé sous la forme d'une seule séquence de vecteurs d’entrée-sortie de l’AP. Tout d'abord, une analyse des méthodes d'identification est présentée, ainsi qu’une étude comparative des méthodes récentes pour l'identification des SED. Puis le problème abordé est décrit - des importantes caractéristiques technologiques dans les systèmes automatisés par l’AP sont détaillées. Ces caractéristiques doivent être prises en compte dans la résolution du problème, mais elles ne peuvent pas être traitées par les méthodes existantes d’identification. La contribution principale de cette thèse est la création de deux méthodes d’identification complémentaires. La première méthode permet de construire systématiquement un modèle RPI à partir d'une seule séquence entrée-sortie représentant le comportement observable du SED. Les modèles RPI décrivent en détail l’évolution des entrées et sorties pendant le fonctionnement du système. La seconde méthode considère des SED grands et complexes - elle est basée sur une approche statistique qui permettre la construction des modèles en RPI compactes et expressives. Elle est composée de deux étapes - la première calcule à partir de la séquence entrée-sortie, la partie réactive du modèle, constituée de places observables et de transitions. La deuxième étape fait la construction de la partie non-observable, en rajoutant des places pour permettre la reproduction de la séquence entrée-sortie. Les méthodes proposées, basées sur des algorithmes de complexité polynomiale, ont été implémentées en outils logiciels, lesquels ont été testés avec des séquences d’entrée-sortie obtenues à partir des systèmes réels en fonctionnement. Les outils sont décrits et leur application est illustrée à travers deux cas d’étude. / This thesis deals with the identification of automated discrete event systems (DES) operating in an industrial context. In particular the work focuses on the systems composed by a plant and a programmable logic controller (PLC) operating in a closed loop- the identification consists in obtaining an approximate model expressed in interpreted Petri nets (IPN) from the observed behaviour given under the form of a single sequence of input-output vectors of the PLC. First, an overview of previous works on identification of DES is presented as well as a comparative study of the main recent approaches on the matter. Then the addressed problem is stated- important technological characteristics of automated systems and PLC are detailed. Such characteristics must be considered in solving the identification problem, but they cannot be handled by previous identification techniques. The main contribution in this thesis is the creation of two complementary identification methods. The first method allows constructing systematically an IPN model from a single input-output sequence representing the observable behaviour of the DES. The obtained IPN models describe in detail the evolution of inputs and outputs during the system operation. The second method has been conceived for addressing large and complex industrial DES- it is based on a statistical approach yielding compact and expressive IPN models. It consists of two stages- the first one obtains, from the input-output sequence, the reactive part of the model composed by observable places and transitions. The second stage builds the non observable part of the model including places that ensure the reproduction of the observed input-output sequence. The proposed methods, based on polynomial-time algorithms, have been implemented in software tools, which have been tested with input-output sequences obtained from real systems in operation. The tools are described and their application is illustrated through two case studies.

Systems biology aims to describe and understand biology at a global scale where biological systems function as a result of complex mechanisms that happen at several scales. Modelling and simulation are computational tools that are invaluable for description, understanding and prediction these mechanisms in a quantitative and integrative way. Thus multi-scale methods that couple the design, simulation and analysis of models spanning several spatial and temporal scales is becoming a new emerging focus of systems biology. This thesis uses an exemplar – Planar cell polarity (PCP) signalling – to illustrate a generic approach to model biological systems at different spatial scales, using the new concept of Hierarchically Coloured Petri Nets (HCPN). PCP signalling refers to the coordinated polarisation of cells within the plane of various epithelial tissues to generate sub-cellular asymmetry along an axis orthogonal to their apical-basal axes. This polarisation is required for many developmental events in both vertebrates and non-vertebrates. Defects in PCP in vertebrates are responsible for developmental abnormalities in multiple tissues including the neural tube, the kidney and the inner ear. In Drosophila wing, PCP is seen in the parallel orientation of hairs that protrude from each of the approximately 30,000 epithelial cells to robustly point toward the wing tip. This work applies HCPN to model a tissue comprising multiple cells hexagonally packed in a honeycomb formation in order to describe the phenomenon of Planar Cell Polarity (PCP) in Drosophila wing. HCPN facilitate the construction of mathematically tractable, compact and parameterised large-scale models. Different levels of abstraction that can be used in order to simplify such a complex system are first illustrated. The PCP system is first represented at an abstract level without modelling details of the cell. Each cell is then sub-divided into seven virtual compartments with adjacent cells being coupled via the formation of intercellular complexes. A more detailed model is later developed, describing the intra- and inter-cellular signalling mechanisms involved in PCP signalling. The initial model is for a wild-type organism, and then a family of related models, permitting different hypotheses to be explored regarding the mechanisms underlying PCP, are constructed. Among them, the largest model consists of 800 cells which when unfolded yields 164,000 places (each of which is described by an ordinary differential equation). This thesis illustrates the power and validity of the approach by showing how the models can be easily adapted to describe well-documented genetic mutations in the Drosophila wing using the proposed approach including clustering and model checking over time series of primary and secondary data, which can be employed to analyse and check such multi-scale models similar to the case of PCP. The HCPN models support the interpretation of biological observations reported in literature and are able to make sensible predictions. As HCPN model multi-scale systems in a compact, parameterised and scalable way, this modelling approach can be applied to other large-scale or multi-scale systems.

O objetivo deste trabalho é o estudo dos processos informados de automação, isto é, onde o fluxo e armazenagem de informação são determinantes para o processo de negócio (PN), além de servir para verificação de qualidade, recuperação de erros, rastreabilidade de ocorrências anômalas, etc. Aborda-se em especial um tratamento onde a internacionalização do acesso aos dados (sistema EPCIS) passa por um elemento de captura e distribuição local, chamado SAVANT-2, que acaba por ser o elemento chave para controle do fluxo e para o desenvolvimento dos projetos (Dos Santos, 2005). As informações são capturadas por leitores de RFID, e não em código de barras como é feito convencionalmente. As etiquetas de código de barras geraram uma revolução nos sistemas de identificação há algumas décadas atrás, mas hoje se mostram inadequadas num número crescente de casos. O código de barras pode ser extremamente barato, mas tem baixa produtividade além de baixa capacidade de armazenamento de dados e uma dependência maior das operações manuais, quando comparado a outras tecnologias de suporte de dados. Um estudo de caso será feito na automação de acervos, onde a informação de base é a retirada e a devolução de obras por usuários, que é atualizada dinamicamente e está intimamente ligada à missão do próprio sistema de controle do acervo. Esse trabalho segue a mesma abordagem proposta por (Tavares, 2006) e (Dos Santos, 2005), ou seja, controlar a informação corporativa localmente e selecionar, além do código de identificação, as informações que podem e devem ser estrategicamente compartilhadas com o restante do mundo. Em outras palavras utilizaremos a modelagem do fluxo de informação em Redes de Petri e os sistemas denominados de SAVANT-2 e EPCIS-2.Para isso, foram desenvolvidos novos módulos EPCIS-2 e SAVANT-2 adaptados dos já desenvolvidos, só que acoplados a leitores e sensores, que compõe um piloto simplificado de um sistema de controle para biblioteca. Este protótipo instalado no Design Lab da Escola Politécnica da Universidade de São Paulo gerencia o acervo de livros e mídias do laboratório. Este é não somente o 1º acervo da América Latina automatizado com sistema utilizando a tecnologia RFID, mas também o primeiro automatizado com base na Rede EPC e com a análise de eventos atípicos de seus processos no mundo. / The objective of this work is to study the informed automation processes, in which the information flow and storage are essential to the business process, providing quality control, error recovering, traceability and the track of anomalous occurrences. In such processes the capture of the proper pieces of information is a key point to the automation process, observing the mission assigned to the system. We focus on a case-study of a heap library service, treating the information with RFID (Radio Frequency Identification), reusing the intermediary system SAVANT-2 (Dos Santos, 2005) and a database to the target storage. Barcode labels caused a revolution in the identification systems a few decades ago, but have become inadequate in an increasing number of cases. Barcodes can be extremely inexpensive, but it has low productivity and low data storage capacity. Moreover, it depends more on manual operation, when compared to other technologies. This work follows the line so study of informed automation concepts explored in the work of (Tavares, 2006) and (Dos Santos, 2005) in a manufacturing application. In other words, the control of the corporate information, besides the identification code, is done locally and afterwards, strategic information is selected to be shared with the rest of the world. We use the dataflow modeling in Petri Nets and systems named SAVANT-2 and EPCIS-2. In order to support this work, new modules EPCIS-2 and SAVANT-2, proposed by (Tavares, 2006) and (Dos Santos, 2005) are expanded e implemented, adapting the existing ones to readers and sensors. A simplified project will be implemented in the Design Lab of the Escola Politécnica, Universidade de São Paulo (USP). This is not only the first catalog in the Latin America automated with an RFID system, but also the first in the world with automation based on EPC Networks and with atypical events analysis of its processes.

Este trabalho introduz a formalização algébrica do F-MFG (Functional Mark Flow Graph) para a análise e simulação computacional de modelos de sistemas antropocêntricos de produção, onde são enfocadas a interação e a interface do elemento humano com o sistema produtivo. Abordando os sistemas antropocêntricos como uma classe de sistemas a eventos discretos, o F-MFG, que é uma técnica baseada nas redes de Petri, comprova ter potencial para descrever detalhadamente as ações e estados do sistema. O F-MFG, em conjunto com a Metodologia PFS/MFG (Production Flow Schema/ Mark Flow Graph), estabelece um procedimento eficiente para o projeto de sistemas antropocêntricos, tornando concisa a modelagem e a posterior avaliação estrutural e comportamental do sistema. / This work introduces an algebraic formalization of F-MFG (Functional-Mark Flow Graph). This formalization is effective for analysis and simulation of anthropocentric production systems, which is focused on the interaction and interface between human elements and production systems. When approaching anthropocentric systems as Discrete Event Dynamic Systems, the F-MFG, which is a Petri Net based technique, has been demonstrated its potential capabilities in describing detailed models of system actions and states. The PFS/MFG Methodology (Production Flow Schema/Mark Flow Graph Methodology) combined with F-MFG establishes an efficient procedure for the design of anthropocentric systems. This procedure results in concise modeling and analysis (system structural and behavioral evaluation) processes.

As importantes transformações das organizações nos últimos anos mostram que diferentes princípios de qualidade, competitividade e inovação devem ser conjugados para o projeto de sistemas de controle de sistemas produtivos. Esta abordagem, que traz benefícios às organizações, é viável em virtude da evolução das estratégias de integração e da tecnologia da informação. A partir da norma em elaboração ANSI/ISA S95, esta dissertação desenvolve procedimentos para definição do escopo funcional, requisitos e modelagem para o projeto de sistemas de controle de sistemas produtivos integrados à organização, atuando de forma estruturada, em conformidade com padrões técnicos de automação e engenharia de requisitos. Como resultados, estabelece procedimentos para o início do projeto que definem o escopo funcional do sistema de controle de sistemas produtivos integrado à gestão da organização. A seguir, estes procedimentos estabelecem os domínios semânticos dos subsistemas necessários para o desempenho de suas funções, acompanhados das respectivas linguagens de modelagem. A dissertação completa-se com a modelagem dos subsistemas através do E-MFG com comunicadores, modelagem esta que suporta os padrões existentes de programação da automação. Neste contexto, parte-se dos requisitos de cada subsistema coletados por uma versão modificada do caso de uso da UML, convertidos finalmente para o E-MFG com comunicadores. / The important changes that are happening inside organizations show that different principles of quality, innovation and competition should be combined during the design of control system of production systems. This approach is possible thanks to the evolution of integration strategy and information technology, generating benefits to organizations. Procedures are established to define system’s functional scope, requirements and models, based on the integrated approach of ANSI/ISA S95 standard. The procedures are developed by a structured process and according to automation standards and requirements engineering. The work’s first result is a procedure that defines a functional scope for control system design of production systems integrated with organization. As a second result, procedures help to define semantic domains of all subsystems needed to develop control system functions, as well as the modeling techniques for each domain. The result is complemented by modeling subsystems using an extended version of Mark Flow Graph (E-MFG with communicators). This task has the assistance of a modified use case version from “Unified Modeling Language" to collect requirements before modeling.