O uso de técnicas e métodos formais contribui para o desenvolvimento de sistemas confiáveis. No entanto, apesar do rigor obtido, em geral, é necessário que essas técnicas sejam complementadas com atividades de teste e validação. Deve-se ressaltar que o custo para eliminar erros encontrados nas etapas iniciais de desenvolvimento é menor do que quando esses erros são encontrados nas fases posteriores. Dessa forma, é essencial a condução de atividades de VV&T - Verificação, Validação e Teste - desde as primeiras fases de desenvolvimento. Critérios de teste, como uma forma sistemática de avaliar e/ou gerar casos de teste de qualidade e, dessa forma, contribuir para aumentar a qualidade da atividade de teste, têm sido investigados para o teste de especificação de Sistemas Reativos. A técnica Redes de Petri Coloridas tem sido constantemente utilizada para a especificação do aspecto comportamental de Sistemas Reativos. Apesar de existirem diversas técnicas de análise, um aspecto não considerado é a cobertura alcançada, visto que, em geral, a aplicação exaustiva não é viável devido ao alto custo. Considerando a relevância do estabelecimento de métodos sistemáticos para o teste e validação dessas especificações, este trabalho propõe a aplicação do critério de teste Análise de Mutantes para o teste de Redes de Petri Coloridas. Neste trabalho foram almejados três objetivos principais, os quais podem ser divididos em estudos teóricos, estudos empíricos e automatização. No contexto de estudos teóricos, foi realizada a definição e embasamento teórico para possibilitar a aplicação da Análise de Mutantes no contexto de Redes de Petri Coloridas. Além disso, investigaram-se mecanismos genéricos para a descrição e geração de mutantes. Definiu-se um algoritmo para a geração de casos de teste baseado na Análise de Mutantes. No contexto de estudos empíricos, foram conduzidos estudos de caso para avaliar a aplicabilidade e eficácia dos resultados teóricos obtidos. Finalmente, no contexto de automatização, foram desenvolvidas ferramentas de apoio à aplicação da Análise de Mutantes. / The usage of formal methods and techniques contributes to the development of highly reliable system, but, in spite of the achieved rigour, these techniques must be complemented with testing and validation activities. It should be highlighted that the cost to eliminate errors found in the early phases of development is smaller than when those errors are found in the later phases. Therefore, the accomplishment of VV&T activities - Verification, Validation and Test - starting at the first development phases is essential. Testing criteria, as a systematic way to evaluate and/or generate test cases, contributing, therefore, to improve the quality of the test activity, have been proposed for testing reactive systems specifications. A technique that has been steadily employed for specifying the behavioural aspect of reactive systems is the coloured Petri nets. Although there are several analysis and validation techniques, a usually neglected aspect is the achieved coverage, given that, in general, the exhaustive application is not feasible due to its high cost. Considering the relevance of establishing systematic methods for the test and validation of coloured Petri nets based specification, this work proposes the investigation of the viability of applying Mutation Testing to test coloured Petri nets. In this work three main goals were pursued, which can be grouped in: theoretical studies, empirical studies and tool development. In the context of theoretical studies, it was accomplished the definition of theoretical concepts to enable the application of Mutant Analysis in the context of coloured Petri nets. Moreover, a mutation-based algorithm was defined to generate test sequences for Petri nets. In the context of empirical studies, case studies were carried out to evaluate the applicability and effectiveness of the achieved theoretical results. Finally, in the context of tool development, tools for supporting the application of Mutation Testing were developed.

