Sistemas Reativos caracterizam-se por reagir continuamente a estímulos externos e internos e controlar atividades humanas. A ocorrência de falhas nesses sistemas pode resultar em grandes prejuízos. Dessa forma, o uso de métodos e técnicas rigorosas para a especificação do comportamento desse tipo de sistema é essencial, buscando-se evitar inconsistências e ambigüidades no modelo. Redes de Petri é uma das técnicas que têm sido usadas para a especificação de sistemas reativos. Teste e validação são atividades essenciais na produção dessa classe de sistemas. Por isso, o critério Análise de Mutantes, um critério de teste baseado em erros normalmente aplicado ao teste de programas, tem sido explorado no contexto de teste de especificações de sistemas reativos. É necessário o desenvolvimento de ferramentas que apóiem sua utilização, visto que a aplicação manual do critério é impraticável. O objetivo deste trabalho é a implementação da ferramenta Proteum-RS/PN, que apóia a aplicação do critério Análise de Mutantes para validar especificações baseadas em Redes de Petri. / Reactive Systems are characterized by continuously reacting to external as well as internal stimuli and controlling human activities. In these systems, faults can result in large losses. The use of rigorous methods and techniques for the specification of their behavior is essential to avoid inconsistencies and ambiguities. Petri Nets have been used for reactive-system specification. The test and validation of the underlying model are essential activities for the production of such systems. Thus, the Mutant Analysis -- a fault-based criterion usually used for program testing -- has been explored in the context of specification testing. The development of tools to support its application is necessary, since its manual application is unrealistic. The objective of this work is the implementation of Proteum-RS/PN, a testing tool which supports the application of Mutant Analysis criterion to validate Petri-Nets based specifications.

Los lenguajes concurrentes est an cada d a m as presentes en nuestra sociedad, tanto en las nuevas tecnolog as como en los sistemas utilizados de manera cotidiana. M as a un, dada la actual distribuci on de los sistemas y su arquitectura interna, cabe esperar que este hecho siga siendo una realidad en los pr oximos a~nos. En este contexto, el desarrollo de herramientas de apoyo al desarrollo de programas concurrentes se vuelve esencial. Adem as, el comportamiento de los sistemas concurrentes es especialmente dif cil de analizar, por lo que cualquier herramienta que ayude en esta tarea, a un cuando sea limitada, ser a de gran utilidad. Por ejemplo, podemos encontrar herramientas para la depuraci on, an alisis, comprobaci on, optimizaci on, o simpli caci on de programas. Muchas de ellas son ampliamente utilizadas por los programadores hoy en d a. El prop osito de esta tesis es introducir, a trav es de diferentes lenguajes de programaci on concurrentes, t ecnicas de an alisis que puedan ayudar a mejorar la experiencia del desarrollo y publicaci on de software para modelos concurrentes. En esta tesis se introducen tanto an alisis est aticos (aproximando todas las posibles ejecuciones) como din amicos (considerando una ejecuci on en concreto). Los trabajos aqu propuestos di eren lo su ciente entre s para constituir ideas totalmente independientes, pero manteniendo un nexo com un: el hecho de ser un an alisis para un lenguaje concurrente. Todos los an alisis presentados han sido de nidos formalmente y se ha probado su correcci on, asegurando que los resultados obtenidos tendr an el grado de abilidad necesario en sistemas que lo requieran, como por ejemplo, en sistemas cr ticos. Adem as, se incluye la descripci on de las herramientas software que implementan las diferentes ideas propuestas. Esto le da al trabajo una utilidad m as all a del marco te orico, permitiendo poner en pr actica y probar con ejemplos reales los diferentes an alisis. Todas las ideas aqu presentadas constituyen, por s mismas, propuestas aplicables en multitud de contextos y problemas actuales. Adem as, individualmente sirven de punto de partida para otros an alisis derivados, as como para la adaptaci on a otros lenguajes de la misma familia. Esto le da un valor a~nadido a este trabajo, como bien atestiguan algunos trabajos posteriores que ya se est an bene ciando de los resultados obtenidos en esta tesis. / Concurrent languages are increasingly present in our society, both in new technologies and in the systems used on a daily basis. Moreover, given the current systems distribution and their internal architecture, one can expect that this remains so in the coming years. In this context, the development of tools to support the implementation of concurrent programs becomes essential. Futhermore, the behavior of concurrent systems is particularly difficult to analyse, so that any tool that helps in this task, even if in a limited way, will be very useful. For example, one can find tools for debugging, analysis, testing, optimisation, or simplification of programs, which are widely used by programmers nowadays. The purpose of this thesis is to introduce, through various concurrent programming languages, some analysis techniques that can help to improve the experience of the software development and release for concurrent models. This thesis introduces both static (approximating all possible executions) and dynamic (considering a specific execution) analysis. The topics considered here differ enough from each other to be fully independent. Nevertheless, they have a common link: they can be used to analyse properties of a concurrent programming language. All the analyses presented here have been formally defined and their correctness have been proved, ensuring that the results will have the reliability degree which is needed for some systems (for instance, for critical systems). It also includes a description of the software tools that implement the different ideas proposed. This gives the work a usefulness well beyond the theoretical aspect, allowing us to put it in practice and to test the different analyses with real-world examples All the ideas here presented are, by themselves, approaches that can be applied in many current contexts and problems. Moreover, individually they serve as a starting point for other derived analysis, as well as for the adaptation to other languages of the same family. This gives an added value to this work, a fact confirmed by some later works that are already benefiting from the results obtained in this thesis. / Tamarit Muñoz, S. (2013). Analysis Techniques for Concurrent Programming Languages [Tesis doctoral no publicada]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/31651 / TESIS

