A competição no mercado globalizado, do ponto de vista do consumidor, aumentou consideravelmente a oferta de produtos e serviços, permitindo a escolha pela qualidade, preço, prazos e/ou disponibilidade. Entretanto, do ponto de vista das empresas, o desafio de atuar em um mercado saturado, dinâmico, competitivo e com aumento da demanda de produção orientado ao consumidor altera consideravelmente toda a estrutura da empresa. Desta forma, a flexibilidade torna-se um pré-requisito fundamental para que as empresas possam atuar neste mercado. Considerando-se o contexto apresentado, o objeto de estudo do presente trabalho são os Sistemas Produtivos Flexíveis (SPFs). Os SPFs são sistemas concebidos para atender às necessidades de um mercado dinâmico e competitivo. Isto causa complexidade no comportamento global desses sistemas exigindo diferentes propostas para o projeto de Sistemas de Controle de SPFs. A complexidade advém do fato de se perder a informação quanto ao pré-determinismo da seqüência de eventos que ocorrem no sistema global, além do fato de não existir previamente a definição de todos os processos de transporte com a designação prévia de todas as ordens de transporte que os transportadores presentes na planta devem executar. Neste contexto, o objetivo deste trabalho é apresentar como resultado uma proposta de sistema de controle modular para SPFs que atenda os requisitos de fluxo de informações envolvendo hierarquia e colaboração simultânea entre os módulos, respeitando a diversidade semântica presente na arquitetura. Apresenta-se então uma sistematização de projeto dos diversos módulos de controle e uma proposta de implementação de um algoritmo de designação dos transportadores para ser utilizado em tempo real permitindo a realização eficiente das atividades de transporte. / The competition in the globalized market increased considerably the demand for products and services to the customer point of view. However, the consumer\'s driven demand change the whole structure of the company. Thus, flexibility becomes an essential pre-requisite for companies to compete in the market. Considering the context presented, the object of study of this work is the Flexible Production System (FPS). The FPS must fulfill the needs on a dynamic and competitive market. This situation causes complexity in the overall performance of these systems, requiring different proposals for the design of the control systems. The complexity arises due to the fact that loses the information about the sequence of events that occur in the global system. Besides there is no previous exist definition for all processes of transport and prior designation for it. In this context, the objective of this work is to present a proposal for modular control systems to FPS that fits the requirements of information flow involving hierarchy and simultaneous collaboration between the modules. It will be presented systematization for the modular design of control as well as an implementation of an algorithm for designation of transport in real time leading to an efficient management of these activities.

