[pt] Este trabalho visa apresentar a integração de várias mídias de informação, como voz, texto, imagem e gráficos em um ambiente de troca de mensagens como a melhor resposta às solicitações de evolução de sistemas de troca de informação. Assim, será apresentado do LANBRETA-DMS (LAN-Based real Time Áudio-Data Message System), com ênfase na especificação de seus serviços, descrevendo-se a sintaxe do protocolo empregado e sua semântica, sendo esta última apresentada sob a forma de uma pseudo-linguagem de programação e sob a forma de redes de Petri. Uma implementação do LANBRETA-DMS, realizada nos laboratórios da PUC-RJ será também apresentada, seguindo- se proposições para extensões futuras. / [en] This work presents the integration of information media such as voice, text, imge and graphics in a message Exchange environment as the best answer to evolution of information Exchange systems. LANBRETA-DMS (LAN-Based Real Time Audio-Data Messege System) will be presented, with enphasis on the specification of its services, the protocol sintax used and its semantics, the latter being presented in a pseudo- programming language and in Petri Networks. An implementation of LANBRETA-DMS, made at PUC-RJ, will alos be introced, with some proposais for future extrensions following.

In the past two decades, multi-agent systems (MAS) have emerged as a new paradigm for conceptualizing large and complex distributed software systems. A multi-agent system view provides a natural abstraction for both the structure and the behavior of modern-day software systems. Although there were many conceptual frameworks for using multi-agent systems, there was no well established and widely accepted method for modeling multi-agent systems. This dissertation research addressed the representation and analysis of multi-agent systems based on model-oriented formal methods. The objective was to provide a systematic approach for studying MAS at an early stage of system development to ensure the quality of design. Given that there was no well-defined formal model directly supporting agent-oriented modeling, this study was centered on three main topics: (1) adapting a well-known formal model, predicate transition nets (PrT nets), to support MAS modeling; (2) formulating a modeling methodology to ease the construction of formal MAS models; and (3) developing a technique to support machine analysis of formal MAS models using model checking technology. PrT nets were extended to include the notions of dynamic structure, agent communication and coordination to support agent-oriented modeling. An aspect-oriented technique was developed to address the modularity of agent models and compositionality of incremental analysis. A set of translation rules were defined to systematically translate formal MAS models to concrete models that can be verified through the model checker SPIN (Simple Promela Interpreter). This dissertation presents the framework developed for modeling and analyzing MAS, including a well-defined process model based on nested PrT nets, and a comprehensive methodology to guide the construction and analysis of formal MAS models.