The thesis deals with design and implementation of the editor object-oriented Petri nets described by language PNTalk. A PNTalk compatible representation and storage format based on XML technologies will be created. The design of the individual parts of the editor focuses on the internal storage facilities, on the graphical user interface and its functionality. In the final part there are practical demonstrations of the application.

Les ateliers flexibles représentent pour les industriels un réel atout face à la concurrence et à l'imprévisibilité du marché. La mise en place et la gestion de ces catégories d'ateliers de production est souvent complexe, difficile et coûteuse. Ce travail de thèse, propose un outil d'aide à la décision permettant d'accompagner les industriels dans l'acquisition et la gestion d'ateliers flexibles de production. Cet outil s'appuie sur un modèle de simulation basé sur les Réseaux de Pétri Colorés Hiérarchiques. En effet, la simulation permet d'observer les variations des paramètres du système et de déterminer ses critères de performance. Les objectifs de cet outil sont de permettre la modélisation, la simulation et l'évaluation des systèmes de production en prenant en compte plusieurs contraintes rencontrées dans les systèmes industriels. Nous avons utilisé ce simulateur pour tester et valider une solution au problème d'acheminement des produits au cours de la production. Le choix des Réseaux de Pétri(RdP), au détriment des modèles analytiques, se justifie par le fait qu'ils offrent une représentation graphique permettant une description des processus plus simplifiée que des modèles analytiques. Au-delà de la modélisation et la simulation, les RdP permettent de vérifier les blocages d'un système. Parmi les modèles que nous avons développés nous pouvons citer : les modèles des machines, des stocks, des ressources de transport et des produits dans un système de production flexible. Nous avons insisté sur la modélisation des produits, des machines et du système de transport qui représentent le coeur des problématiques de flexibilité. Nous avons validé ces modèles sur un cas réel à savoir la chaîne de production du CESI de Rouen. Ensuite pour résoudre le problème du transport, nous avons proposé et déployé une méthode d'aide à la décision basée sur l'entropie et le classement de règles de dispatching. Cette méthode permet de définir, en fonction de l'état actuel, un ordre de priorité entre les règles de dispatching. Nous avons comparé cette nouvelle méthode à la méthode classique où l'importance des règles de priorité est définie préalablement, avant la phase de production. Notre proposition a donné des résultats intéressants que nous avons exposés et discutés. / Flexible Manufacturing Systems are real opportunity for industrials to face the comptetion and the unpredictability of the market. The management implementation of this kind of manufacturing systems are complex difficult and expensive.In this thesis work, we propose a decision making tool for managing Flexible Manufacturing Systems. The latter is based on a simulation model with Hierarchical Colored Petri Nets. The simulation allows the observation of the parameters variation of a system, and the determination of performance criteria. The objectives of this tool are to enable the modeling, simulation and evaluation of production systems taking into account most of the constraints encountered in industrial systems. We used this simulator to test and validate a solution to the problem of routing products during production. The choice of Petri nets (PN) to the detriment of analytical models is justified by the fact that Petri Nets with its graphical representation allows a simplified description of processes as analytical models , Petri Nets can be used for simulation, and with simulation we can predict the behaviour of a systems during a production phase. Petri Nets allow, beyond modeling and simulation to prevent the dead locks of systems. These are the reasons why we use Petri Nets to develop our models. Among the models that we have developed we can mention : machine, stocks, transportation resources and products models. We insisted on product and machine modelling which are in the center of flexibility issues. In order to study the routing problem, We defined models to represent the transport activity. We validated these models on a real case namely the production chain of CESI of Rouen. Then to solve the routing problem, we developed a decision making method based on entropy and dispacthing rules. This method allows to modify the dispatching rules weight in function of the state of the manufacturing systems during the production (size of stocks; machine failure). We compared this method with an another one where the weight of dispatching rules are unchanged during the production phase. We obtained interesting result that we have presented and discussed.

