Thèses sur le sujet « Preemptive Time Petri Nets »

Bibliography: leaves 177-191. This thesis uses a new type of extended time Petri net to model and analyse command and control decision processes. A comprehensive review of existing time Petri net structures is given. This concludes with the introduction of time Petri net structure that incorporates the most commonly used time structures. This extended time Petri net structure is then used in the definition of the basic modelling blocks required to model command and control decision processes. This basic modelling block forms the basis of the direct analysis techniques that are introduced in the thesis.

Operational support as an area of process mining aims to predict the temporal performance of individual cases and the overall business process. Although seasonal effects, delays and performance trends are well-known to exist for business processes, there is up until now no prediction model available that explicitly captures this. In this paper, we introduce time series Petri net models. These models integrate the control flow perspective of Petri nets with time series prediction. Our evaluation on the basis of our prototypical implementation demonstrates the merits of this model in terms of better accuracy in the presence of time series effects.

Embedded systems are used in a wide spectrum of applications ranging from home appliances and mobile devices to medical equipment and vehicle controllers. They are typically characterized by their real-time behavior and many of them must fulfill strict requirements on reliability and correctness.

In this thesis, we concentrate on aspects related to modeling and formal verification of realtime embedded systems.

First, we define a formal model of computation for real-time embedded systems based on Petri nets. Our model can capture important features of such systems and allows their representations at different levels of granularity. Our modeling formalism has a welldefined semantics so that it supports a precise representation of the system, the use of formal methods to verify its correctness, and the automation of different tasks along the design process.

Second, we propose an approach to the problem of formal verification of real-time embedded systems represented in our modeling formalism. We make use of model checking to prove whether certain properties, expressed as temporal logic formulas, hold with respect to the system model. We introduce a systematic procedure to translate our model into timed automata so that it is possible to use available model checking ools. Various examples, including a realistic industrial case, demonstrate the feasibility of our approach on practical applications.

Nous évaluons dans cette thèse deux performances temporelles des architectures d’automatisation distribuées sur Ethernet commuté et utilisant un modèle de coopération client/serveur : Le temps de réponse entre une occurrence d’un événement d’entrée et l’occurrence de l’événement de sortie correspondant ; Le temps de cycle réeseau pour la scrutation par un contrôleur de l’ensemble de ses modules d’entrées / sorties déportées. La conjonction de trois mécanismes de consommation de temps rend ces deux performances variables et difficiles à déterminer de manière analytique. Par conséquent, la méthode proposée se base sur la simulation d’un modèle en réseau de Petri temporisé et coloré du comportement dynamique de l’architecture complète. Les résultats obtenus sur six architectures test permettent de : Montrer que les architectures multi-contrôleurs utilisant le modèle de coopération client / serveur donnent des temps de cycle réseau plus rapide que celles basées sur les modèles maître / esclave et producteur / consommateur ; Quantifier l’influence du réseau et des mécanismes de consommation du temps
In this work, two time performances of switched Ethernet automation systems that use a client/server cooperation model are evaluated : The response time from an occurrence of an input event to the occurrence of the corresponding output event ; The network cycle time for the scanning by a controller of the whole set of its remote inputs / outputs modules. The conjunction of three time consumption mechanisms makes both time performances variable and difficult to compute in an analytic fashion. Thus, the proposed method is based on simulation of a timed and coloured Petri net model of the dynamic behaviour of the whole automation architecture. The results which have been obtained on six benchmark architectures enabled us : To show that multi-controllers architectures using a client/server cooperation model provide faster network cycle times than those based on master/slave and producer/consumer models ; To quantify the influence of the time consumption mechanisms on these performances

The current thesis considers the issue of state estimation of condition systems, a form of petri net with signal inputs and outputs. In previous research the problem of unobservability due to progress confusion was identified, in the presence of which state estimation is not possible. Here we introduce the notion of Time Condition Systems", a class of condition systems that uses timing information from condition models to overcome state estimation problem caused by progress confusion. To make use of the timing information in the plant model, a procedure called Exploded Time Plant" is synthesized. This procedure makes the plant model an observable model. It is proved that this procedure does not alter the structural and temporal behavior of the plant model and the plant maintains its integrity. The time plant(s) and the corresponding Exploded time plant(s) are subsequently used to develop observer(s) and controller(s) for Time condition models.

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.

