Sistemas Instrumentados de Segurança (SIS) são projetados para prevenir e/ou mitigar acidentes, evitando indesejáveis cenários com alto potencial de risco, assegurando a proteção da saúde das pessoas, proteção do meio ambiente e economia de custos com equipamentos industriais. Desta forma, é extremamente recomendado neste projeto de SIS o uso de métodos formais para garantir as especificações de segurança em conformidade com as normas regulamentadoras vigentes, principalmente para atingir o nível de integridade de segurança (SIL) desejado. Adicionalmente, algumas das normas de segurança como ANSI / ISA S.84.01; IEC 61508, IEC 61511, entre outras, recomendam uma série de procedimentos relacionados ao ciclo de vida de segurança de um projeto de SIS. Desta forma, destacam-se as atividades que compreendem o desenvolvimento e a validação dos algoritmos de controle em que se separam semanticamente os aspectos voltados para o diagnóstico de falhas críticas e o tratamento destas falhas associado a um controle de coordenação para filtrar a ocorrência de falhas espúrias. Portanto, a contribuição deste trabalho é propor um método formal para a modelagem e análise de SIS, incluindo o diagnóstico e o tratamento de falhas críticas, baseado em rede Bayesiana (BN) e rede de Petri (PN). Este trabalho considera o diagnóstico e o tratamento para cada função instrumentada de segurança (SIF) a partir do resultado do estudo de análise de riscos, de acordo com a metodologia de HAZOP (Hazard and Operability). / Safety Instrumented Systems (SIS) are design to prevent and/or mitigate accidents, avoiding undesirable high potential risk scenarios, assuring protection of people health, protecting the environment and saving costs of industrial equipment. It is strongly recommended in this design formal method to assure the safety specifications in accordance to standards regulations, mainly for reaching desired safety integrity level (SIL). Additionally, some of the safety standards such as ANSI/ISA S.84.01; IEC 61508, IEC 61511, among others, guide different activities related to Safety Life Cycle (SLC) design of SIS. In special, there are design activities that involves the development and validation of control algorithm that separate semantically aspects oriented to diagnosis and treatment of critical faults associated with a control coordination to filter spurious failures occurrence. In this context, the contribution of this work is to propose a formal method for modeling and analysis of SIS designed including diagnostic and treatment of critical faults based on Bayesian networks (BN) and Petri nets (PN). This approach considers diagnostic and treatment for each safety instrumented function (SIF) obtained according hazard and operability (HAZOP) methodology.

O sistema de proteção técnica contra incêndio (SPTCI) é um dos principais sistemas que compõem o edifício inteligente (EI), pois a eficiência do seu funcionamento afeta diretamente a segurança das pessoas e o patrimônio do prédio. O SPTCI é composto de diferentes dispositivos, estratégias de controle e atua segundo legislação específica. Devido à complexidade do SPTCI, torna-se fundamental uma modelagem adequada que permita verificar a dinâmica do sistema e sua relação com outros sistemas prediais. Neste contexto, este trabalho propõe um procedimento para a modelagem e análise de estratégias de controle para o SPTCI, integrado com outros sistemas prediais dentro do contexto de EI. A abordagem considerada para este propósito baseia-se na teoria dos sistemas a eventos discretos, na aplicação de técnicas derivadas da rede de Petri e em técnicas de análise através de simulação discreta. Com esta abordagem são desenvolvidos modelos do sistema de controle do SPTCI onde é considerada a sua relação com outros sistemas prediais. Particularmente, explora-se as extensões da rede de Petri como as técnicas Production Flow Schema e Mark Flow Graph. Um estudo de caso é apresentado para ilustrar as principais características deste procedimento. / From the point of view of property damage and personal security, the fire protection system (FPS) is one of the most important systems in an intelligent building (IB). The FPS is composed of several devices and control strategies. Furthermore, it must act in accordance with specific laws. As a consequence the design of FPSs is a complex task and it is very important to provide an adequate model that supports the verification of the FPS dynamics and its integration with others building systems, facilitating its test and validation. In this context, this work proposes a procedure to model in a systematic and rational way a FPS in the IB context. Considering the nature of the structure and processes of FPS the approach is based on the discrete event dynamic system theory and the application of the Petri net. Then, the models the FPS control system and the controlled plant must include its integration with other building systems. Particularly, it explores Petri net extensions such as Production Flow Schema and Mark Flow Graph techniques. Through an example it is illustrated the main aspects of the proposed procedure.

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