This paper describes the analysis tool DSPNexpress which has been developed at the Technische Universität Berlin since 1991. The development of DSPNexpress has been motivated by the lack of a powerful software package for the numerical solution of deterministic and stochastic Petri nets (DSPNs) and the complexity requirements imposed by evaluating memory consistency models for multicomputer systems. The development of DSPNexpress has gained by the author's experience with the version 1.4 of the software package GreatSPN. However, opposed to GreatSPN, the software architecture of DSPNexpress is particularly tailored to the numerical evaluation of DSPNs. Furthermore, DSPNexpress contains a graphical interface running under the X11 window system. To the best of the author's knowledge, DSPNexpress is the first software package which contains an efficient numerical algorithm for computing steady-state solutions of DSPNs.

Enterprise SIM profile provisioning solution is currently in development by some big players in the telecommunication industry. This solution may support an enterprise user staying anonymous to mobile network operators when remotely subscribing to SIM profiles. Another advantage refers to providing a seamless solution to enterprises where they can handle subscriptions of their employees. However, the solution is still in an early stage of production, and it is of utmost importance to proactively detect threats and deviant behaviors. The focus of this master thesis is providing a part towards achieving a secure solution by gaining insight and understanding of the system behavior. Colored Petri Nets technique is applied to the process and provides deterministic insights on system behavior. The solution of enterprise remote SIM profile provisioning is analyzed from different reachability goals by performing multiple simulations of different cases. Simulations are performed using different conditions and provide an understanding of system behavior with not fulfilled conditions. Essential aspects of this work can be in consideration when developing the solution to not end up in a state where a user receives a bad SIM profile or exposes the system to other threats.

Le " serious gaming " est une approche récente pour mener des activités " sérieuses " telles que communiquer, sensibiliser ou apprendre, en utilisant les techniques mises en œuvre dans les jeux vidéo. Les jeux sérieux sont devenus aujourd'hui un élément incontournable de la formation en ligne. C'est dans ce cadre du serious gaming pour la formation que se situe ce sujet de thèse. En effet, quelle que soit l'acception privilégiée, de nombreuses questions de recherche se posent. En particulier, comment peut-on évaluer les connaissances acquises par le joueur/apprenant à travers le jeu ? Nous sommes concentrés sur les jeux de type étude de cas utilisés notamment en gestion ou en médecine et proposons une méthode basée sur l'Evidence Centered Design pour concevoir le suivi de l'apprenant à des fins de diagnostic à destination de l'enseignant et de l'apprenant. Les actions liées aux études de cas sont très proches des actions métiers et recourent à des règles bien précises. Nous avons fait le choix de les représenter à l'aide de réseaux de Petri. Pour apporter de la sémantique à l'analyse par réseau de Petri, nous l'avons adossé à une ontologie du domaine et des actions de jeu. L'ontologie apporte une complémentarité non négligeable au réseau de Petri qui a une dimension purement procédurale. Nous combinons des réseaux de Petri et les ontologies afin de produire des indicateurs de performance pour cette catégorie particulière de jeux sérieux. L'étude des erreurs nous a conduits à proposer une taxinomie particulière pour les jeux sérieux en nous inspirant notamment des travaux réalisés dans le domaine de la sécurité. / "Serious gaming" is a recent approach, using the techniques implemented in video games, to conduct "serious" activities such as communication, awareness and learning. Serious games have now become an essential element of online training. This thesis takes place in the context of serious games for training. Indeed, whatever the preferred meaning, many research questions arise. In particular, how can we assess the knowledge acquired by the player / learner through the game? We have focused on case study type games used especially in management or medicine. We propose a method based on Evidence Centered Design to plan the monitoring of the learner for diagnostic purposes to the teacher and the learner. Actions in case studies are very close to business actions and resort to specific rules. We have chosen to represent them using Petri nets. To bring semantics to the Petri net analysis, we have added a domain and game action ontology. The ontology provides a significant complementarity to Petri net that has a purely procedural dimension. We have combined Petri nets and ontologies to produce performance indicators for this particular category of serious games. The study of errors led us to propose a particular taxonomy for serious games based on the work done in the field of security.