Neste trabalho e proposta a abordagem TempER-Tr, uma técnica de modelagem conceitual, fundamentada em rede de Petri, que integra a especificação das propriedades dinâmicas de um sistema a um modelo de dados temporal do tipo entidade relacionamento. Um modelo ou esquema conceitual descreve as propriedades identificadas de um sistema a ser desenvolvido. Estas propriedades podem ser classificadas em propriedades estáticas e propriedades dinâmicas As propriedades estáticas descrevem os estados que o sistema pode alcançar, enquanto que as propriedades dinâmicas descrevem as transições entre estes estados. A modelagem conceitual das propriedades estáticas é normalmente conhecida como modelagem de dados. A modelagem das propriedades dinâmicas é denominada de modelagem funcional ou comportamental. Mais especificamente, o modelo TempER-Tr é uma extensão de um trabalho anterior, conhecido como ER-Tr. No modelo ER-Tr, para descrever as propriedades estáticas de um sistema utiliza-se o modelo entidade-relacionamento convencional. No modelo TempER-Tr passa-se a adotar um modelo entidade-relacionamento temporal. Aliado a isto, uma nova linguagem de anotação, baseada em SQL, com mais poder de expressão é proposta. O modelo entidade-relacionamento convencional não possui dispositivos de modelagem capazes de especificar restrições que envolvam a associação dos objetos com o tempo, exigindo que isto se faca ao nível da modelagem das propriedades dinâmicas. Em um modelo entidade-relacionamento convencional, os conjuntos de entidades e relacionamentos apresentam apenas duas dimensões: a primeira refere-se as instâncias (linhas) e a segunda aos atributos (colunas). Em uma abordagem entidade relacionamento temporal, uma nova dimensão e acrescentada: o eixo temporal, possibilitando que as restrições temporais decorrentes da associação entre os objetos possam ser especificadas ao nível do modelo estático. Um requisito importante a ser preenchido por um modelo de dados temporal é permitir que em um mesmo diagrama seja possível associar objetos (entidades, relacionamentos ou atributos) temporalizados com objetos não temporalizados. lsto porque em sistemas de informação alguns dados precisam ser explicitamente referenciados ao tempo e outros não, ou porque não mudam com o tempo, ou porque é irrelevante ao usuário saber quando os fatos ocorreram. O modelo de dados temporal proposto neste trabalho, denominado TempER, pressupõe que todas as entidades, sejam elas temporalizadas ou não temporalizadas, apresentam uma "existência", ou seja, uma validade temporal. No caso das entidades temporalizadas esta existência é um subconjunto de pontos do eixo temporal. Em virtude disto são chamadas de entidades transitórias. Em relação as entidades não temporalizadas, e assumido que "existem sempre", ou seja, a sua validade temporal é constante, implícita e igual a todo o eixo temporal. Por isto são denominadas entidades perenes. Tanto as entidades transitórias quanto as entidades perenes, são focalizadas pelo modelo TempER através de duas perspectivas: uma intemporal e outra temporal. Através da perspectiva intemporal as entidades apresentam duas dimensões, semelhança do que ocorre em um modelo entidade-relacionamento convencional. Através da perspectiva temporal as entidades apresentam três dimensões, as duas convencionais e mais o tempo. Enquanto que o modelo de dados temporal descreve as propriedades estáticas de um sistema, o modelo comportamental, a outra face da abordagem TempER-Tr, focaliza as transações executadas no interior do sistema, em resposta a eventos que ocorrem no ambiente externo. Estas transações, quando efetivadas, provocam mudanças de estados no sistema. Entretanto, para estarem habilitadas a ocorrer, é necessário que um determinado conjunto de restrições dinâmicas sejam atendidas, o que se configura em um comportamento análogo ao de uma rede de Petri. O modelo TempER-Tr é completamente mapeável, inclusive o modelo de dados temporal, para a rede CEM, um tipo de rede de Petri de alto nível. Isto permite que a sua semântica seja formalmente especificada e possibilita o aproveitamento das características das redes de Petri.
This dissertation presents TempER-Tr approach. TempER-Tr is a conceptual modeling technique based on Petri nets that integrates the specification of the dynamic properties of system to a temporal entity-relationship data model. A model or conceptual schema describes the identified properties of a system. These properties can be classified into static and dynamic properties. The static properties describe the states that the system can reach, while the dynamic properties describe the transitions between the states. The conceptual modeling of the static properties is usually known as data modeling, while behavioral or functional modeling deals with dynamic properties. The TempER-Tr model is an extension of a model known as ER-Tr. In the ER-Tr model, the conventional entity-relationship model is used to describe the static properties of a system. In the TempER-Tr model, it is adopted a kind of temporal entityrelationship model. In addition, a new notation language is proposed, based on SQL, with more expression power. The conventional entity-relationship model doesn't provide tools to specify constraints that involve the association of objects with the time dimension, requiring that this have to be done at the dynamic properties modeling level. At the conventional entityrelationship model the entities and relationships sets present just two dimensions: the first one is related to the instance (lines) and the second to the attributes (columns). At a temporal entity-relationship approach, a new dimension is added: the time line. This way, the temporal constraints can be specified at the level of the static diagrams. An important requirement to be supplied by any temporal data model is the possibility to relate, into the same diagram, time-varying objects with time-invarying objects. This is due to the fact that in information systems some data need to be explicitly related to time and others don't, either because they don't change with time, or because users don't need to know when the facts occurred. • The temporal data model proposed in this work, nominated TempER, presupposes that all entities, being them time-varying or time-invarying, have an "existence", or a temporal validity. At the time-varying entities, named transitory entities, this existence is a subset of points from the time line. In time-invarying entities, named perennial entities, it is assumed that they "always exist", i.e., their temporal validity is constant, implicit, and equal to all points of the time line. Transitory entities, as much as perennial entities, are focused by the TempER model through two perspectives: a temporal perspective and a non-temporal perspective. Through the non-temporal perspective the entities present two dimensions - lines and columns - similar to a conventional entity-relationship model. Through the temporal perspective the entities present three dimensions: the two conventional dimensions and, in addition, the time dimension. While the temporal data model describes the static properties of a system, the behavioral model in the TempER-Tr approach focus the transactions that are executed by the system, in response to the events that occur at the external environment. A certain set of dynamic constraints must be attended so that transactions are enable to occur. This configures a behavior similar to a Petri net. The TempER-Tr model is completely mappeable, inclusive the temporal data model, to the CEM net, a kind of high level Petri net. This way, the semantic of TempER-Tr model is formally specified. In addition, the utilization of the characteristics of Petri nets is possible.

Dissertação para obtenção do Grau de Mestre em Engenharia Informática
Domain Specific Modeling (DSM) is a methodology to provide programs or system’s specification at higher level of abstraction, making use of domain concepts instead of low level programming details. To support this approach, we need to have enough expressive power in terms of those domain concepts, which means that we need to develop new languages , usually termed Domain Specific Languages (DSLs). An approach to execute specifications developed using DSLs goes by applying a model transformation technique to produce a specification in another language. These transformation techniques are applied sucessively until the specification reaches a language with an implemented run-time. The language named Concurrent Object-Oriented Petri Nets (CO-OPN) is being used successfully as a target language for such model transformation techniques. CO-OPN is an object-oriented formal language for specifying concurrent systems, that separates coordination from computational tasks. CO-OPN offers mechanisms to define the system structure and behavior, and like DSLs, relieves the developer from stipulate how that structure and behavior are attained by the underlying system. The currently available code generator for CO-OPN only produces sequential code, despite of this language potential of expressing specifications rich in concurrent behavior. The generated sequential code can be executed either in a Sequential Run-Time or in the step simulator, which is part of CO-OPN Builder IDE. The generation of sequential code turns out to be an adversity to CO-OPN application since concurrent specifications cannot be executed in parallel and therefore this languages potential is not fully exploited. This dissertation aims at filling this CO-OPN’s execution gap, through the development of a Parallel Run-Time. The new Run-Time is achieved through the adaptation of the sequential code generator and actual execution support mechanisms. In this manner, all concurrent specifications that target CO-OPN benefit from thread safe code, ready for execution in parallel and distributed environments, relieving the developer from delving into parallel programming details.By guaranteeing a safe execution environment, CO-OPN becomes an alternative to the way parallel software is nowadays developed.

Made available in DSpace on 2014-06-12T15:49:47Z (GMT). No. of bitstreams: 1 license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2009
A grande expansão do mercado de dispositivos digitais tem forçado empresas desenvolvedoras de sistemas embarcados em lidar com diversos desafios para prover sistemas complexos nesse nicho de mercado. Um dos desafios prominentes está relacionado ao consumo de energia, principalmente, devido aos seguintes fatores: (i) mobilidade; (ii) problemas ambientais; e (iii) o custo da energia. Como consequência, consideráveis esforços de pesquisa têm sido dedicados para a criação de técnicas voltadas para aumentar a economia de energia. Na última década, diversas técnicas foram desenvolvidas para reduzir o consumo de energia em sistemas embarcados. Muitos métodos lidam com gerenciamento dinâmico de energia (DPM), como, por exemplo, dynamic voltage scaling (DVS), cooperativamente com sistemas operacionais especializados, a fim de controlar o consumo de energia durante a execução do sistema. Entretanto, apesar da disponibilidade de muitos métodos de redução de consumo de energia, diversas questões estão em aberto, principalmente, no contexto de sistemas de tempo real crítico. Este trabalho propõe um método de síntese de software, o qual leva em consideração relação entre tarefas, overheads, restrições temporais e de energia. O método é composto por diversas atividades, as quais incluem: (i) medição; (ii) especificação; (iii) modelagem formal; (vi) escalonamento; e (v) geração de código. O método também é centrado no formalismo redes de Petri, o qual define uma base para geração precisa de escalas em tempo de projeto, adotando DVS para reduzir o consumo de energia. A partir de uma escala viável, um código customizado é gerado satisfazendo as restrições especificadas, e, dessa forma, garantindo previsibilidade em tempo de execução. Para lidar com a natureza estática das escalas geradas em tempo de projeto, um escalonador simples em tempo de execução é também proposto para melhorar o consumo de energia durante a execução do sistema. Diversos experimentos foram conduzidos, os quais demonstram a viabilidade da abordagem proposta para satisfazer restrições críticas de tempo e energia. Adicionalmente, um conjunto integrado de ferramentas foram desenvolvidas para automatizar algumas atividades do método de síntese de software proposto