Os simuladores de treinamento têm se tornado cada vez mais populares, apresentando aplicações em diversas áreas, como na condução de veículos terrestres, aeronaves, procedimentos médicos, operações militares, entre outras. Estes simuladores podem ser classificados em diferentes grupos, de acordo com a finalidade do seu treinamento. Os simuladores que envolvem o treinamento de procedimentos têm a finalidade de capacitar o usuário na execução de atividades bem definidas, dando ênfase às ações que o usuário precisa efetuar e às relações de dependência existentes entre estas ações. As aplicações deste grupo de simuladores são o objeto deste trabalho e podem ser usadas em diversas situações, como na montagem, desmontagem, operação e manutenção de máquinas complexas, na execução de atividades que ofereçam risco ao usuário ou, possam causar dano ao equipamento utilizado. As vantagens associadas com o treinamento em Realidade Virtual têm aumentado a procura por este tipo de aplicação. Apesar disto, no cenário nacional, poucos trabalhos acadêmicos foram publicados nesta área de pesquisa. Com a finalidade de auxiliar o desenvolvimento de simuladores de procedimentos, este trabalho apresenta a proposta de um arcabouço de treinamento, que foi elaborado com base nos elementos obtidos na revisão da literatura e na investigação de outras arquiteturas e ferramentas. A revisão da literatura considerou diversas técnicas usadas na descrição dos cenários de treinamento, entre elas, podemos citar a Máquina de estados, Sistema baseado em regras, STORM, Grafos, Diagrama LORA e rede de Petri. O arcabouço proposto _e composto por uma arquitetura, que define os componentes e os conceitos envolvidos no treinamento de procedimentos, e uma biblioteca de software, planejada com base nesta arquitetura e elaborada com o propósito de facilitar o desenvolvimento de aplicações de treinamento. As características deste arcabouço foram verificadas e validadas através da implementação de dois casos de uso. O primeiro caso consiste em uma aplicação de simulação de troca de cruzeta em linha viva, onde o usuário realiza um procedimento de risco na manutenção de redes de distribuição, e o segundo caso, envolve a prática da montagem e desmontagem de uma Unidade Geradora Hidrelétrica. Em ambas as aplicações, o modelo de Máquina de estados foi utilizado de forma simplificada na representação dos objetos interativos, e o modelo de rede de Petri foi usado para representar os procedimentos de treinamento. / The simulators for training have become increasingly popular, with applications in several areas, such as in land vehicles, aircraft, medical procedures, military operations, among others. These simulators can be classified into different groups according to the purpose of their training. The simulators that involve the training of procedures are intended to empower the user to perform well defined activities, with an emphasis on the actions that the user needs to perform and on the existing dependencies between these actions. The applications of this group of simulators are the subject of this work, and can be used in various situations, such as in assembly, disassembly, operation and maintenance of complex machinery, in performing activities that poses any danger to the user, or may cause damage to the equipment. The advantages associated with virtual reality training have increased the demand for this type of application. Despite this, in Brazil, few papers have been published in this area of research. In order to assist the development of procedure simulators, this work proposes a framework for virtual training, which was based on evidences obtained in the literature review and while investigating other architectures and tools. The literature review found several techniques used in the description of the training scenarios, among them, we may mention the state machine, rule-based system, STORM, Graphs, LORA Diagram and Petri net. The proposed framework consists of an architecture, that defines the components and concepts involved in training procedures, and a software library, which was planned based on this architecture and elaborated with the purpose of facilitating the development of applications for training. The characteristics of this framework has been verified and validated through the implementation of two use cases. The first case is a application for simulating the exchange of a crosshead, where the user performs a risky procedure in the maintenance of distribution networks, and the second case, which involves assembling and disassembling of a Hydroelectric Generating Unit. In both applications, the model of simple state machine was used to represent the behavior of interactive objects, and the Petri net model was used to represent the training procedures.

Frequentemente, as empresas adquirem ou desenvolvem aplicações para apoiar a tomada de decisões e aperfeiçoar seus processos de negócio. Estas aplicações compõe o ecossistema de software, que geralmente é heterogêneo e ainda são desenvolvidas sem levar em conta sua possível integração, dificultando assim a sua reutilização. A área de Enterprise Application Integration (EAI) proporciona metodologias, técnicas e ferramentas para as empresas desenvolverem soluções de integração. O problema abordado nessa dissertação consiste em identificar os possíveis gargalos de desempenho na solução de integração que trata do processo e rematrículas da Universidade Unijuí, para que estes possam ser minimizados antes da implementação da solução. O aparecimento destes possíveis gargalos é um problema, porque se um modelo conceitual for implementado com gargalos, poderá gerar falhas, que aumentam os custos, tempo e riscos da solução. Nesse contexto, propõe-se identificar possíveis gargalos de desempenho, utilizando o modelo conceitual, por meio do qual é desenvolvido um modelo formal de simulação, utilizando o formalismo matemático das Redes de Petri Coloridas e Temporizadas. É por meio da simulação, que busca-se conhecer o comportamento do sistema, visando identificar tarefas que possam representar gargalos de desempenho. A partir da simulação, foi possível analisar duas variáveis: tempo médio de permanência das mensagens nos slots e tamanho máximo e médio dos slots. Os resultados da simulação das duas variáveis foram interpretados e analisados, identificando-se a ocorrência de gargalos de desempenho. / 145 f.