Les réseaux de transport multimodaux modernes sont essentiels pour la durabilité écologique et l’aisance économique des agglomérations urbaines, par conséquent aussi pour la qualité de vie de leurs habitants. D’ailleurs, le bon fonctionnement sur le plan de la compatibilité entre les différents services et lignes est essentiel pour leur acceptation, étant donné que (i) la plupart des trajets nécessitent des changements entre les lignes et que (ii) des investissements coûteux, dans le but de créer des liens plus directs avec la construction de nouvelles lignes ou l’extension de lignes existantes, ne sont pas à débattre. Une meilleure compréhension des interactions entre les modes et les lignes dans le contexte des transferts de passagers est ainsi d’une importance cruciale. Toutefois, comprendre ces transferts est singulièrement difficile dans le cas de situations inhabituelles comme des incidents de passagers et/ou si la demande dévie des plans statistiques à long terme. Ici le développement et l’intégration de modèles mathématiques sophistiqués peuvent remédier à ces inconvénients. À ce propos, la supervision via des modèles prévoyants représente un champ d’application très prometteur, analysée ici. La supervision selon des modèles prévoyants peut prendre différentes formes. Dans le présent travail, nous nous intéressons à l’analyse de l’impact basé sur des modèles de différentes actions, comme des départs en retard de certains véhicules après un arrêt, appliqué sur le fonctionnement du réseau de transport et sa gestion de situations de stress qui ne font pas partie des données statistiques. C’est pourquoi nous introduisons un nouveau modèle, un automate hybride avec une dynamique probabiliste, et nous montrons comment ce modèle profondément mathématique peut prédire le nombre de passagers dans et l’état de fonctionnement du véhicule en question du réseau de transport, d’abord par de simples estimations du nombre de tous les passagers et la connaissance exacte de l’état du véhicule au moment de l’incident. Ce nouvel automate réunit sous un même regard les passagers demandeurs de services de transport à parcours fixes ainsi que les véhicules capables de les assurer. Il prend en compte la capacité maximale et le fait que les passagers n’empruntent pas nécessairement des chemins efficaces, dont la représentation sous la forme d’une fonction de coût facilement compréhensible devient nécessaire. Chaque passager possède son propre profil de voyage qui définit un chemin fixe dans l’infrastructure du réseau de transport, et une préférence pour les différents services de transport sur son chemin. Les mouvements de véhicules sont inclus dans la dynamique du modèle, ce qui est essentiel pour l’analyse de l’impact de chaque action liée aux mouvements de véhicule. De surcroît, notre modèle prend en compte l’incertitude qui résulte du nombre inconnu de passagers au début et de passagers arrivant au fur et à mesure. Comparé aux modèles classiques d’automates hybrides, notre approche inspirée du style des réseaux de Pétri ne requiert pas le calcul de ces équations différentielles à la main. Ces systèmes peuvent être dérivés de la représentation essentiellement graphique d’une manière automatique pour le calcul en temps discret d’une prévision. Cette propriété de notre modèle réduit le risque de précisions faites par des humains et les erreurs qui en résulteraient. Après avoir introduit notre nouveau modèle, nous développons dans ce rapport également quelques éléments constitutifs sous la forme d'algorithmes qui visent les deux types d'impasses qui sont probables d'occurir pendant la simulation faisant un pronostic, c-à-d l'intégration numérique des systèmes de haute dimension d'équations différentielles et l'explosion combinatoire de son état discret. En plus, nous prouvons la faisabilité des calculs et nous montrons les bénéfices prospectifs de notre approche dans la forme de quelques tests simplistes et quelques cas plus réalistes. / Without any doubt, modern multimodal transportation systems are vital to the ecological sustainability and the economic prosperity of urban agglomerations, and in doing so to the quality of life of their many inhabitants. Moreover it is known that a well-functioning interoperability of the different modes and lines in such networked systems is key to their acceptance given the fact that (i) many if not most trips between different origin/destination pairs require transfers, and (ii) costly infrastructure investments targeting the creation of more direct links through the construction of new or the extension of existing lines are not open to debate. Thus, a better understanding of how the different modes and lines in these systems interact through passenger transfers is of utmost importance. However, acquiring this understanding is particularly tricky in degraded situations where some or all transportation services cannot be provided as planned due to e.g. some passenger incident, and/or where the demand for these scheduled services deviates from any statistical long term-plannings. Here, the development for and integration of sophisticated mathematical models into the operation of such systems may provide remedy, where model-predictive supervision seems to be one very promising area of application which we consider here. Model-predictive supervision can take several forms. In this work, we focus on the model-based impact analysis of different actions, such as the delayed departure of some vehicle from a stop, applied to the operation of the considered transportation system upon some downgrading situation occurs which lacks statistical data. For this purpose, we introduce a new stochastic hybrid automaton model, and show how this mathematically profound model can be used to forecast the passenger numbers in and the vehicle operational state of this transportation system starting from estimations of all passenger numbers and an exact knowledge of the vehicle operational state at the time of the incident occurrence. Our new automaton model brings under the same roof, all passengers who demand fixed-route transportation services, and all vehicles which provide them. It explicitly accounts for all capacity-limits and the fact that passengers do not necessarily follow efficient paths which must be mapped to some simple to understand cost function. Instead, every passenger has a trip profile which defines a fixed route in the infrastructure of the transportation system, and a preference for the different transportation services along this route. Moreover, our model does not abstract away from all vehicle movements but explicitly includes them in its dynamics, which latter property is crucial to the impact analysis of any vehicle movement-related action. In addition our model accounts for uncertainty; resulting from unknown initial passenger numbers and unknown passenger arrival flows. Compared to classical modelling approaches for hybrid automata, our Petri net-styled approach does not require the end user to specify our model's many differential equations systems by hand. Instead, all these systems can be derived from the model's predominantly graphical specification in a fully automated manner for the discrete time computation of any forecast. This latter property of our model in turn reduces the risk of man-made specification and thus forecasting errors. Besides introducing our new model, we also develop in this report some algorithmic bricks which target two major bottlenecks which are likely to occur during its forecast-producing simulation, namely the numerical integration of the many high-dimensional systems of stochastic differential equations and the combinatorial explosion of its discrete state. Moreover, we proof the computational feasibility and show the prospective benefits of our approach in form of some simplistic test- and some more realistic use case.