O presente trabalho trata da verificação e design de sistemas complexos, especificamente da verificação de sistemas de tempo real concorrentes e distribuídos. Propõe-se uma técnica enumerativa para a verificação formal de modelos que permite determinar a validade de propriedades quantitativas, além das qualitativas. A técnica proposta separa a construção do espaço de estados dos algoritmos de rotulação das fórmulas temporais, o que possibilita a diminuição da complexidade do processo de verificação, tornando-o viável para aplicações práticas. A técnica proposta foi inicialmente aplicada sobre modelos de redes de Petri temporizadas e depois em uma rede unificada chamada GHENeSys para aproveitar as características de abstração, hierarquia e de elementos de interação chamados pseudo-boxes. A definição da rede GHENeSys foi modificada para permitir a modelagem de sistemas onde os requisitos temporais devem ser expressos através de atrasos e prazos como e o caso dos sistemas de tempo real. A rede suporta ainda mecanismos de refinamento tanto para os elementos ativos quanto os passivos. A demonstração da manutenção de propriedades como invariantes, vivacidade, limitação assim como da validade de fórmulas lógicas no processo de refinamento constitui um aspecto fundamental no projeto de sistemas complexos, e foi portanto revista em detalhes para a rede GHENeSys. Alguns exemplos práticos são apresentados para avaliar o desempenho dos algoritmos e um estudo de caso finaliza a apresentação, onde se pode contrastar os algoritmos propostos com os implementados na ferramenta UPPAAL.
This work deals with the process of design and verification of complex systems, mainly real time, concurrent and distributed systems. An enumerative technique is proposed for model-checking which is capable of determining both quantitative and qualitative properties. The proposed technique detach the algorithm for labeling the formula being checked from the state space construction, allowing a better result in the verification process. This model-checking approach shows itself valuable in practical applications. This approach was first applied to systems modeled by Time Petri Nets and further extended to a unified net called GHENeSys, which includes abstraction and hierarchy concepts as well as elements for data and control interchange, called pseudo-boxes. The GHENeSys definition was modified in order to deal with systems in which temporal requirements can be expressed through delays and deadlines as in the real-time systems. The GHENeSys environment supports a refinement technique applied to both passive and active elements. Net properties like invariants, liveness, boundedness and also the validity of temporal formulas was proved to be maintained through the refinement process if some conditions are satisfied. Such characteristics are useful to deal with complex systems design. Some experiments based on well known academic articles were used to avaliate the performance of the algorithms and a case study is presented in order to compare obtained results with those obtained using the UPPAAL tool.

Les systèmes temps réel doivent répondre à des contraintes d’exactitude et de sureté de fonctionnement, ce qui nécessite de pouvoir les tester. Dans ces travaux de thèse, nous proposons une méthode permettant de forcer une exécution d’un système temps réel de manière à atteindre un état choisi. Cette technique peut permettre le test de systèmes temps réel dans des situations où l’état choisi pourrait être compliqué à atteindre en ne manipulant que les données d’entrée du système. Un exemple d’application pourrait être celui d’un état déclenchant un redondant, et dont l’exécution serait peu fréquente, mais que l’on souhaite néanmoins tester. Dans ce cas d’utilisation, il s’agit effectivement de l’injection de fautes dans le système. Cette solution est basée sur une analyse hors-ligne d’un ensemble de modèles comportementaux du système, utilisant le formalisme des structures de Kripke à durée. Les modèles du système sont issu d’une démarche IDM, et présentent le comportement des tâches du point de vue du système d’exploitation temps réel. À l’aide d’une paramétrisation, transformation et composition des modèles, nous effectuons une analyse paramétrée du réseau de Petri temporel résultant. Grâce au résultat de cette analyse, nous déterminons un ensemble de délais à ajouter à l’exécution du système afin de forcer le système à atteindre l’état choisi. En utilisant un modèle embarqué des différentes tâches, et par le biais d’un contrôleur intégré au système d’exploitation temps réel, nous effectuons le forçage en ligne du système afin de permettre l’atteinte de l’état choisi, et éventuellement le test de l’exécution découlant de cet état. Ce travail de thèse détaille les formalismes utilisés pour modéliser l’application, la manière dont ils sont modifiés et analysés pour obtenir les délais d’exécution, ainsi que l’implémentation dans un système d’exploitation temps réel : TrampolineRTOS
Real-time systems must conform to requirements of correctness and safety, which requires testing them. In this thesis, we propose a method that allows to force an execution of a real-time system so as to reach a chosen state. This technique can be used to test real-time systems in situations where the chosen state could be hard to reach when dealing with the input sequence of the system alone. One example of an application could be that of a state that triggers a redundancy mechanism when reached, the execution of which would be infrequent, but that still requires testing. In this use case, it is effectively fault injection in the system. This solution is based on an offline analysis of a set of behavioral models of the system, using the formalism of durational Kripke structures. The models of the system are obtained through a Model Driven Engineering approach, and present the behaviors of the tasks from the point of view of the real-time operating system. Using a parametrization, transformation and composition of the models, we perform a parametric analysis of the resulting Time Petri net. Thanks to the result of this analysis, we establish a set of delays to be added to the execution of the system so as to reach the chosen state. With the help of an embedded model of the different tasks of the system, and through the means of a controller embedded in the real-time operating system, we perform the runtime enforcement of the system so as to make it reach the chosen state, and possibly allow for testing the execution starting from this state. This thesis details the formalisms used to model the application, the way in which the models are modified and analyzed to obtain the execution delays, as well as the implementation in a real-time operating system: TrampolineRTOS