A arquitetura IP Multimedia Subsystem, proposta pelo consórcio 3rd Generation Partnership Project como base para o suporte à convergência entre telefonia móvel e a Internet, define uma série de elementos arquiteturais, entre os quais, o componente Call Session Control Function e o protocolo Session Initiation Protocol. Session Initiation Protocol é um protocolo da camada de aplicação utilizado para estabelecer, modificar e terminar sessões multimídia entre dispositivos. Em redes baseadas na arquitetura IP Multimedia Subsystem, o Session Initiation Protocol é o responsável pela comunicação entre dispositivos e a rede, e entre os componentes responsáveis pelo gerenciamento de sessão. Nos últimos anos, estudos detectaram degradação de desempenho em redes baseadas na arquitetura IP Multimedia Subsystem em função das características centralizadas do Session Initiation Protocol e dos componentes de gerenciamento de sessão. Este trabalho apresenta uma arquitetura distribuída para redes baseadas em IP Multimedia Subsystem, tendo como fundamento o paradigma de computação paralela baseado em espaço de tuplas onde os servidores são organizados em uma rede P2P, com objetivo de prover uma infraestrutura escalável e tolerante a falhas. A validação da arquitetura em termos de desempenho e escalabilidade se deu através de modelagem formal e simulação com Redes de Petri Coloridas. / The IP Multimedia Subsystem architecture, proposed by the 3rd Generation Partnership Project consortium as basis to support the convergence between mobile networks and the Internet, defines a set of architectural elements, among them, the Call Session Control Function and the Session Initiation Protocol. The Session Initiation Protocol is an application layer protocol used to establish, modify and terminate sessions between devices. On the IP multimedia subsystem based network, the Session Initiation Protocol play a key role on the communication between devices and the network, and between session management components. In the last years, studies have detected a performance bottleneck on IP multimedia subsystem networks due to centralized characteristic of the Session Initiation Protocol and in Session Control components. This work shows a distributed architecture for IP Multimedia Subsystem networks based on the tuple space paradigm, and the servers structured in a P2P network, aiming to achieve a scalable and fault-tolerant infrastructure. The validation of the architecture on the performance and scalability took place through the Coloured Petri Net formal modeling and simulation.