Cette thèse s'inscrit dans le cadre de la théorie des systèmes linéaires dans les dioïdes. Cette théorie concerne la sous-classe des systèmes à événements discrets modélisables par les Graphes d'Événements Temporisés (GET). La dynamique de ces graphes peut être représentée par des équations récurrentes linéaires sur des structures algébriques particulières telles que l'algèbre (max,+) ou l'algèbre (min,+).Ce mémoire est consacré à l'analyse de performances des systèmes dynamiques qui peuvent être modélisés graphiquement par des Graphes d'Événements Temporisés Généralisés (GETG). Ces derniers, contrairement au GET, n'admettent pas une représentation linéaire dans l'algèbre (min,+). Pour pallier à ce problème de non linéarité, nous avons utilisé une approche de modélisation définie sur un dioïde d'opérateurs muni de deux lois internes : loi additive correspondant à l'opération (min), et loi multiplicative équivalente à la loi de composition usuelle. Le modèle d'état obtenu, est utilisé pour évaluer les performances des GETG. Pour cela, nous avons proposé une nouvelle méthode qui a pour but de linéariser le modèle mathématique régissant l'évolution dynamique du modèle graphique, dans le but d'obtenir un modèle (min,+) linéaire. La deuxième partie de cette thèse est consacrée au problème qui consiste à déterminer les ressources à utiliser dans une ligne de production, en vue d'atteindre des performances souhaitée. Ceci est équivalent à déterminer le marquage initial de la partie commande du GETG. / This thesis is part of the theory of linear systems over dioids. This theory concerns the subclass of discrete event dynamic systems modeled by Timed Event Graphs (TEG). The dynamics of these graphs can be represented by linear recurrence equations over specific algebraic structures such as (max,+) algebra or (min,+) algebra.This report is devoted to the performance analysis of dynamic systems which can be represented graphically by Generalized Timed Event Graphs(GTEG). These type of graphs, unlike TEG, do not admit a linear representation in (min,+) algebra. To mitigate the problem of nonlinearity, we used a modeling approach defined on a dioid operators. The obtained state model is used to evaluate the performance of GTEG. For this, we proposed a new method to linearize the mathematical model governing the dynamic evolution of the graphical model in order to obtain a linear model in (min,+) algebra. The second part of this work is devoted to the problem of determining the resources to use in a production line, in order to achieve desired performance. These is equivalent to determining the initial marking of the control part of the GTEG.

This work deals with the development and use of a graphical editor of object-oriented Petri nets implemented in the PNtalk language. First, Petri nets that expand over time are described here. They are followed by a description of the object-oriented paradigm. Next, the structure of object-oriented Petri nets in the implementation of PNtalk is described here. Further work presents a description of the application design, which shows the entire structure of the application from the perspective of views. The main motivation for creating this tool is the effort to make object-oriented Petri nets accessible to their users. The application was implemented in the JavaFX framework and the whole procedure is given in the following chapter together with testing. The result of the work is presented in the examples contained in the last chapter, which also contains detailed manuals for controlling the application. The tool in cooperation with the PNtalk server enables users to work more pleasantly with OOPN and their visual appearance.

Due to higher requirements of computational power and safety, or functional safety ofequipments intended for the use in the industrial domain, embedded systems containing areal-time operating system are still the active area of research. This thesis addresses thehardware-assisted control module that is based on the runtime model-based verificationof a target application. This subsystem is intended to increase the diagnostic coverage,particularly, the detection of the execution errors. After the specification of the architecture,the formal model is defined and implemented into hardware using FPGA technology.This thesis also discuss some other aspects and embodies new approaches in the area ofembedded flow control, e.g. the integration of the design patterns. Using the simulation,the created module was tested using the created scenarios, which follow the real programexecution record. The results suggest that the error detection time is lower than usingstandard techniques, such a watchdog.