Les systèmes temps réel (STR) sont au coeur de machines souvent jugés critiques pour la sécurité : ils en contrôlent l'exécution afin que celles-ci se comportent de manière sûre dans le contexte d'un environnement dont l'évolution peut être imprévisible. Un STR n'a d'autre alternative que de s'adapter `a son environnement : sa correction dépend des temps de réponses aux stimuli de ce dernier. Il est couramment admis que le formalisme des réseaux de Petri temporels (RdPT) est adapté à la description des STR. Cependant, la modélisation de systèmes simples, ne possédant que quelques tâches périodiques ordonnancées de façon basique se révèle être un exercice souvent complexe. En premier lieu, la modélisation efficace d'une gamme étendue de politiques d'ordonnancements se heurte à l'incapacité des RdPT à imposer un ordre d'apparition à des évènements concurrents survenant au même instant. D'autre part, les STR ont une nette tendance à être constitués de caract éristiques récurrentes, autorisant une modélisation par composants. Or les RdPT ne sont guère adaptés à une utilisation compositionnelle un tant soit peu générale. Afin de résoudre ces deux problèmes, nous proposons dans cette thèse Cifre - en partenariat entre Airbus et le Laas-Cnrs - d'étendre les RdPT à l'aide de deux nouvelles relations, les relations d'inhibition et de permission, permettant de spécifier de manière plus fine les contraintes de temps. Afin de cerner un périmètre clair d'adéquation de cette nouvelle extension à la modélisation des systèmes temps réel, nous avons défini Pola, un langage spécifique poursuivant deux objectifs : déterminer un sous-ensemble des systèmes temps réel modélisables par les réseaux de Petri temporels à inhibitions/permissions et fournir un langage simple à la communauté temps réel dont la vérification, idéalement automatique, est assurée par construction. Sa sémantique est donnée par traduction en réseaux de Petri temporels à inhibitions/permissions. L'explorateur d'espace d'états de la boite à outils Tina a été étendu afin de permettre la vérification des descriptions Pola.

The modeling and evaluation calculus FMC-QE, the Fundamental Modeling Concepts for Quanti-tative Evaluation [1], extends the Fundamental Modeling Concepts (FMC) for performance modeling and prediction. In this new methodology, the hierarchical service requests are in the main focus, because they are the origin of every service provisioning process. Similar to physics, these service requests are a tuple of value and unit, which enables hierarchical service request transformations at the hierarchical borders and therefore the hierarchical modeling. Through reducing the model complexity of the models by decomposing the system in different hierarchical views, the distinction between operational and control states and the calculation of the performance values on the assumption of the steady state, FMC-QE has a scalable applica-bility on complex systems. According to FMC, the system is modeled in a 3-dimensional hierarchical representation space, where system performance parameters are described in three arbitrarily fine-grained hierarchi-cal bipartite diagrams. The hierarchical service request structures are modeled in Entity Relationship Diagrams. The static server structures, divided into logical and real servers, are de-scribed as Block Diagrams. The dynamic behavior and the control structures are specified as Petri Nets, more precisely Colored Time Augmented Petri Nets. From the structures and pa-rameters of the performance model, a hierarchical set of equations is derived. The calculation of the performance values is done on the assumption of stationary processes and is based on fundamental laws of the performance analysis: Little's Law and the Forced Traffic Flow Law. Little's Law is used within the different hierarchical levels (horizontal) and the Forced Traffic Flow Law is the key to the dependencies among the hierarchical levels (vertical). This calculation is suitable for complex models and allows a fast (re-)calculation of different performance scenarios in order to support development and configuration decisions. Within the Research Group Zorn at the Hasso Plattner Institute, the work is embedded in a broader research in the development of FMC-QE. While this work is concentrated on the theoretical background, description and definition of the methodology as well as the extension and validation of the applicability, other topics are in the development of an FMC-QE modeling and evaluation tool and the usage of FMC-QE in the design of an adaptive transport layer in order to fulfill Quality of Service and Service Level Agreements in volatile service based environments. This thesis contains a state-of-the-art, the description of FMC-QE as well as extensions of FMC-QE in representative general models and case studies. In the state-of-the-art part of the thesis in chapter 2, an overview on existing Queueing Theory and Time Augmented Petri Net models and other quantitative modeling and evaluation languages and methodologies is given. Also other hierarchical quantitative modeling frameworks will be considered. The description of FMC-QE in chapter 3 consists of a summary of the foundations of FMC-QE, basic definitions, the graphical notations, the FMC-QE Calculus and the modeling of open queueing networks as an introductory example. The extensions of FMC-QE in chapter 4 consist of the integration of the summation method in order to support the handling of closed networks and the modeling of multiclass and semaphore scenarios. Furthermore, FMC-QE is compared to other performance modeling and evaluation approaches. In the case study part in chapter 5, proof-of-concept examples, like the modeling of a service based search portal, a service based SAP NetWeaver application and the Axis2 Web service framework will be provided. Finally, conclusions are given by a summary of contributions and an outlook on future work in chapter 6. [1] Werner Zorn. FMC-QE - A New Approach in Quantitative Modeling. In Hamid R. Arabnia, editor, Procee-dings of the International Conference on Modeling, Simulation and Visualization Methods (MSV 2007) within WorldComp ’07, pages 280 – 287, Las Vegas, NV, USA, June 2007. CSREA Press. ISBN 1-60132-029-9.
FMC-QE (Fundamental Modeling Concepts for Quantitative Evaluation [1]) ist eine auf FMC, den Fundamental Modeling Concepts, basierende Methodik zur Modellierung des Leistungsverhaltens von Systemen mit einem dazugehörenden Kalkül zur Erstellung von Leistungsvorhersagen wie Antwortzeiten und Durchsatz. In dieser neuen Methodik steht die Modellierung der hierarchischen Bedienanforderungen im Mittelpunkt, da sie der Ursprung aller dienstbasierenden Systeme sind. Wie in der Physik sind in FMC-QE die Bedienanforderungen Tupel aus Wert und Einheit, um Auftragstransformationen an Hierarchiegrenzen zu ermöglichen. Da die Komplexität durch eine Dekomposition in mehreren Sichten und in verschiedene hierarchische Schichten, die Unterscheidung von Operations- und Kontrollzuständen, sowie dazugehörige Berechungen unter Annahme der Stationarität reduziert wird, skaliert die Anwendbarkeit von FMC-QE auf komplexe Systeme. Gemäß FMC wird das zu modellierende System in einem 3-dimensionalen hierarchischen Beschreibungsraum dargestellt. Die quantitativen Kenngrößen der Systeme werden in drei beliebig frei-granularen hierarchischen bi-partiten Graphen beschrieben. Die hierarchische Struktur der Bedienanforderungen wird in Entity Relationship Diagrammen beschrieben. Die statischen Bedienerstrukturen, unterteilt in logische und reale Bediener, sind in Aufbaudiagrammen erläutert. Außerdem werden Petri Netze, genauer Farbige Zeit-behaftete Petri Netze, dazu verwendet, die dynamischen Abläufe, sowie die Kontrollflüsse im System zu beschreiben. Anschließend wird eine Menge von hierarchischen Gleichungen von der Struktur und den Parametern des Modells abgeleitet. Diese Gleichungen, die auf dem stationären Zustand des Systems beruhen, basieren auf den beiden Fundamental Gesetzen der Leistungsanalyse, dem Gesetz von Little und dem Verkehrsflussgesetz. Das Gesetz von Little definiert hierbei Beziehungen innerhalb einer hierarchischen Schicht (horizontal) und das Verkehrsflussgesetz wiederum Beziehungen zwischen hierarchischen Schichten (vertikal). Die Berechungen erlauben Leistungsvorhersagen für komplexe Systeme durch eine effiziente Berechnung von Leistungsgrößen für eine große Auswahl von System- und Lastkonfigurationen. Innerhalb der Forschungsgruppe von Prof. Dr.-Ing Werner Zorn am Hasso Plattner Institut an der Universität Potsdam ist die vorliegende Arbeit in einen größeren Forschungskontext im Bereich FMC-QE eingebettet. Während hier ein Fokus auf dem theoretischen Hintergrund, der Beschreibung und der Definition der Methodik als auch der Anwendbarkeit und Erweiterung gelegt wurde, sind andere Arbeiten auf dem Gebiet der Entwicklung einer Anwendung zur Modellierung und Evaluierung von Systemen mit FMC-QE bzw. der Verwendung von FMC-QE zur Entwicklung einer adaptiven Transportschicht zur Einhaltung von Dienstgüten (Quality of Service) und Dienstvereinbarungen (Service Level Agreements) in volatilen dienstbasierten Systemen beheimatet. Diese Arbeit umfasst einen Einblick in den Stand der Technik, die Beschreibung von FMC-QE sowie die Weiterentwicklung von FMC-QE in repräsentativen allgemeinen Modellen und Fallstudien. Das Kapitel 2: Stand der Technik gibt einen Überblick über die Warteschlangentheorie, Zeit-behaftete Petri Netze, weitere Leistungsbeschreibungs- und Leistungsvorhersagungstechniken sowie die Verwendung von Hierarchien in Leistungsbeschreibungstechniken. Die Beschreibung von FMC-QE in Kapitel 3 enthält die Erläuterung der Grundlagen von FMC-QE, die Beschreibung einiger Grundannahmen, der graphischen Notation, dem mathematischen Modell und einem erläuternden Beispiel. In Kapitel 4: Erweiterungen von FMC-QE wird die Behandlung weiterer allgemeiner Modelle, wie die Modellklasse von geschlossenen Netzen, Synchronisierung und Mehrklassen-Modelle beschrieben. Außerdem wird FMC-QE mit dem Stand der Technik verglichen. In Kapitel 5 werden Machbarkeitsstudien beschrieben. Schließlich werden in Kapitel 6 eine Zusammenfassung und ein Ausblick gegeben. [1] Werner Zorn. FMC-QE - A New Approach in Quantitative Modeling. In Hamid R. Arabnia, editor, Proceedings of the International Conference on Modeling, Simulation and Visualization Methods (MSV 2007) within WorldComp ’07, 280 – 287, Las Vegas, NV, USA, Juni 2007. CSREA Press. ISBN 1-60132-029-9.

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.

This work is devoted to the issue of monitoring of distributed real-time systems. In particular, it focuses on formal aspects of model-based supervision and problems which are related to it. In its first part, we present the basic properties of two well-known formal models used to model distributed systems: networks of timed automata and time Petri nets. We show that the behavior of these models can be represented with so-called branching processes. We also introduce the key conceptual elements of the supervisory system. The second part of the work is dedicated to the issue of constrained unfoldings which enable us to track causal relationships between events in a distributed system. This type of structure can be used to reproduce processes of the system on the basis of a completely unordered set of previously observed events. Moreover, we show that time constraints imposed on a system and observations submitted to the supervisory system can significantly affect a course of events in the system. We also raise the issue of parameters in time constraints. The proposed methods are illustrated with case studies. The third part of the work deals with the issue of unobservable cyclical behaviors in distributed systems. This type of behaviors leads to an infinite number of events in constrained unfoldings. We explain how we can obtain a finite structure that stores information about all observed events in the system, even if this involves processes that are infinite due to such unobservable loops. The fourth and final part of the work is dedicated to implementation issues of the previously described methods.

This thesis is concerned with the modeling and the analysis of distributedreal-time systems. In distributed systems, components evolve partlyindependently: concurrent actions may be performed in any order, withoutinfluencing each other and the state reached after these actions does notdepends on the order of execution. The time constraints in distributed real-timesystems create complex dependencies between the components and the events thatoccur. So far, distributed real-time systems have not been deeply studied, andin particular the distributed aspect of these systems is often left aside. Thisthesis explores distributed real-time systems. Our work on distributed real-timesystems is based on two formalisms: time Petri nets and networks of timedautomata, and is divided into two parts.In the first part, we highlight the differences between centralized anddistributed timed systems. We compare the main formalisms and their extensions,with a novel approach that focuses on the preservation of concurrency. Inparticular, we show how to translate a time Petri net into a network of timedautomata with the same distributed behavior. We then study a concurrency relatedproblem: shared clocks in networks of timed automata can be problematic when oneconsiders the implementation of a model on a multi-core architecture. We showhow to avoid shared clocks while preserving the distributed behavior, when thisis possible.In the second part, we focus on formalizing the dependencies between events inpartial order representations of the executions of Petri nets and time Petrinets. Occurrence nets is one of these partial order representations, and theirstructure directly provides the causality, conflict and concurrency relationsbetween events. However, we show that, even in the untimed case, some logicaldependencies between event occurrences are not directly described by thesestructural relations. After having formalized these logical dependencies, wesolve the following synthesis problem: from a formula that describes a set ofruns, we build an associated occurrence net. Then we study the logicalrelations in a simplified timed setting and show that time creates complexdependencies between event occurrences. These dependencies can be used to definea canonical unfolding, for this particular timed setting.

Le but de ce rapport est de présenter une méthode globale de développement à partir de spécifications informelles, depuis la modélisation graphique des exigences temporelles d'un système ferroviaire critique jusqu'à une implantation systématique au moyen de méthodes formelles. Nous proposons d'utiliser ici les réseaux de Petri temporels pour décrire le comportement attendu du logiciel de contrôle-commande à construire.Tout d'abord nous construisons un modèle des exigences p-temporel prenant en compte toutes les contraintes que doit vérifier le système. Nous proposons des outils et des méthodes capables de valider et de vérifier ce modèle. Ensuite, il s'agit de construire un modèle de processus solution en réseau de Petri t-temporel. Ce modèle illustre des exigences techniques relatives à un choix technologique ou architectural. L'objectif est double : tout d'abord il est nécessaire de vérifier la traçabilité des exigences ; ensuite, il faut vérifier que l'ensemble des exigences sources sont bien implémentées dans la solution préconisée et dans sa mise en oeuvre. Enfin, nous proposons une approche visant à transformer de façon systématique le modèle de processus en machine abstraite $B$ afin de poursuivre une procédure formelle $B$ classique. Finalement, le cas d'étude du passage à niveau, composant critique dans le domaine de la sécurité ferroviaire est décrit
The introduction of new European standards for railway safety, coupled with an increasing use of software technology changes the method of development of critical railway systems. Indeed, new systems have to be at least as good as the previous ones. Therefore the appropriate safety level of critical systems has to be proved in order to obtain the necessary approval from the authorities. Accordingly a high level of reliability and correctness must be reached by the use of mathematical proofs and then formal methods. We focus on the treatment of the temporal requirements in the level crossing case study which is modelled with p-time Petri nets, and on the translation of this model in a more formal way by using the B method. This paper introduces a methodology to analyse the safety of timed discrete event systems. First, our goal is to take out the forbidden state highlighted by a p-time Petri net modelling. This model deals with the requirements of the considered system and has to contain all the constraints that have to be respected. Then we aim at describing a process identified as a solution of the system functioning. This method consists in exploring all the possible behaviours of the system by means of the construction of state classes. Finally, we check if the proposed process corresponds to the requirements model previously built.Our case-study is the level crossing, a critical component for the safety of railway systems

Ce travail s’inscrit dans le cadre d’étude de la sûreté de fonctionnement.

La sûreté de fonctionnement est progressivement devenue partie intégrante de l’évaluation des performances des systèmes industriels. En effet, les pannes d’équipements, les pertes de production consécutives, et la maintenance des installations ont un impact économique majeur dans les entreprises. Il est donc essentiel pour un manager de pouvoir estimer de manière cohérente et réaliste les coûts de fonctionnement de l’entreprise, en tenant notamment compte des caractéristiques fiabilistes des équipements utilisés, ainsi que des coûts induits entre autres par le non-fonctionnement du système et la restauration des performances de ses composants après défaillance.

Le travail que nous avons réalisé dans le cadre de ce doctorat se concentre sur un aspect particulier de la sûreté de fonctionnement, à savoir les politiques de remplacement d’équipements basées sur la fiabilité des systèmes qu’ils constituent. La recherche menée part de l’observation suivante :si la littérature consacrée aux politiques de remplacement est abondante, elle repose généralement sur l’hypothèse implicite que les nouveaux équipements envisagés présentent les mêmes caractéristiques et performances que celles que possédaient initialement les composants objets du remplacement.

La réalité technologique est souvent bien différente de cette approche, quelle que soit la discipline industrielle envisagée. En effet, de nouveaux équipements sont régulièrement disponibles sur le marché ;ils assurent les mêmes fonctions que des composants plus anciens utilisés par une entreprise, mais présentent de meilleures performances, par exemple en termes de taux de défaillance, consommation d’énergie, " intelligence " (aptitude à transmettre des informations sur leur état de détérioration).

De plus, il peut devenir de plus en plus difficile de se procurer des composants de l’ancienne génération pour remplacer ceux qui ont été déclassés. Cette situation est généralement appelée obsolescence technologique.

Le but de ce travail est de prolonger et d’approfondir, dans le cadre de la sûreté de fonctionnement, les réflexions engagées par les différents articles présentés dans la section état de l’art afin de définir et de modéliser des stratégies de remplacements d’équipements soumis à obsolescence technologique. Il s’agira de proposer un modèle, faisant le lien entre les approches plus économiques et celles plus fiabilistes, permettant de définir et d’évaluer l’efficacité, au sens large, des différentes stratégies de remplacement des unités obsolètes. L’efficacité d’une stratégie peut se mesurer par rapport à plusieurs critères parfois contradictoires. Parmi ceux-ci citons, évidemment, le coût total moyen engendré par la stratégie de remplacement, seul critère considéré dans les articles cités au chapitre 2, mais aussi la façon dont ces coûts sont répartis au cours du temps tout au long de la stratégie, la variabilité de ces coûts autour de leur moyenne, le fait de remplir certaines conditions comme par exemple d’avoir remplacé toutes les unités d’une génération par des unités d’une autre génération avant une date donnée ou de respecter certaines contraintes sur les temps de remplacement.

Pour arriver à évaluer les différentes stratégies, la première étape sera de définir un modèle réaliste des performances des unités considérées, et en particulier de leur loi de probabilité de défaillance. Etant donné le lien direct entre la probabilité de défaillance d’un équipement et la politique de maintenance qui lui est appliquée, notamment la fréquence des maintenances préventives, leur effet, l’effet des réparations après défaillance ou les critères de remplacement de l’équipement, un modèle complet devra considérer la description mathématique des effets des interventions effectuées sur les équipements. On verra que la volonté de décrire correctement les effets des interventions nous a amené à proposer une extension des modèles d’âge effectif habituellement utilisés dans la littérature.

Une fois le modèle interne des unités défini, nous développerons le modèle de remplacement des équipements obsolètes proprement dit.

Nous appuyant sur la notion de stratégie K proposée dans de précédents travaux, nous verrons comment adapter cette stratégie K à un modèle pour lequel les temps d’intervention ne sont pas négligeables et le nombre d’équipes limité. Nous verrons aussi comment tenir compte dans le cadre de cette stratégie K d’une part des contraintes de gestion d’un budget demandant en général de répartir les coûts au cours du temps et d’autre part de la volonté de passer d’une génération d’unités à l’autre en un temps limité, ces deux conditions pouvant être contradictoires.

Un autre problème auquel on est confronté quand on parle de l’obsolescence technologique est le modèle d’obsolescence à adopter. La manière dont on va gérer le risque d’obsolescence dépendra fortement de la manière dont on pense que les technologies vont évoluer et en particulier du rythme de cette évolution. Selon que l’on considère que le temps probable d’apparition d’une nouvelle génération est inférieur au temps de vie des composants ou supérieur à son temps de vie les solutions envisagées vont être différentes. Lors de deux applications numériques spécifiques.

Nous verrons au chapitre 12 comment envisager le problème lorsque l’intervalle de temps entre les différentes générations successives est largement inférieur à la durée de vie des équipements et au chapitre 13 comment traiter le problème lorsque le délai entre deux générations est de l’ordre de grandeur de la durée de vie des équipements considérés.

Le texte est structuré de la manière suivante :Après une première partie permettant de situer le contexte dans lequel s’inscrit ce travail, la deuxième partie décrit le modèle interne des unités tel que nous l’avons utilisé dans les différentes applications. La troisième partie reprend la description des stratégies de remplacement et des différentes applications traitées. La dernière partie permet de conclure par quelques commentaires sur les résultats obtenus et de discuter des perspectives de recherche dans le domaine.

Doctorat en Sciences de l'ingénieur
info:eu-repo/semantics/nonPublished

Preemptive Time Petri Nets (pTPNs) support modeling and analysis of concurrent timed software components running under fixed priority preemptive scheduling. The model is supported by a well established theory based on symbolic state-space analysis through Difference Bounds Matrix (DBM), with specific contributions on compositional modularization, trace analysis, and efficient over-approximation and clean-up in the management of suspension deriving from preemptive behavior. The aim of this dissertation is to devise and implement a framework that brings the theory to application. To this end, the theory is cast into an organic tailoring of design, coding, and testing activities within a V-Model software life cycle in respect of the principles of regulatory standards applied to the construction of safety-critical software components. To implement the toolchain subtended by the overall approach into a Model Driven Development (MDD) framework, the theory of state-space analysis is complemented with methods and techniques supporting semi-formal specification and automated compilation into pTPN models and real-time code, measurement-based Execution Time estimation, test-case selection and sensitization, coverage evaluation.

碩士
國立交通大學
資訊科學學系
86
In this thesis, we present an extended fuzzy Petri net model to model fuzzy IF-THEN rules and fuzzy IF-THEN-ELSE rules of rule- based systems. We also develop an efficient algorithm for performing vague reasoning automatically based on the extended fuzzy Petri net model. The proposed algorithm allows the computers to perform reasoning in a more flexible and more intelligent manner. Based on the proposed vague reasoning algorithm, we have implemented a vague reasoning system on a Pentium PC for performing vague reasoning automatically. Furthermore, we propose a method to describe the relationships between states and events for temporal knowledge representation and reasoning using time Petri nets. We also propose an algorithm to infer the consistency of the temporal knowledge based on the time Petri nets. Based on the proposed temporal reasoning algorithm, we have implemented a temporal reasoning system on a Pentium PC to check the consistency of the temporal knowledge.

Effective command and control is crucial to both military and non-military environments. Accurate representations of the processes associated with the inter and intra activities of nodes or agencies of such systems is essential in the analysis of command and control. One of the most important things is to be able to model the decision processes. These are the parts of the system that make decisions and then guide the direction of other elements in the system overall. This thesis uses a new type of extended time Petri net to model and analyse command and control decision processes. A comprehensive review of existing time Petri net structures is given. This concludes with the introduction of a time Petri net structure that incorporates the most commonly used time structures. This extended time Petri net structure is then used in the definition of the basic modelling blocks required to model command and control decision processes. This basic modelling block forms the basis of the direct analysis techniques that are introduced in the thesis. Due to the transient nature of the systems being modelled and the measures of interest a new type of measure is introduced, the mean conditional first hitting reward. This measure does not currently appear to be part of the stochastic process literature. Explicit procedures are given to determine the hitting probabilities and mean conditional first hitting reward for decision process models and discrete, continuous and semi-Markov chains. Finally the some extensions of the decision process sub-class are considered.
Thesis (Ph.D.) - University of Adelaide, Dept. of Applied Mathematics, 2001

碩士
國立暨南國際大學
資訊管理學系
91
Among the increasingly widespread e-commerce protocols, RosettaNet is developed initially to support the specific electronic industry domain, especially for their vertical collaborative integration of the entire supply chain of electronic products. RosettaNet provides a complete and easy way to build a platform for electronic business document exchange. Similar to other communication protocols, RosettaNet is subject to protocol verification problems, like issues of liveness. However, there are neither research efforts devoted to these problem nor any solid results to resolve them. There are risks and difficulties incurred during the implementation of RosettaNet without any protocol verification scheme applied. RosettaNet PIPs (Partner Interface Processes) are XML-based dialogs that are specially designed for system-to-system information exchange of business processes between trading partners. In each PIP specification, there define a business process with the choreography of the message dialog, and a business document with the vocabulary. Although, RosettaNet PIPs intend to provide open e-commerce standards for automated information excess and exchange across the boundaries of individual companies, some of their pilot implementations, however, faced fierce obstacles and difficulties. Most of them are caused by the inability to handle exceptional conditions. For instance, consider a situation when a buyer places a purchase order to a seller. The buyer first sends a business document to the seller. Complying to the PIPs specifications, the seller side has to return an acknowledgement to the buyer side after receiving the purchase order. Assume that due to some unexpected noises during data transferring, this message of acknowledgement were lost. According to the PIPs, the buyer side has to resend the business document to at most three times and resume its state at being executing after then. One problem arises with the question whether the seller does receive the purchase order, but the buyer doesn't receive the confirmation of the purchase order. Such ambiguities impose difficulties and burdens on system testing activities. This paper deals with the verification problem of RosettaNet. The PIPs Specifications are first modeled with time Petri nets. Time Petri nets allow an explicit modeling of concurrency and parallelism and have been widely used in real-time system specification and verification. Behavioral specification models can be automatically translated into a state transition graph, from which properties such as deadlock and reachability become explicit. The correctness of the time Petri nets models is then verified to ensure the capability of deadlock-free, auto-repairing implementations of RosettaNet applications. Ideas of the deadlock detection mechanism to check the possible existence of an uncontrolled siphon are adopted. We then extend the models to complete the RosettaNet PIPs specifications at both the sender and receiver counterparts.

碩士
國立臺灣大學
電機工程學系
85
Petri nets, a useful model for concurrent systems, lack the notion of time which is critical in modeling real-time systems. Thus, Petri nets, in general, are not appropriate for modeling systems on which timing constraints are imposed. Several timed versions of Petri nets have been proposed in theliterature, incorporating timing information into the Petri net model either implicitly or explicitly. Among such extended Petri nets, clocked Petri nets associate each transition with a set of clockconstraints and/or clock reset operations.After we associate timing information with the transitions of thePetri net we can use this enhanced model to effectively model real- time systems. However,since a system's configuration must now include timing information, both the state space and the system complexity increase significantly.To reduce the complexity, weuse the concept of Stubborn set introduced by Antti Valmari. The intuition behind stubborn sets is simply that in each of the reachable states, only portion of the next states will be explored,resulting in a reduced state space. Aside from the above analytical aspect of clocked Petri nets,in this thesis we also implement a Time-Warp distributedsimulator on a distributed shared memory system for simple timedPetri nets. Our empirical results reveal how the "partition" issue affects the performance of our simulation.

Indiana University-Purdue University Indianapolis (IUPUI)
In the healthcare industry, several modern patient identification and patient matching systems have been introduced. Most of these implement patient identification by their first, middle and last names. They also use Social Security Number and other similar national identifiers. These methods may not work for many developing and underdeveloped countries where identifying a patient is a challenge with highly redundant and interchangeable first and last names of the patient, this is aggravated by the absence of a national identification system. In order to make the patient identification more efficient, Muzima, an interface of OpenMRS (Open source medical records system) introduced an additional identifier, fingerprint, through a module to the system. Ordinary and Time Petri nets are used to analyze this module. Chapter 1 introduces Muzima fingerprint module and describes the workflow of this interface followed by the related work, importance and applications of Petri nets. Chapter 2 introduces Ordinary and Time Petri nets using examples. Chapter 3 discusses about the mathematical modeling of the Muzima Fingerprint module using Petri nets. Chapter 4 explains the qualitative and quantitative analysis done on the Muzima fingerprint module. Chapter 5 discusses about the programming and simulation done to prove the theoretical results obtained. Chapter 6 provides the conclusion and future work for the thesis.

In Canada, access to magnetic resonance imaging (MRI) examination is limited with an outcome of long patient waiting time. It is reported that the current median waiting time for MRI examination in Saskatoon is almost double the target for waiting time, which may aggravate the disease. This research is towards reducing the waiting time of patients for MRI examination in Canada by applying an improved management. As a first step of this effort, a comprehensive model of MRI booking and serving system is needed. The city of Saskatoon was taken as an example and the MRI booking and serving system in the city was studied. The common tools (queuing theory, system dynamics (SD) and discrete event dynamics simulation (DES)) were compared and it is found that DES is more suitable, in particular Petri nets (PNs), deemed to be the best choice for the purpose of this thesis. The model in this research was constructed on the basis of Hierarchical Coloured Petri nets (HCPNs), a combination of two extended PNs: Coloured PNs (CPNs) and Hierarchical PNs (HPNs). The model is able to simulate and predict patients' waiting times. Given that the structure of the model developed by HCPNs is still too complex, two extensions to CPNs, Ordered CPNs (OCPNs) and Prioritized HCPNs (PHCPNs), were proposed in this study to reduce the complexity of the model. Validation of the model was performed using the data of Saskatoon Health Region - Royal University Hospital. The results have shown that the proposed model can effectively describe the real system. The model has potential applications in decision-making for the selection of an optimal booking strategy to shorten waiting time and in the prediction of possible waiting time of the system in the future, which may assist MRI administrators in the management of medical resources and may greatly improve the quality of MRI service.

Indiana University-Purdue University Indianapolis (IUPUI)
Yan, Jiaxiang. M.S.E.C.E., Purdue University, May 2013. Modeling, Monitoring and Optimization of Discrete Event Systems Using Petri Nets. Major Professor: Lingxi Li. In last decades, the research of discrete event systems (DESs) has attracts more and more attention because of the fast development of intelligent control strategies. Such control measures combine the conventional control strategies with discrete decision-making processes which simulate human decision-making processes. Due to the scale and complexity of common DESs, the dedicated models, monitoring methods and optimal control strategies for them are necessary. Among various DES models, Petri nets are famous for the advantage in dealing with asynchronous processes. They have been widely applied in intelligent transportation systems (ITS) and communication technology in recent years. With encoding of the Petri net state, we can also enable fault detection and identification capability in DESs and mitigate potential human errors. This thesis studies various problems in the context of DESs that can be modeled by Petri nets. In particular, we focus on systematic modeling, asynchronous monitoring and optimal control strategies design of Petri nets. This thesis starts by looking at the systematic modeling of ITS. A microscopic model of signalized intersection and its two-layer timed Petri net representation is proposed in this thesis, where the first layer is the representation of the intersection and the second layer is the representation of the traffic light system. Deterministic and stochastic transitions are both involved in such Petri net representation. The detailed operation process of such Petri net representation is stated. The improvement of such Petri net representation is also provided with comparison to previous models. Then we study the asynchronous monitoring of sensor networks. An event sequence reconstruction algorithm for a given sensor network based on asynchronous observations of its state changes is proposed in this thesis. We assume that the sensor network is modeled as a Petri net and the asynchronous observations are in the form of state (token) changes at different places in the Petri net. More specifically, the observed sequences of state changes are provided by local sensors and are asynchronous, i.e., they only contain partial information about the ordering of the state changes that occur. We propose an approach that is able to partition the given net into several subnets and reconstruct the event sequence for each subnet. Then we develop an algorithm that is able to reconstruct the event sequences for the entire net that are consistent with: 1) the asynchronous observations of state changes; 2) the event sequences of each subnet; and 3) the structure of the given Petri net. We discuss the algorithmic complexity. The final problem studied in this thesis is the optimal design method of Petri net controllers with fault-tolerant ability. In particular, we consider multiple faults detection and identification in Petri nets that have state machine structures (i.e., every transition in the net has only one input place and one output place). We develop the approximation algorithms to design the fault-tolerant Petri net controller which achieves the minimal number of connections with the original controller. A design example for an automated guided vehicle (AGV) system is also provided to illustrate our approaches.

Indiana University-Purdue University Indianapolis (IUPUI)
In recent years, there have been a lot of technology innovations to automate the day to day processes done by every person. These days the automobile manufacturers introduce new features in their cars, in order to improve customer experience, like Adaptive cruise control, Parallel park assist, etc. The objective of this thesis is to model an automated parallel parking system and to simulate the system behavior, by taking into account the high level events which happen when a car is parallel parked. The tool used in this thesis to model and simulate the system is Hybrid Petri net (HPN), which is versatile to model the real life systems. Chapter 1 deals with a brief introduction of the related work in Hybrid Petri net modeling of real life systems, automatic parallel parking systems and how the concept for modeling the parallel parking system was developed. Chapter 2 deals with the general introduction about Discrete, Continuous and Hybrid Petri nets and their dynamics which are essential for understanding this thesis. Chapter 3 deals with the development of the model and the various stages in the model development. Errors encountered in each stage is briefly discussed and the improvements are discussed in the next stage of development. This chapter concludes with the final integrated model and operation of the model. Chapter 4 deals with the discussion of results obtained when the model is tested in MATLAB and SIMHPN (which is a Matlab embedded simulation program). The results are compared, the system behavior is observed and the purpose of the thesis is justified. In Chapter 5, a conclusion is provided to summarize the entire thesis.

Indiana University-Purdue University Indianapolis (IUPUI)
In recent decades, Petri nets (PNs) have been used to model traffic networks for different purposes, such as signal phase control, routing, and traffic flow estimation, etc. Because of the complex nature of traffic networks where both discrete and continuous dynamics come into play, the Hybrid Petri net (HPN) model becomes an important tool for the modeling and analysis of traffic networks. In Chapter 1 a brief historical summery about traffic systems control and then related work is mentioned followed by the major contributions in this research. Chapter 2 provides a theoretical background on Petri nets. In Chapter 3, we develop a HPN model for a single signalized intersection first, then we extend this model to study a simple traffic network that consists of two successive intersections. Time delays between different points of network are also considered in order to make the model suitable for analysis and simulation. In addition to HPN models, we also consider discrete Petri nets where their modeling simplicity enables the characterization of the occurrences of all events in the system. This discrete PN is particularly useful to give a higher-level representation of the traffic network and study its event occurrences and correlations. In Chapter 4, we build a discrete PN model to represent a traffic network with two successive intersections. However, we find that the model leads to unbounded places which cannot accurately reflect the dynamics of the traffic in terms of event occurrences. Hence, we introduce the Modified Binary Petri nets (MBPN) to overcome the limitation and resolve the confliction problem when we design our controllers. This MBPN model is a powerful tool and can be useful for the modeling and analysis of many other applications in traffic networks. Chapter 5 gives a summary for each chapter, provides conclusion and discusses future work for both discrete and hybrid Petri nets.

The thesis describes the research that has been carried out in order to reduce the limitations of current analysis techniques for non-Markovian models, which led to a three-fold contribution. The first contribution is a technique that allows to integrate different analysis techniques for the evaluation of kernels of a MRGP. Specifically, the state space of the underlying timed model is analyzed to identify epochs between regenerations and apply distinct methods for their analysis depending on the locally satisfied conditions. For epochs not amenable to existing methods, an adaptive approximation of kernel entries based on partial exploration of the state space is proposed, leveraging heuristics that permit to reduce the error on transient probabilities. This approach extends the class of models that can be analyzed, reduces errors committed by approximate analysis and allows one to automatize the selection of the analysis technique. The second contribution is a technique for the computations of the equilibrium probability density functions (PDFs) for the continuous component of the state in MRGP. Equilibrium PDFs are derived as closed-form analytical expressions by applying the Key Renewal Theorem to stochastic state classes computed between regenerations. This techniques provides a basis to analyze system properties from the equilibrium such as survivability. The last contribution, is an extension of the analysis of hierarchical semi-Markov processes with parallel regions, a technique that evaluates steady-state probabilities of models with multiple concurrent non-Markovian timers in a compositional way without the need of full state space generation. Specifically, the technique has been extended by removing some of its limitations and increasing its modeling power. By applying the time advancement mechanism known from stochastic state classes, exits in parallel regions with different time origins can be taken into account. Furthermore, exits can be put on state borders such that the model evolution depends on the exited region and a concept for history states is also presented. This significantly increases modeling power, such that the gap between semi-Markov processes with restricted modeling power and non-Markovian models without modeling restrictions but also with less efficient analysis is filled.

Hierarchical Scheduling (HS) techniques achieve resource partitioning among a set of Real-Time Applications, providing reduction of complexity, confinement of failure modes, and temporal isolation among system applications. This facilitates compositional analysis for architectural verification and plays a crucial role in all industrial areas where highperformance microprocessors allow growing integration of multiple applications on a single platform. We propose a compositional approach to formal specification and schedulability analysis of Real-Time Applications running under a Time Division Multiplexing (TDM) Global Scheduler and preemptive Fixed Priority (FP) Local Schedulers, according to the ARINC-653 standard. As a characterizing trait, each application is made of periodic, sporadic, and jittering tasks with offsets, jitters, and non-deterministic Execution Times, encompassing intra-application synchronizations through semaphores and mailboxes and inter-application communications among periodic tasks through message passing. The approach leverages the assumption of a TDM partitioning to enable compositional design and analysis based on the model of preemptive Time Petri Nets (pTPNs), which is expressly extended with a concept of Required Interface (RI) that specifies the embedding environment of an application through sequencing and timing constraints. This enables exact verification of intra-application constraints and approximate but safe verification of inter-application constraints. Experimentation illustrates results and validates their applicability on two challenging workloads in the field of safety-critical avionic systems.