Over the past decade, the ubiquity of business processes and their need for ongoing management in the same manner as other corporate assets has been recognized through the establishment of a dedicated research area: Business Process Management (or BPM). There are a wide range of potential software technologies on which a BPM o®ering can be founded. Although there is signi¯cant variation between these alternatives, they all share one common factor { their execution occurs on the basis of a business process model { and consequently, this ¯eld of technologies can be termed Process-Aware Information Systems (or PAIS). This thesis develops a conceptual foundation for PAIS based on the results of a detailed examination of contemporary o®erings including work°ow and case han- dling systems, business process modelling languages and web service composition languages. This foundation is based on 126 patterns that identify recurrent core constructs in the control-°ow, data and resource perspectives of PAIS. These patterns have been used to evaluate some of the leading systems and business process modelling languages. It also proposes a generic graphical language for de¯ning exception handling strategies that span these perspectives. On the basis of these insights, a comprehensive reference language { newYAWL { is developed for business process modelling and enactment. This language is formally de¯ned and an abstract syntax and operational semantics are provided for it. An assessment of its capabilities is provided through a comprehensive patterns-based analysis which allows direct comparison of its functionality with other PAIS. newYAWL serves as a reference language and many of the ideas embodied within it are also applicable to existing languages and systems. The ultimate goal of both the patterns and newYAWL is to improve the support and applicability of PAIS.

Denial-of-service attacks (DoS) and distributed denial-of-service attacks (DDoS) attempt to temporarily disrupt users or computer resources to cause service un- availability to legitimate users in the internetworking system. The most common type of DoS attack occurs when adversaries °ood a large amount of bogus data to interfere or disrupt the service on the server. The attack can be either a single-source attack, which originates at only one host, or a multi-source attack, in which multiple hosts coordinate to °ood a large number of packets to the server. Cryptographic mechanisms in authentication schemes are an example ap- proach to help the server to validate malicious tra±c. Since authentication in key establishment protocols requires the veri¯er to spend some resources before successfully detecting the bogus messages, adversaries might be able to exploit this °aw to mount an attack to overwhelm the server resources. The attacker is able to perform this kind of attack because many key establishment protocols incorporate strong authentication at the beginning phase before they can iden- tify the attacks. This is an example of DoS threats in most key establishment protocols because they have been implemented to support con¯dentiality and data integrity, but do not carefully consider other security objectives, such as availability. The main objective of this research is to design denial-of-service resistant mechanisms in key establishment protocols. In particular, we focus on the design of cryptographic protocols related to key establishment protocols that implement client puzzles to protect the server against resource exhaustion attacks. Another objective is to extend formal analysis techniques to include DoS- resistance. Basically, the formal analysis approach is used not only to analyse and verify the security of a cryptographic scheme carefully but also to help in the design stage of new protocols with a high level of security guarantee. In this research, we focus on an analysis technique of Meadows' cost-based framework, and we implement DoS-resistant model using Coloured Petri Nets. Meadows' cost-based framework is directly proposed to assess denial-of-service vulnerabil- ities in the cryptographic protocols using mathematical proof, while Coloured Petri Nets is used to model and verify the communication protocols using inter- active simulations. In addition, Coloured Petri Nets are able to help the protocol designer to clarify and reduce some inconsistency of the protocol speci¯cation. Therefore, the second objective of this research is to explore vulnerabilities in existing DoS-resistant protocols, as well as extend a formal analysis approach to our new framework for improving DoS-resistance and evaluating the performance of the new proposed mechanism. In summary, the speci¯c outcomes of this research include following results; 1. A taxonomy of denial-of-service resistant strategies and techniques used in key establishment protocols; 2. A critical analysis of existing DoS-resistant key exchange and key estab- lishment protocols; 3. An implementation of Meadows's cost-based framework using Coloured Petri Nets for modelling and evaluating DoS-resistant protocols; and 4. A development of new e±cient and practical DoS-resistant mechanisms to improve the resistance to denial-of-service attacks in key establishment protocols.

This thesis investigates a method for tackling the verification of parametric systems, systems whose behaviour may depend on the value of one or more parameters. The range of allowable values for such parameters may, in general, be large or unknown. This results in a large number of instances of a system that require verification, one instance for each allowable combination of parameter values. When one or more parameters are unbounded, the family of systems that require verification becomes infinite. Computer protocols are one example of such parametric systems. They may have parameters such as the maximum sequence number or the maximum number of retransmissions. Traditional protocol verification approaches usually only analyse and verify properties of a parametric system for a small range of parameter values. It is impossible to verify in this way every concrete instance of an infinite family of systems. Also, the number of reachable states tends to increase dramatically with increasing parameter values, and thus the well known state explosion phenomenon also limits the range of parameters for which the system can be analysed. In this thesis, we concentrate on the parametric verification of the Stop-and-Wait Protocol (SWP), an elementary flow control protocol. We have used Coloured Petri Nets (CPNs) to model the SWP, operating over an in-order but lossy medium, with two unbounded parameters: the maximum sequence number; and the maximum number of retransmissions. A novel method has been used for symbolically representing the parametric reachability graph of our parametric SWP CPN model. This parametric reachability graph captures exactly the infinite family of reachability graphs resulting from the infinite family of SWP CPNs. The parametric reachability graph is represented symbolically as a set of closed-form algebraic expressions for the nodes and arcs of the reachability graph, expressed in terms of the two parameters. By analysing the reachability graphs of the SWP CPN model for small parameter values, structural regularities in the reachability graphs were identified and exploited to develop the appropriate algebraic expressions for the parametric reachability graph. These expressions can be analysed and manipulated directly, thus the properties that are verified from these expressions are verified for all instances of the system. Several properties of the SWP that are able to be verified directly from the parametric reachability graph have been identified. These include a proof of the size of the parametric reachability graph in terms of both parameters, absence of deadlocks (undesired terminal states), absence of livelocks (undesirable cycles of behaviour from which the protocol cannot escape), absence of dead transitions (actions that can never occur) and the upper bounds on the content of the underlying communication channel. These are verified from the algebraic expressions and thus hold for all parameter values. Significantly, language analysis is also carried out on the parametric SWP. The parametric reachability graph is translated into a parametric Finite State Automaton (FSA), capturing symbolically the infinite set of protocol languages (i.e. sequences of user observable events) by means of similar algebraic expressions to those of the parametric reachability graph. Standard FSA reduction techniques were applied in a symbolic fashion directly to the parametric FSA, firstly to obtain a deterministic representation of the parametric FSA, then to obtain an equivalent minimised FSA. It was found that the determinisation procedure removed the effect of the maximum number of retransmissions parameter, and the minimisation procedure removed the effect of the maximum sequence number parameter. Conformance of all instances of the SWP over both parameters to its desired service language is proved. The development of algebraic expressions to represent the infinite class of Stop-and-Wait Protocols, and the verification of properties (including language analysis) directly from these algebraic expressions, has demonstrated the potential of this method for the verification of more general parametric systems. This thesis provides a significant contribution toward the development of a general parametric verification methodology.

Made available in DSpace on 2015-05-08T14:53:27Z (GMT). No. of bitstreams: 1 arquivototal.pdf: 2050762 bytes, checksum: d03ea0191257aa516c9df03c51af0335 (MD5) Previous issue date: 2011-09-26 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / This study proposes a systematic method for evaluating the performance of service delivery through process modeling and failure analysis. The implementation of the proposal took place in a distribution company of electricity (COELCE), in which he was elected New Process Connections as an object of study for the following reasons: This process helps to reduce the deficit of households without electricity in the country and showed a high rate of irregularities pointed out by regulators from providing that service here has to justify the choice of process and not the company. This is a case study, with secondary data were collected in books, websites, internal documents COELCE and scientific publications (journals, dissertations and theses). We obtained the primary data in reading and statistical analysis of company documents to the investigator assigned by the managers of the process, meetings with experts COELCE before, during and after field research, and intensive direct observation of the teams responsible for the physical connections of the units consumers. The methodology proposed by the tool is composed of colored Petri nets for modeling process New Links and techniques of failure analysis (FTA Fault Tree Analysis) and FMEA (Failure Mode and Effects Analysis). The systematic validation enabled: first - viewing different phases and activities of the process; second - identification of critical functions and potential failure of the process, the third - the formulation of action plan by the researcher to improve the process of New Connections. The action plan was endorsed by the group of experts COELCE, which collaborates with the research, from the exploratory phase. The use of integrated techniques proposed in this paper contributes to scientific knowledge by using the approach of process modeling and analysis techniques of failures in service businesses, especially in regard to the reduced number of work in this area. It is noteworthy that the systematics can be applied to other companies in the services sector can contribute in improving the performance of the processes analyzed. / Este estudo propõe uma sistemática para avaliar o desempenho da prestação de serviços por meio da modelagem de processos e análise de falha. A aplicação da proposta ocorreu em uma empresa de distribuição de energia elétrica (COELCE), na qual elegeu-se o Processo de Novas Ligações como objeto de estudo pelos seguintes motivos: esse processo contribui para reduzir o déficit de domicílios sem energia elétrica no país e apresentava elevado índice de irregularidades apontadas pelos órgãos reguladores da prestação desse serviço público. Trata-se de um estudo de caso cujos dados secundários foram coletados em livros, sites, documentos internos da COELCE e publicações científicas (periódicos, dissertações e teses). Obteve-se os dados primários em leitura e tratamento estatístico de documentos da empresa cedidos ao pesquisador pelos gestores do processo, reuniões com especialistas da COELCE, antes, durante e após pesquisa de campo, e observação direta intensiva das equipes responsáveis pelas ligações físicas das unidades consumidoras. A sistemática proposta é composta pela ferramenta redes de Petri Coloridas para modelagem do Processo de Novas Ligações e as técnicas de análise de falhas FTA (Fault Tree Analysis) e FMEA (Failure Mode and Effects Analysis). A validação da sistemática permitiu: primeiro - visualização de diferentes fases e atividades do processo; segundo identificação de funções críticas e falhas potenciais do processo; terceiro - formulação de plano de ação pelo pesquisador para melhoria do Processo de Novas Ligações. O plano de ação foi validado pelo grupo de especialistas da COELCE, que colabora com a pesquisa, desde a fase exploratória. A utilização das técnicas de forma integrada proposta neste trabalho contribui para o conhecimento científico por utilizar a abordagem de modelagem de processos e técnicas de análise de falhas em empresas de serviço, principalmente no que tange ao reduzido número de trabalho nesta área. Vale ressaltar que a sistemática pode ser aplicada em outras empresas do setor de serviços podendo contribuir na melhoria do desempenho dos processos analisados.

Made available in DSpace on 2015-03-03T15:08:46Z (GMT). No. of bitstreams: 1 RicardoWA.pdf: 1646499 bytes, checksum: efcc744c6ff7cea26befa0adbedb8c6a (MD5) Previous issue date: 2005-09-02 / Este trabalho apresenta uma t?cnica de verifica??o formal de Sistemas de Racioc?nio Procedural, PRS (Procedural Reasoning System), uma linguagem de programa??o que utiliza a abordagem do racioc?nio procedural. Esta t?cnica baseia-se na utiliza??o de regras de convers?o entre programas PRS e Redes de Petri Coloridas (RPC). Para isso, s?o apresentadas regras de convers?o de um sub-conjunto bem expressivo da maioria da sintaxe utilizada na linguagem PRS para RPC. A fim de proceder fia verifica??o formal do programa PRS especificado, uma vez que se disponha da rede de Petri equivalente ao programa PRS, utilizamos o formalismo das RPCs (verifica??o das propriedades estruturais e comportamentais) para analisarmos formalmente o programa PRS equivalente. Utilizamos uma ferramenta computacional dispon?vel para desenhar, simular e analisar as redes de Petri coloridas geradas. Uma vez que disponhamos das regras de convers?o PRS-RPC, podemos ser levados a querer fazer esta convers?o de maneira estritamente manual. No entanto, a probabilidade de introdu??o de erros na convers?o ? grande, fazendo com que o esfor?o necess?rio para garantirmos a corretude da convers?o manual seja da mesma ordem de grandeza que a elimina??o de eventuais erros diretamente no programa PRS original. Assim, a convers?o automatizada ? de suma import?ncia para evitar que a convers?o manual nos leve a erros indesej?veis, podendo invalidar todo o processo de convers?o. A principal contribui??o deste trabalho de pesquisa diz respeito ao desenvolvimento de uma t?cnica de verifica??o formal automatizada que consiste basicamente em duas etapas distintas, embora inter-relacionadas. A primeira fase diz respeito fias regras de convers?o de PRS para RPC. A segunda fase ? concernente ao desenvolvimento de um conversor para fazer a transforma??o de maneira automatizada dos programas PRS para as RPCs. A convers?o autom?tica ? poss?vel, porque todas as regras de convers?o apresentadas seguem leis de forma??o gen?ricas, pass?veis de serem inclu?das em algoritmos

O uso de técnicas e métodos formais contribui para o desenvolvimento de sistemas confiáveis. No entanto, apesar do rigor obtido, em geral, é necessário que essas técnicas sejam complementadas com atividades de teste e validação. Deve-se ressaltar que o custo para eliminar erros encontrados nas etapas iniciais de desenvolvimento é menor do que quando esses erros são encontrados nas fases posteriores. Dessa forma, é essencial a condução de atividades de VV&T - Verificação, Validação e Teste - desde as primeiras fases de desenvolvimento. Critérios de teste, como uma forma sistemática de avaliar e/ou gerar casos de teste de qualidade e, dessa forma, contribuir para aumentar a qualidade da atividade de teste, têm sido investigados para o teste de especificação de Sistemas Reativos. A técnica Redes de Petri Coloridas tem sido constantemente utilizada para a especificação do aspecto comportamental de Sistemas Reativos. Apesar de existirem diversas técnicas de análise, um aspecto não considerado é a cobertura alcançada, visto que, em geral, a aplicação exaustiva não é viável devido ao alto custo. Considerando a relevância do estabelecimento de métodos sistemáticos para o teste e validação dessas especificações, este trabalho propõe a aplicação do critério de teste Análise de Mutantes para o teste de Redes de Petri Coloridas. Neste trabalho foram almejados três objetivos principais, os quais podem ser divididos em estudos teóricos, estudos empíricos e automatização. No contexto de estudos teóricos, foi realizada a definição e embasamento teórico para possibilitar a aplicação da Análise de Mutantes no contexto de Redes de Petri Coloridas. Além disso, investigaram-se mecanismos genéricos para a descrição e geração de mutantes. Definiu-se um algoritmo para a geração de casos de teste baseado na Análise de Mutantes. No contexto de estudos empíricos, foram conduzidos estudos de caso para avaliar a aplicabilidade e eficácia dos resultados teóricos obtidos. Finalmente, no contexto de automatização, foram desenvolvidas ferramentas de apoio à aplicação da Análise de Mutantes. / The usage of formal methods and techniques contributes to the development of highly reliable system, but, in spite of the achieved rigour, these techniques must be complemented with testing and validation activities. It should be highlighted that the cost to eliminate errors found in the early phases of development is smaller than when those errors are found in the later phases. Therefore, the accomplishment of VV&T activities - Verification, Validation and Test - starting at the first development phases is essential. Testing criteria, as a systematic way to evaluate and/or generate test cases, contributing, therefore, to improve the quality of the test activity, have been proposed for testing reactive systems specifications. A technique that has been steadily employed for specifying the behavioural aspect of reactive systems is the coloured Petri nets. Although there are several analysis and validation techniques, a usually neglected aspect is the achieved coverage, given that, in general, the exhaustive application is not feasible due to its high cost. Considering the relevance of establishing systematic methods for the test and validation of coloured Petri nets based specification, this work proposes the investigation of the viability of applying Mutation Testing to test coloured Petri nets. In this work three main goals were pursued, which can be grouped in: theoretical studies, empirical studies and tool development. In the context of theoretical studies, it was accomplished the definition of theoretical concepts to enable the application of Mutant Analysis in the context of coloured Petri nets. Moreover, a mutation-based algorithm was defined to generate test sequences for Petri nets. In the context of empirical studies, case studies were carried out to evaluate the applicability and effectiveness of the achieved theoretical results. Finally, in the context of tool development, tools for supporting the application of Mutation Testing were developed.

Made available in DSpace on 2016-06-02T19:05:53Z (GMT). No. of bitstreams: 1 3978.pdf: 2293519 bytes, checksum: bebf48e9b57957fa077811d04a5d672e (MD5) Previous issue date: 2010-06-29 / Financiadora de Estudos e Projetos / A Flexible Manufacturing System is a production system where more than one event can occur simultaneously in parallel, asynchronously or concurrently. These are designed to meet the needs of the market, demand for improved product quality, lower costs and shorter delivery times. Due to the complexity and flexibility of these systems, conflicts can occur when more than one process requests the same resource, such as machines or AGVs, or when a product can be produced in more than one production routing. Thus, a conflict resolution policy is needed in this type of environment. This study uses Fuzzy Coloured Petri Nets for modeling a manufacturing system. The manufacturing system is modeled considering the resources, buffers, production routings, AGV routes and identifying conflict points. The conflict resolution is performed considering both information on the shop floor and production management. Fuzzy rules are constructed to prioritize conflicting processes and a fuzzy rule-based system is modeled on Fuzzy Coloured Petri Nets in the same network as the manufacturing system, making the model of the system independent of other systems of support for the resolution of conflicts. In this work we considered the conflicts that can occur when loading and unloading station and the input and output buffer. According to the source of conflict, a rule base is shaped to assign priorities to processes. From this model it is possible to make the control system and ensure that identified conflicts are resolved. / Um Sistema Flexível de Manufatura é um sistema de produção onde mais de um evento pode ocorrer ao mesmo tempo de forma paralela, assíncrona ou de forma concorrente. Estes foram projetados para atender às necessidades do mercado, que demanda por melhor qualidade dos produtos, redução de custos e prazos de entrega menores. Devido à complexidade e à flexibilidade destes sistemas, conflitos podem ocorrer quando mais de um processo requisita o mesmo recurso, como máquinas ou AGVs, ou quando um produto pode ser produzido em roteiros distintos. Assim, uma política de solução de conflito é necessária neste tipo de ambiente. Este trabalho usa Redes de Petri Coloridas Fuzzy para modelar um sistema de manufatura. O sistema de manufatura é modelado considerando os recursos, buffers, roteiros de produção, rotas dos AGV e identificando os pontos de conflitos. A resolução dos conflitos é realizada considerando tanto informações do chão de fábrica quanto da gestão da produção. Regras fuzzy são construídas para atribuir prioridades aos processos conflitantes e um sistema baseado em regras fuzzy é modelado em Redes de Petri Coloridas Fuzzy na mesma rede do sistema de manufatura, tornado o modelo do sistema independente de outros sistemas de apoio para a solução dos conflitos. Neste trabalho foram considerados os conflitos que podem ocorrer na estação de carga e descarga e nos buffer de entrada e saída. De acordo com o ponto de conflito, uma base de regras é modelada para atribuir prioridades aos processos. A partir desta modelagem é possível realizar o controle do sistema e garantir que os conflitos identificados sejam resolvidos.

CoordenaÃÃo de AperfeÃoamento de Pessoal de NÃvel Superior / This work presents a method to generate games with multilevel and multiple users using Hierarchical Coloured Petri Nets. The design of a multiuser game containing multiple navigation environments (multilevel) is made from the model of a Hierarchical Coloured Petri Net, in which are specified all of the rules, properties and structures of the game. The created model for the game can be formally analysed, verifying the existence of deadlocks and invalid paths, for example, and others possible conception problems, that can be done with the tools available on CPN Tools. To validate this method, a tool has been developed, called CPN Games, which allows fast and dynamic development of simple conception games only using Hierarchical Coloured Petri Nets. The XML codes of the designed models in CPN Tools are interpreted by CPN Games following a set of predefined rules to instantiate different games, without additional programing. It is demonstrated the mechanisms of the design, analysis and validation of the models and finally it is presented several examples of games developed by this tool. / Este trabalho apresenta um mÃtodo para geraÃÃo de jogos multinÃveis e com mÃltiplos usuÃrios por meio de modelagem em Redes de Petri Coloridas HierÃrquicas. A concepÃÃo de um jogo multiusuÃrio, contendo mÃltiplos ambientes de navegaÃÃo (multinÃveis), à feita a partir da criaÃÃo de um modelo hierÃrquico em Rede de Petri Colorida, no qual se especificam todas as regras, propriedades e estruturas do jogo. O modelo criado para o jogo pode ser analisado formalmente, verificando-se, por exemplo, a existÃncia de bloqueios e de transiÃÃes mortas (caminhos invÃlidos), entre outros possÃveis problemas de concepÃÃo, o que pode ser feito com a utilizaÃÃo de ferramentas disponÃveis no CPN Tools. Para validar esse mÃtodo, foi concebida uma ferramenta, denominada CPN Games, que permite o desenvolvimento rÃpido e dinÃmico de jogos de concepÃÃo simples exclusivamente por Rede de Petri Colorida HierÃrquica. Os cÃdigos em XML de modelos constituÃdos com o CPN Tools sÃo interpretadas pelo CPN Games seguindo um conjunto de regras prà estabelecidas para instanciar diferentes jogos, sem a necessidade de programaÃÃo adicional. SÃo demonstrados os mecanismos de criaÃÃo, anÃlise e validaÃÃo dos modelos e diferentes exemplos de jogos construÃdos com a ferramenta.