Uma vez que uma aplicação ou projeto tenha sido identificado como sujeito ao uso da simulação, decisões devem ser tomadas acerca de como conduzir os estudos. Embora não haja regras definitivas, alguns passos são geralmente recomendados, tais como: planejamento do estudo, definição do sistema, construção do modelo, execução dos experimentos, análise dos resultados e relatório final. E, a construção do modelo é uma das etapas mais demoradas e complexas. Na execução dos experimentos, e na análise dos resultados a Realidade Virtual (RV) é uma interface que pode fornecer um suporte importante para a tomada de decisões, pois a RV auxilia na criação de mundos virtuais semelhantes ao mundo real, que ajudam na compreensão do funcionamento dos sistemas. Este trabalho propõe um metamodelo para o desenvolvimento de sistemas de simulação de eventos discretos com interface de RV aplicados a ambientes ou estações de trabalho de manufatura. A proposta do metamodelo é composto por quatro módulos: i) de edição e validação de modelos, ii) de criação, edição e execução de ambientes virtuais, iii) de conexão para efetuar o elo entre os dois primeiros módulos e, iv) de controle para gerenciar a comunicação e controlar a simulação. Como resultado tem-se a simulação centralizada baseada no modelo descrito em Rede de Petris (RP) com interface de RV distribuída. O sistema computacional gerado pelo metamodelo auxiliará no aprendizado e compreensão do problema simulado, e ainda permitirá ao usuário o envolvimento através da iteração. / The VR aids in the creation of virtual worlds similar to the real world, helping in understanding how a system works. This research work is concerned with the development of a discrete-event system simulation based on Petri Nets, with Virtual Reality interface for manufacturing environment or workstations. The system is composed of four modules, the first is model editing and validation, the second module is a modeling tool for virtual objects and/or a library of virtual elements, the third module makes the link between the two previous modules, and finally, the fourth is a simulation and control module. The centralized simulation is based on models described by Petri Nets with distributed RV interface resulting in a flexible and consistent system. The system will help users in learning and understanding the simulation problem, and it will also allow the user\'s integration with the environment through the interaction, and through distributed interface.