Indiana University-Purdue University Indianapolis (IUPUI) / This thesis proposed an algorithm that can find optimized Petri nets from given observation sequences according to some rules of optimization. The basic idea of this algorithm is that although the length of the observation sequences can keep growing, we can think of the growing as periodic and algorithm deals with fixed observations at different time. And the algorithm developed has polynomial complexity. A segment of example code programed according to this algorithm has also been shown. Furthermore, we modify this algorithm and it can check whether a Petri net could fit the observation sequences after several steps. The modified algorithm could work in constant time. These algorithms could be used in optimization of the control systems and communication networks to simplify their structures.

Indiana University-Purdue University Indianapolis (IUPUI) / In automotive industry, driver assistance and active safety features are main areas of research. This thesis concentrates on designing one of the famous ADAS system feature called Adaptive cruise control. Feature development and analysis of various functionalities involved in the system control are done using Petri Nets. A background on the past and current ACC research is noted and taken as motivation. The idea is to implement the adaptive cruise control system in Petri net and analyze how to provide fault tolerance to the system. The system can be evaluated for various cases. The ACC technology implemented in di erent cars were compared and discussed. The interaction of the ACC module with other modules in the car is explained. The cruise system's algorithm in Petri net is used as the basis for developing Adaptive Cruise Control system's algorithm. The ACC system model is designed using Petri nets and various Petri net functionalities like place invariant, transition invariant and reachability tree of the model are analyzed. The results are veri ed using Matlab. Controllers are introduced for ideal cases and are implemented in Petri nets. Then the error cases are considered and fault tolerance techniques are carried out on the model to identify the fault places.