This thesis deals with optimization problems of planning and scheduling. There are using genetic algorithms which are inspired by evolution process. Main work is familiar with the problem of planning and scheduling, genetic algorithm and Petri nets. This knowledge was used to create applications that would with the use of genetic algorithms was able to solve planning problems and the resulting plans would be represented the Time Petri Net. In conclusion of the this thesis are presented obtained results and examples of field use.

Dans cette thèse, nous analysons la dynamique de systèmes à événements discrets avec synchronisation et priorités, au moyen de réseaux de Petri et de réseaux de files d'attente.Nous appliquons cela à l'évaluation de performance d'un centre d'appels d'urgence.Notre motivation de départ est pratique. Pendant la durée de ce travail, un nouveau centre d'appels d'urgence a été mis en place pour l'agglomération parisienne, traitant les appels pour la police et les pompiers.La nouvelle organisation traite les appels en deux niveaux.Un premier niveau d'opérateurs répond aux appels, identifie les appels urgents et traite les appels non urgents.Les opérateurs de second niveau sont spécialistes (policiers ou pompiers) et traitent les demandes d'intervention.Quand un appel est identifié au niveau 1 comme très urgent, l'opérateur reste en ligne avec l'appelant jusqu'à ce qu'un opérateur de niveau 2 réponde. De plus, l'appel est prioritaire.Une conséquence de cette procédure est que, lorsqu'aucun opérateur de niveau 2 n'est disponible, les opérateurs de niveau 1 attendent avec ces appels très urgents, et la capacité du niveau 1 diminue.Nous nous intéressons à l'évaluation de performance de divers systèmes correspondant à cette description générale, dans des situations de saturation.Nous proposons trois modèles différents pour traiter ce type de systèmes.Les deux premiers sont des modèles de réseaux de Petri temporisés.Nous enrichissons les classiques réseaux de Petri à choix libres en autorisant des situations de conflit où le routage est résolu par des priorités.La principale difficulté est alors que l'opérateur de la dynamique n'est plus monotone.Dans un premier modèle, nous proposons une dynamique discrète pour cette classe de réseaux de Petri, avec des temps de séjour constants sur les places.Nous prouvons que les variables compteurs d'une exécution du réseau sont les solutions d'un système affine par morceaux, avec retards.Nous étudions les régimes stationnaires de cette dynamique, et caractérisons les régimes affines comme solutoins d'un système affine par morceaux, qui peut être vu comme un système sur le semi-corps de germes tropical (min plus).Les applications numériques montrent cependant que la convergence ne se fait pas toujours vers ces régimes stationnaires affines.Le second modèle est une transformation continue du précédent. Pour la même classe de réseaux de Petri, nous proposons une dynamique sous forme d'équations différentielles discontinues.Nous établissons l'existence et l'unicité de la solution.L'objectif de cette modélisation est d'obtenir un système plus simple dans lequel les pathologies du temps discret disparaissent. Nous montrons que les régimes stationaires sont les mêmes que ceux de la dynamique discrète. Les simulations numériques semblent montrer que la convergence s'obtient effectivement dans ce cas.Nous modélisons aussi le centre d'appels d'urgence comme un réseau de files d'attente, prenant ainsi en compte le caractère aléatoire des différentes variables du centre d'appel.Pour ce système, nous prouvons que la dynamique, après une transformation d'échelle, converge vers une limite fluide, qui correspond au système d'équations différentielles précédent.Cela conforte notre seconde modélisation.Les principaux outils de la preuve de convergence sont le calcul stochastique pour les processus de Poisson, les formulations de Skorokhod généralisées, ou encore des arguments de couplage.Ainsi, nos trois modèles d'un même centre d'appels d'urgence définissent un même comportement asymptotique schématique, décrivant différentes phases de congestion du centre.Dans une seconde partie de cette thèse, nous analysons des simulations poussées, prenant en compte les nombreux détails de notre étude de cas. Les simulations confirment le comportement schématique prédit par nos modèles mathématiques. Nous discutons aussi des interactions complexes provenant de la nature hétérogène du niveau 2. / In this thesis, we analyze the dynamics of discrete event systems with synchronization and priorities, by the means of Petri nets and queueing networks.We apply this to the performance evaluation of an emergency call center.Our original motivation is practical. During the period of this work, a new emergency call center became operative in Paris area, handling emergency calls to police and firemen.The new organization includes a two-level call treatment. A first level of operators answers calls, identifies urgent calls and handles (numerous) non-urgent calls.Second level operators are specialists (policemen or firemen) and handle emergency demands.When a call is identified at level 1 as extremely urgent, the operator stays in line with the call until a level 2 operator answers. The call has priority for level 2 operators.A consequence of this procedure is that, when level 2 operators are busy, level 1 operators wait with extremely urgent calls, and the capacity of level 1 diminishes.We are interested in the performance evaluation of various systems corresponding to this general description, in stressed situations.We propose three different models addressing this kind of systems.The first two are timed Petri net models.We enrich the classical free choice Petri nets by allowing conflict situations in which the routing is solved by priorities.The main difficulty in this situation is that the operator of the dynamics becomes non monotone.In a first model, we consider discrete dynamics for this class of Petri nets, with constant holding times on places.We prove that the counter variables of an execution of the Petri net are solutions of a piecewise linear system with delays.As far as we know, this proof is new, even for the class of free choice nets, which is a subclass of ours.We investigate the stationary regimes of the dynamics, and characterize the affine ones as solutions of a piecewise linear system, which can be seen as a system over a tropical (min-plus) semifield of germs.Numerical experiments show that, however, convergence does not always holds towards these affine stationary regimes.The second model is a ``continuization'' of the previous one. For the same class of Petri nets, we propose dynamics expressed by differential equations, so that the tokens and time events become continue.For this differential system with discontinuous righthandside, we establish the existence and uniqueness of the solution.By using differential equations, we aim at obtaining a simpler model in which discrete time pathologies disappear. We show that the stationary regimes are the same as the stationary regimes of the discrete time dynamics.Numerical experiments tend to show that, in this setting, convergence effectively holds.We also model the emergency call center described above as a queueing system, taking into account the randomness of the different call center variables.For this system, we prove that, under an appropriate scaling, the dynamics converges to a fluid limit which corresponds to the differential equations of our Petri net model.This provides support for the second model.Stochastic calculus for Poisson processes, generalized Skorokhod formulations and coupling arguments are the main tools used to establish this convergence.Hence, our three models of an identical emergency call center yield the same schematic asymptotic behavior, expressed as a piecewise linear system of the parameters, and describing the different congestion phases of the system.In a second part of this thesis, simulations are carried out and analyzed, taking into account the many subtleties of our case study (for example, we construct probability distributions based on real data analysis).The simulations confirm the schematic behavior described by our mathematical models.We also address the complex interactions coming from the heterogeneous nature of level 2.

Indiana University-Purdue University Indianapolis (IUPUI) / With the rapid growth of technology, scientists are trying to find ways to make the world a more efficient and eco-friendly place. The research and development of electric vehicles suddenly boomed since natural resource are becoming very scarce. The significance of an electric vehicle goes beyond using free energy, it is environ- mental friendly. The objective of this thesis is to understand what Vehicle to Grid Communication (V2G) for an electric vehicle is, and to implement a model of this highly efficient system into a Hybrid Petri Net. This thesis proposes a Hybrid Petri net modeling of Vehicle to Grid (V2G) Communication topology. Initially, discrete, continuous, and hybrid Petri net's are defined, familiarized, and exemplified. Secondly, the Vehicle and Grid side of the V2G communication system is introduced in detail. The modeling of individual Petri nets, as well as their combination is discussed thoroughly. Thirdly, in order to prove these systems, simulation and programming is used to validate the theoretical studies. A Matlab embedded simulation program known as SimHPN is used to simulate specific scenario's in the system, which uses Depth-first Search (DFS) Algorithm. In addition to SimHPN simulation program, Matlab program is made to output four levels of the reachability tree as well as specifying duplicate and terminate nodes. This code incorporates a technique known as Breadth-first Search (BFS) Algorithm.

No description available.