Esquemas baseados em grafos, em diferentes níveis de formalismo, são um forte apelo para a constituição de representações de sistemas complexos e de grande porte aplicados em várias áreas do conhecimento. Este fato responde pelo crescimento acentuado de métodos e representações formais baseadas em grafos e aplicadas em diferentes áreas, especialmente na Engenharia. As Redes de Petri (RdP) constituem um destes métodos, que apareceu em 1962 e desde então tem contribuído para o avanço dos métodos formais para o tratamento de sistemas de controle, sistemas discretos, logística, workflow, cadeia de fornecedores, redes de computadores, e uma variada classe de outros sistemas. Da mesma forma que outras representações formais, as primeiras tentativas de uso prático destas redes estiveram sempre ligadas ao domínio de aplicação, o que levou à criação de várias extensões. Por outro lado, a necessidade de se aplicar a representação em redes para sistemas de grande porte suscitou a discussão sobre as limitações do formalismo e sobre a necessidade de se inserir redes de alto nível. No entanto, todo este desenvolvimento, apesar de sua difusão em diferentes domínios, levantou a discussão sobre a unificação das redes. Desde 1992 a unificação do formalismo das RdPs é discutida pela comunidade acadêmica e, finalmente, no início deste século um padrão ISO/IEC foi proposto. Esta proposta conduz a dois desafios: i) mostrar que um formalismo de redes que seja candidato a ser usado na prática pertença de fato à classe de redes prescrita pelo padrão; ii) participar da discussão sobre a semântica das extensões propondo ambientes computacionais para o uso prático na modelagem e design de sistemas de grande porte. A rede GHENeSys, concebida e desenvolvida no Design Lab da Universidade de São Paulo, é uma rede estendida com conceitos de orientação a objetos, um mecanismo de hierarquia e, até o momento, parece ser uma das primeiras tentativas de prover um ambiente de modelagem e design com as propriedades de uma rede unificada, com capacidade para cobrir as diferentes variantes das RdP e suas extensões. Neste trabalho é apresentada uma proposta de ambiente integrado de modelagem para a representação de sistemas a eventos discretos (SEDs) em RdP, baseada em um formalismo enquadrado dentro da norma ISO/IEC 15909 recentemente proposta. Este formalismo é a rede GHENeSys, que terá sua definição estendida utilizando como base a definição das RdPs Coloridas (CPN) com o objetivo de permitir a representação de tipos nas marcas. Um protótipo para testes, resultado da integração de diversos trabalhos desenvolvidos separadamente por membros do D-Lab que nunca foram implementados nem integrados em formalismo único, é apresentado. Este protótipo é utilizado em um estudo de caso com a finalidade de validar de forma prática os novos elementos acrescentados à definição da rede GHENeSys para permitir a modelagem de sistemas utilizando os elementos das RdPs de alto nível. / Graph schemas are a strong approach to the representation (in dierent degrees of formality) of large and complex systems in several areas of knowledge. This fact has provided a continuous growth of methods and new formal schemas, specially in Engineering. Petri Nets(PN) are one of these methods, which appears in 1962 and since then has improved the representation of discrete control, discrete systems, logistics, workflow, supply chain, computer networks, and a variety of other systems. As any other representation, the first attempts to use it in practice were always made in a close relation between the representation and the domain of discourse, openning opportunity for several extensions. Also the need to use it in large systems brought a discussion about the formalism and the need for high level systems. However, all this development, besides the broad use in different domains, rose the need for an unified approach. Since 1992 such unification has been addressed by the scientific community and finally, in the beginning of this century, a ISO/IEC standard was proposed. That proposal also brings two new challenges: i) to show that any proposed net that belongs to Petri Net class proved itself as satisfying the requirements of the standard; ii) to enter the discussions of the semantics of extensions and also provide practical and unified system environments that can really support the design of large and complex systems. In this work, we present a proposal for the developing of an integrated modeling environment for the representation of discrete event systems using Petri Nets. This environment will use an underlying formalism framed within the rules defined recently by the ISO/IEC, in the standard 15909. The formalism to be used will be the GHENeSys net, which will have its definition extended using the definition of the Coloured PN (CPN) as a starting point in order to allow the representation of types within the net tokens. A testing prototype for this integrated modeling environment, result of the integration of several previous works of D-Lab members that were never implemented or integrated in a unique formalism, is presented. This prototype will be used in a case study in order to validate in practical way the new elements added to the definition of GHENeSys, to allow the modeling of systems using the elements of HLPNs.

Propõe-se uma estratégia de modelagem e de análise formal de políticas de segurança para sistemas baseados em fluxos de trabalho (workflows) e contendo regras que envolvam aspectos de lógica de negócios. Verifica-se com o auxílio de uma política de exemplo que a estratégia proposta resulta em modelos amplamente capazes de expressar restrições lógicas em função de parâmetros de negócio sem comprometer a viabilidade de suas análises. A modelagem baseia-se no uso de um metamodelo definido a partir da identificação das entidades que caracterizam o estado de proteção de um sistema e representado na forma de uma rede de Petri colorida. Por meio da escrita de predicados para consulta sobre o espaço de estados da rede de Petri, verifica-se o atendimento às regras de segurança no modelo formal. A tratabilidade da análise é garantida pela adoção de um paradigma diferenciado principalmente pela busca de ramos inseguros em vez de nós inseguros no espaço de estados e por explorar a natureza independente entre serviços de negócio distintos, expressa por restrições ao fluxo de informação no metamodelo. Tais restrições permitem que a análise seja fracionada evitando o problema da explosão de estados. O exemplo discutido de modelagem e análise de um sistema de serviços bancários online fornece evidências suficientes para atestar a aplicabilidade do método à validação de políticas de segurança para sistemas reais. / A strategy is proposed for the formal modeling and analysis of workflow- -based security policies having rules which involve aspects of business logic. Aided by an example of security policy, the proposed strategy is shown to lead to models widely capable of expressing logical restrictions as functions of business parameters without compromising the feasibility of its analyses. The modeling is based on the usage of a metamodel defined from the identification of the entities that characterize the protection state of a system, and represented as a colored Petri net. By writing predicates for querying the Petri net state-space, compliance with security rules at the formal model is verified. The feasibility of the analysis is ensured by the adoption of a paradigm distinguished mainly for the search for insecure branches rather than insecure nodes in the state-space, and for exploiting the independent nature among different business services, expressed by restrictions to the information flow within the metamodel. Such restrictions allow the analysis to be fractioned, avoiding the state explosion problem. The example provided of modeling and analysis of an online banking services system offers enough evidence to attest the applicability of the method to the validation of security policies for real-world systems.