Les systèmes logiciels complexes sont omniprésents dans notre vie quotidienne. De ce fait, un dysfonctionnement peut occasionner aussi bien une simple gêne qu'un danger mettant en péril des vies humaines. Le test est l'une des techniques les plus répandues (en particulier dans l'industrie) pour détecter les erreurs d'un système. Lorsque le cahier des charges d'un système est décrit par une spécification formelle, le test de conformité est utilisé pour garantir un certain niveau de confiance dans la correction d'une implémentation de ce système - dans ce cadre, la relation de conformité formalise la notion de correction. Cette thèse se focalise sur le test de conformité pour les systèmes concurrents. Le test de conformité pour les systèmes concurrents utilise principalement des modèles qui interprètent la concurrence par des entrelacements. Néanmoins, cette approche souffre du problème de l'explosion de l'espace d'états et elle n'offre pas la possibilité de tester certaines propriétés de la spécification telle que l'indépendance entre actions. Pour ces raisons, nous utilisons une sémantique d'ordres partiels pour la concurrence. De plus, nous proposons une nouvelle sémantique qui permet à certaines actions concurrentes d'être entrelacées et en force d'autres à être implémentées indépendamment. Nous proposons une généralisation de la relation de conformité ioco où les spécifications sont des réseaux de Petri et leur sémantique d'ordres partiels est donnée par leur dépliage. Cette relation de conformité permet de préserver l'indépendance, dans l'implémentation, des actions spécifiées comme concurrentes. Nous présentons un cadre de test complet pour cette relation. Nous définissons la notion de cas de test globaux gérant la concurrence, réduisant ainsi non seulement la taille des cas de test mais aussi celle de la suite de tests. Nous montrons comment les cas de test globaux peuvent être construits à partir du dépliage de la spécification en s'appuyant sur une traduction SAT, et nous réduisons le problème de la sélection de tests à la sélection d'un préfixe fini de ce dépliage : nous définissons différents critères de sélection à partir de la notion d'événement limite (cut-off event). Enfin, en supposant que chaque processus d'un système distribué possède une horloge locale, nous montrons que la conformité globale peut être testée dans une architecture de test distribuée en utilisant seulement des testeurs locaux ne communiquant pas entre eux. / Complex systems are everywhere and are part of our daily life. As a consequence, their failures can range from being inconvenient to being life-threatening. Testing is one of the most widely accepted techniques (especially in industry) to detect errors in a system. When the requirements of the system are described by a formal specification, conformance testing is used to guarantee a certain degree of confidence in the correctness of an implementation- in this setting a conformance relation formalizes the notion of correctness. This thesis focuses on conformance testing for concurrent systems. Conformance testing for concurrent system has mainly focused on models that interpret concurrency by interleavings. This approach does not only suf- fer from the state space explosion problem, but also lacks the ability to test properties of the specification such as independence between actions. For such reasons, we focus not only on partial order semantics for concurrency, but also propose a new semantics that allows to interleave some actions while forcing others to be implemented as independent. We propose a generalization of the ioco conformance relation, based on Petri nets specifications and their partial order semantics given by their unfoldings, preserving thus independence of actions from the specification. A complete testing framework for this conformance relation is presented. We introduce the notion of global test cases which handle concurrency, reducing not only the size of the test case, but also the number of tests in the test suite. We show how global test cases can be constructed from the unfolding of the specification based on a SAT encoding and we reduce the test selection problem to select a finite prefix of such unfolding: different testing criteria are defined based on the notion of cut-off events. Finally, we show that assuming each process of a distributed system has a local clock, global conformance can be tested in a distributed testing architecture using only local testers without any communication.

A fairly general model of the elevator system is presented. Coloured Petri Nets (CPN) and CPN tools are adopted as modeling tools. The model, which is independent of the number of floors and elevators, covers different stages of the elevator system in substantial detail. The model assists simulation-based analysis of different algorithms and rules which govern real elevator systems. The results prove the compatibility and applicability of this model in various situations and demonstrate the expressive power and convenience of CPN. / Thesis / Master of Applied Science (MASc)

Yes / System safety, reliability and risk analysis are important tasks that are performed throughout the system lifecycle to ensure the dependability of safety-critical systems. Probabilistic risk assessment (PRA) approaches are comprehensive, structured and logical methods widely used for this purpose. PRA approaches include, but not limited to, Fault Tree Analysis (FTA), Failure Mode and Effects Analysis (FMEA), and Event Tree Analysis (ETA). Growing complexity of modern systems and their capability of behaving dynamically make it challenging for classical PRA techniques to analyse such systems accurately. For a comprehensive and accurate analysis of complex systems, different characteristics such as functional dependencies among components, temporal behaviour of systems, multiple failure modes/states for components/systems, and uncertainty in system behaviour and failure data are needed to be considered. Unfortunately, classical approaches are not capable of accounting for these aspects. Bayesian networks (BNs) have gained popularity in risk assessment applications due to their flexible structure and capability of incorporating most of the above mentioned aspects during analysis. Furthermore, BNs have the ability to perform diagnostic analysis. Petri Nets are another formal graphical and mathematical tool capable of modelling and analysing dynamic behaviour of systems. They are also increasingly used for system safety, reliability and risk evaluation. This paper presents a review of the applications of Bayesian networks and Petri nets in system safety, reliability and risk assessments. The review highlights the potential usefulness of the BN and PN based approaches over other classical approaches, and relative strengths and weaknesses in different practical application scenarios. / This work was funded by the DEIS H2020 project (Grant Agreement 732242).

A methodology for representing and analyzing manufacturing systems in a hybrid systems framework for control reconfiguration purposes in the presence of defects and failures at the product and system levels is presented. At the top level, a supervisory Petri net directs parts/jobs through the manufacturing system. An object-based hybrid systems model that incorporates both Petri nets at the event-driven level and differential equations at the time-driven level describes the subsystems. Rerouting capabilities utilizing this model at the product and operation levels were explained. Simulations were performed on a testbed model for optimal time and mode transition cost to determine the route for parts. The product level reconfiguration architecture utilizes an adaptive network-based fuzzy inference system (ANFIS) to map histogram comparison metrics to set-point adjustments when product defects were detected. Tests were performed on good and defective plastic parts from a plastic injection molding machine. In addition, a mode identification architecture was described that incorporates both time- and event-driven information to determine the operating mode of a system from measured sensor signals. Simulated data representing the measured process signals from a Navy ship chiller system were used to verify that the appropriate operating modes were detected.

This thesis deals with the concept of the formalism of Petri nets, which allows to investigate the dynamic behavior of parallel and nondeterministic systems. Furthermore, this deals with its variant of Object-Oriented Petri Nets (OOPN), which aims to facilitate the process of modeling systems with an object-oriented approach. The aim of this master thesis is to design an internal representation of OOPN models, which is suitable for efficient interpretation and implement compiler from PNtalk language into the internal representation. Subsequently, design and implement an OOPN model interpreter using this internal representation of models, which in addition to Petri net objects, must also be able to work with a selected subset of objects from the Java language.

This thesis is focused on distributed systems modeling using Petri nets. Distributed systems are increasingly being implemented in applications and computing systems, where their task is to ensure sufficient performance and stability for a large number of its users. When modeling a distributed systems, stochastic behavior of Petri nets is important, which will provide more realistic simulations. Therefore, this thesis focuses mainly on timed Petri nets. The theoretical part of this thesis summarizes distributed systems, their properties, types and available architectures, as well as Petri nets, their representation, types and the principle of an operation. In the practical part, two models were implemented, namely a horizontally scaled web application divided into several services with a distributed database and a large grid computing system, more precisely the BOINC platform with the Folding@home project. Both models were implemented using the PetNetSim library of Python. The goal of this thesis is to perform simulations on the created models for different scenarios of their behavior.

This diploma thesis formally defines the Object Oriented Petri Nets and presents term a virtual machine. Then it introduces the concept of Object Oriented Petri Nets Virtual Machine. Finally, project describes a procedure for implementation of the OOPN Virtual Machine.

[pt] Lógica Proposicional Dinâmica (PDL) é um sistema lógico multi-modal utilizada para especificar e verificar propriedades em programas sequenciais. Redes de Petri são um formalismo largamente utilizado na especificação de sistemas concorrentes e possuem uma interpretação gráfica bastante intuitiva. Neste trabalho apresentam-se extensões da Lógica Proposicional Dinâmica onde os programas são substituídos por Redes de Petri. Define-se uma codificação composicional para as Redes de Petri através de redes básicas, apresentando uma semântica composicional. Uma axiomatização é definida para a qual o sistema é provado ser correto, e completo em relação à semântica proposta. Três Lógicas Dinâmicas são apresentadas: uma para efetuar inferências sobre Redes de Petri Marcadas ordinárias e duas para inferências sobre Redes de Petri Estocásticas marcadas, possibilitando a modelagem de cenários mais complexos. Alguns sistemas dedutivos para essas lógicas são apresentados. A principal vantagem desta abordagem concerne em possibilitar efetuar inferências sobre Redes de Petri [Estocásticas] marcadas sem a necessidade de traduzí-las a outros formalismos. / [en] Propositional Dynamic Logic (PDL) is a multi-modal logic used for specifying and reasoning on sequential programs. Petri Net is a widely used formalism to specify and to analyze concurrent programs with a very intuitive graphical representation. In this work, we propose some extensions of Propositional Dynamic Logic for reasoning about Petri Nets. We define a compositional encoding of Petri Nets from basic nets as terms. Second, we use these terms as PDL programs and provide a compositional semantics to PDL Formulas. Then we present an axiomatization and prove completeness regarding our semantics. Three versions of Dynamic Logics to reasoning with Petri Nets are presented: one of them for ordinary Marked Petri Nets and two for Marked Stochastic Petri Nets yielding to the possibility of model more complex scenarios. Some deductive systems are presented. The main advantage of our approach is that we can reason about [Stochastic] Petri Nets using our Dynamic Logic and we do not need to translate it into other formalisms. Moreover our approach is compositional allowing for construction of complex nets using basic ones.