A fase inicial de projeto de sistemas, baseada na elicitação, modelagem e análise dos requisitos é considerada a mais complexa e a mais estratégica para obtenção de bons resultados. Por conseguinte, erros precisam ser detectados durante esta fase inicial, antes de começar a implementação, evitando assim o desperdício de tempo e recursos. Este trabalho propõe um método formal de modelagem, análise e verificação de requisitos, partindo de uma representação semi-formal de requisitos em UML, e utilizando o formalismo das Redes de Petri para proceder à modelagem, análise e verificação. Propriedades das redes de Petri, tais como invariantes, são usadas para analisar os requisitos, permitindo uma validação antecipada dos requisitos no processo de design. O objetivo deste trabalho é estender a aplicação das redes de Petri como representação formal para a modelagem e análise de requisitos, endereçando assim a fase anterior às especificações. Pressupõe-se a existência de uma disciplina de projeto baseada em modelos (model driven) que abrange a fase inicial do projeto e se propaga para a modelagem e verificação de soluções. Assim, a abordagem proposta nesta tese se encaixa plenamente em um processo orientado a modelos que use a mesma linguagem: as redes de Petri. / The first stage of system design, which includes elicitation, modeling, and analysis of requirements is considered at the same time, very complex and very strategic to achieve proper results.Therefore it is important to detect mistakes both, conceptual and in requirements, before implementation begins, avoiding the waste of time and resources. This work proposes a formal method for modeling, analysis and verification of requirements, starting with a semi-formal representation of requirements in UML. Petri net and its properties such as invariants are used to analyze requirements, thereby allowing that requirements can be validated earlier. The main objective of this work is to extend the application of Petri Nets, as a formal representation, to requirements phase, addressing specification building. It is assumed that there is a model driven design approach that encompass the initial (requirements) phase and goes through the modeling and verification of solutions. Therefore the approach proposed in this work fits a model driven general approach which could use the same formal language: Petri Nets.

A segurança do espaço aéreo pode aumentar consideravelmente com o uso de operações de espaçamento e separação aerotransportados. Sob este paradigma, a tarefa de manter distância em relação a outras aeronaves é delegada aos pilotos, que contarão com o Sistema de Assistência de Separação Aerotransportado (ASAS). Com este sistema, ainda em fase experimental, os pilotos tornam-se cientes dos riscos do tráfego circundante com até 15 minutos de antecedência, sem necessitar de auxílio dos controladores de tráfego aéreo. Esta antecedência é muito maior que a do atual sistema anti-colisão (TCAS), que é de menos de 1 minuto. O sistema ASAS utiliza uma tecnologia de comunicação mais avançada que a tecnologia do transponder modo C, utilizado atualmente pelo sistema anti-colisão. O novo sistema ASAS está sendo desenvolvido intensivamente no Eurocontrol e em outras iniciativas nos Estados Unidos da América, e funcionará em conjunto com o atual sistema anti-colisão, proporcionando redundância, ou seja: se o antigo sistema falhar, o novo ainda pode emitir um alerta, ou vice-versa. O presente trabalho de pesquisa aborda a aplicação do ASAS para aumentar a precisão do espaçamento entre aeronaves que chegam sequencialmente a um determinado aeroporto, por meio de um formalismo matemático denominado \"Rede de Petri Estocástica e Dinamicamente Colorida\", com a obtenção de dados quantitativos sobre o risco de acidente. Esses dados indicam que o risco de acidente é significativamente menor com o uso do ASAS do que sem o uso do ASAS. / The safety in the airspace can considerably increase with the use of airborne spacing and separation operations. Under this paradigm, the task of maintaining a safe distance between aircraft is delegated to the pilots, which will be supported by the Airborne Separation Assistance System (ASAS). With this system, which is still in experimental phase, pilots become aware of the surrounding air traffic risks with up to 15 minutes in advance, without the help of air traffic controllers on the ground. This antecedence is much greater than the one provided by the current Traffic Collision Avoidance System (TCAS). ASAS uses a more advanced communication technology than Mode-C transponder, broadly used in the current civil aviation for collision avoidance purposes. The development of ASAS is being carried out intensively in Eurocontrol and in other initiatives in the United States of America, and this novel system is intended to work in parallel with the current collision avoidance systems, acting as safety nets. The present study approaches the ASAS application to improve the precision of spacing between aircraft that sequentially arrive at an airport, using the so called mathematical formalism \"Stochastically and Dynamically Coloured Petri Net\", for evaluating quantitative data about accident risk. These data indicate that the accident risk is significantly smaller when aircraft pairs use ASAS Spacing than when aircraft pairs do not use ASAS Spacing.

L'être humain fait des erreurs, en particulier dans la réalisation de taches complexes comme la construction des systèmes informatiques modernes. Nous nous intéresserons dans cette thèse à la vérification assistée par ordinateur du bon fonctionnement des systèmes informatiques. Les systèmes informatiques actuels sont de grande complexité. Afin de garantir leur fiabilité, la vérification automatique est une alternative au 'testing' et à la simulation. Elle propose d'utiliser des ordinateurs pour explorer exhaustivement l'ensemble des états du système, ce qui est problématique: même des systèmes assez simples peuvent atteindre un grand nombre d'états. L'utilisation des bonnes représentations des espaces d'états est essentielle pour surmonter la complexité des problèmes posés en vérification automatique. La vérification des systèmes concurrents amène des difficultés additionnelles, car l'analyse doit, en principe, examiner tous les ordres possibles d'exécution des actions concurrentes. Le dépliage des réseaux de Petri est une technique largement étudiée pour la vérification des systèmes concurrents. Il représentent l'espace d'états du système par un ordre partiel, ce qui se révèle aussi naturel qu'efficace pour la vérification automatique. Nous nous intéressons à la vérification des systèmes concurrents modélisés par des réseaux de Petri, en étudiant deux techniques remarquables de vérification: le 'model checking' et le diagnostic. Nous étudions les dépliages des réseaux de Petri étendus avec des arcs de lecture. Ces dépliages, aussi appelés dépliages contextuels, semblent être une meilleure représentation des systèmes contenant des actions concurrentes qui lisent des ressources partagées : ils peuvent être exponentiellement plus compacts dans ces cas. Ce travail contient des contributions théoriques et pratiques. Dans un premier temps, nous étudions la construction des dépliages contextuels, en proposant des algorithmes et des structures de données pour leur construction efficace. Nous combinons les dépliages contextuels avec les 'merged process', une autre représentation des systèmes concurrents qui contourne l'explosion d'états dérivée du non-déterminisme. Cette nouvelle structure, appelée 'contextual merged process', est souvent exponentiellement plus compacte, ce que nous montrons expérimentalement. Ensuite, nous nous intéressons à la vérification à l'aide des dépliages contextuels. Nous traduisons vers SAT le problème d'atteignabilité des dépliages contextuels, en abordant les problèmes issus des cycles de conflit asymétrique. Nous introduisons également une méthode de diagnostic avec des hypothèses d'équité, cette fois pour des dépliages ordinaires. Enfin, nous implémentons ces algorithmes dans le but de produire un outil de vérification compétitif et robuste. L'évaluation de nos méthodes sur un ensemble d'exemples standards, et leur comparaison avec des techniques issues des dépliages ordinaires, montrent que la vérification avec des dépliages contextuels est plus efficace que les techniques existantes dans de nombreux cas. Ceci suggère que les dépliages contextuels, et les structures d'évènements asymétriques en général, méritent une place légitime dans la recherche en concurrence, également du point de vu de leur efficacité. / Humans make mistakes, especially when faced to complex tasks, such as the construction of modern hardware or software. This thesis focuses on machine-assisted techniques to guarantee that computers behave correctly. Modern computer systems are large and complex. Automated formal verification stands as an alternative to testing or simulation to ensuring their reliability. It essentially proposes to employ computers to exhaustively check the system behavior. Unfortunately, automated verification suffers from the state-space explosion problem: even relatively small systems can reach a huge number of states. Using the right representation for the system behavior seems to be a key step to tackle the inherent complexity of the problems that automated verification solves. The verification of concurrent systems poses additional issues, as their analysis requires to evaluate, conceptually, all possible execution orders of their concurrent actions. Petri net unfoldings are a well-established verification technique for concurrent systems. They represent behavior by partial orders, which not only is natural but also efficient for automatic verification. This dissertation focuses on the verification of concurrent systems, employing Petri nets to formalize them, and studies two prominent verification techniques: model checking and fault diagnosis. We investigate the unfoldings of Petri nets extended with read arcs. The unfoldings of these so-called contextual nets seem to be a better representation for systems exhibiting concurrent read access to shared resources: they can be exponentially smaller than conventional unfoldings on these cases. Theoretical and practical contributions are made. We first study the construction of contextual unfoldings, introducing algorithms and data structures that enable their efficient computation. We integrate contextual unfoldings with merged processes, another representation of concurrent behavior that alleviates the explosion caused by non-determinism. The resulting structure, called contextual merged processes, is often orders of magnitude smaller than unfoldings, as we experimentally demonstrate. Next, we develop verification techniques based on unfoldings. We define SAT encodings for the reachability problem in contextual unfoldings, thus solving the problem of detecting cycles of asymmetric conflict. Also, an unfolding-based decision procedure for fault diagnosis under fairness constraints is presented, in this case only for conventional unfoldings. Finally, we implement our verification algorithms, aiming at producing a competitive model checker intended to handle realistic benchmarks. We subsequently evaluate our methods over a standard set of benchmarks and compare them with existing unfolding-based techniques. The experiments demonstrate that reachability checking based on contextual unfoldings outperforms existing techniques on a wide number of cases. This suggests that contextual unfoldings, and asymmetric event structures in general, have a rightful place in research on concurrency, also from an efficiency point of view.

Empresas e instituições de pesquisa nacionais e internacionais tem concentrado esforços no sentido de desenvolver e promover a implementação do padrão internacional ISO 11783, baseado no protocolo de comunicação digital CAN (Contoller Network Area), para integração de dispositivos em máquinas e implementos agrícolas. Nesse contexto, é apresentado o desenvolvimento e a aplicação de um modelo baseado no formalismo das redes de Petri como uma ferramenta de suporte para a análise e implantação de uma rede CAN em aplicações com tempos-críticos. O modelo foi elaborado no ambiente para edição e simulação DesignCPN, sendo que a simulação é utilizada para a análise do desempenho e do comportamento de uma rede CAN com diferentes configurações que será embarcada em um veículo autônomo agrícola (VAA). / Intemational and national research institutions and companies have focused efforts to develop and promote the implementation of the international standard ISO 11783, based upon the digital communication protocol CAN (Controller Area Network), in order to integrate devices in machines and agricultural implements. Therefore, it is presented the development and the application of a model based on Petri nets\' formalism as a tool for the support, analysis and accomplishment of a CAN bus in time-critical applications. The model was constructed in an environrnent for edition and sirnulation of colored Petri nets, the software DesignCPN. The sirnulation was used for the analysis of the behavior and the performance the CAN bus for several configurations, which will be embedded in an Autonomous Agricultural Vehicle (VAA).