In this work, an approach based on Deadlock avoidance of Interorganizational Work-Flow nets is proposed to deal with these situations. Interorganizational business processes are modeled by Interorganizational WorkFlow nets. Deadlock situations in interorganizational business processes come generally related to losses during message exchanges between several business processes. Within the Petri net theory, a Deadlock situation is characterized by the presence of a siphon that can be empty. After detecting and controlling the Siphon structures that lead to Deadlock situations in Interorganizational WorkFlow nets, a method for the design of Interorganizational WorkFlow nets free of Deadlock is proposed. In particular, the basic principle is to dene new Work- Flow nets shared among the original work ow processes that allow one to remove the scenarios responsible for the Deadlocks. / Neste trabalho e proposta uma abordagem baseada na prevenção de deadlocks em WorkFlow nets Interorganizacionais para lidar com situações dessa natureza. Processos de negocio interorganizacionais são modelados por work ows interorganizacionais. Situações de deadlock nos processos de negocio interorganizacionais geralmente estão relacionadas a perdas durante trocas de mensagens entre varios processos de negocio. Dentro da teoria das redes de Petri, uma situação de deadlock e caracterizada pela presenca de um sifão que pode car vazio. Depois de detectar e controlar as estruturas de sifão que levam as situações de deadlock nas WorkFlow nets Interorganizacionais, e proposta uma arquitetura distribuda para modelar as WorkFlow nets Interorganizacionais livre de deadlock. Em particular, o princpio basico consiste em denir novas WorkFlow nets compartilhadas entre os work ows originais que permitem remover os cenarios responsaveis pelos deadlocks. / Mestre em Ciência da Computação

Orientadores: Luiz Eduardo Buzato, Edmundo Roberto Mauro Madeira / Tese (doutorado) - Universidade Estadual de Campinas, Instituto de Computação / Made available in DSpace on 2018-08-16T20:16:50Z (GMT). No. of bitstreams: 1 Cicerre_FabioRodrigodeLima_D.pdf: 1417286 bytes, checksum: 642d37f1cb522ec4a356bbb4e9b55b96 (MD5) Previous issue date: 2010 / Resumo: O conceito de grade surgiu com a necessidade crescente de se aproveitar recursos computacionais disponíveis em uma ou mais organizações para resolver problemas que exigem compartilhamento de dados e um grande poder de processamento. Uma grade computacional tem como objetivo principal permitir a execução distribuída e paralela de tarefas em recursos compartilhados. Uma grade é constituída de infra-estrutura física, composta de uma ou mais redes autônomas de computadores, e de um sistema de suporte (middleware), que provê serviços de gerenciamento de informações sobre os recursos da grade, controle de acesso e execução de tarefas sobre esse recursos e mecanismos de comunicação. Atualmente existem diversos sistemas que suportam a execução de tarefas independentes em uma grade computacional, mas poucos consideram a execução de processos de workflow, que permitem a definição de dependência explícita de dados e controle entre tarefas, o que impede um melhor aproveitamento de recursos, escalabilidade, desempenho de execução e recuperação automática de processos com manutenção de consistência. O sistema Xavantes, proposto e descrito nesse trabalho, procura suprir essas deficiências, tendo como principal objetivo suportar a execução distribuída de processos de workflow em máquinas heterogêneas, em uma ou mais organizações autônomas e dinâmicas, provendo um middleware que forneça uma melhor escalabilidade, desempenho e confiabilidade para a execução de aplicações em grades computacionais / Abstract: The grid concept has emerged from the increasing necessity of using available computational resources in one or more organizations in order to solve problems that require data sharing and large processing power. The main goal of a computational grid is to allow the distributed and parallel execution of tasks in shared resources. A grid is composed of a physical infra-structure, with one or more autonomous networks of computers, and a middleware, which provides services of information management about the grid resources, access control and tasks execution in these resources and communication mechanisms. Nowadays, there are some systems that support the execution of independent tasks in a computational grid, but only ones consider the execution of workflow processes, which allow the explicit definition of data and control dependencies among tasks, and this restricts a better use of available resources, scalability, execution performance, and automatic recovery of processes with the correct consistency maintenance. The Xavantes system, proposed and described in this work, is designed to reduce these deficiencies, having as its main goal the supports to the distributed execution of workflows in heterogeneous resources of one or more autonomous and dynamic organizations, providing a middleware that delivers a better scalability, performance and reliability to the application execution in grid computing / Doutorado / Sistemas Distribuídos e Redes de Computadores / Doutor em Ciência da Computação

Orientador: Edmundo Roberto Mauro Madeira / Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Computação / Made available in DSpace on 2018-08-06T12:20:00Z (GMT). No. of bitstreams: 1 Bittencourt_LuizFernando_M.pdf: 1217558 bytes, checksum: dcbdeb1eaf538ae17a83304451a73126 (MD5) Previous issue date: 2006 / Resumo: Uma grade computacional é um sistema heterogêneo colaborativo, geograficamente distribuído, multi-institucional e dinâmico, onde qualquer recurso computacional ligado a uma rede, local ou não, é um potencial colaborador. Grades computacionais são atualmente um grande foco de estudos relacionados à execução de aplicações paralelas, tanto aquelas que demandam grande poder computacional quanto aquelas que se adaptam bem a ambientes distribuídos. Como os recursos de uma grade pertencem a vários domínios administrativos diferentes com políticas diferentes, cada recurso tem autonomia para participar ou deixar de participar da grade em qualquer momento. Essa característica dinâmica e a heterogeneidade tornam o escalonamento de aplicações, a gerência de recursos e a tolerância a falhas grandes desafios nesses sistemas. Particularmente, o escalonamento desempenha um papel de suma importância, pois é determinante no tempo de execução das aplicações. O escalonamento de tarefas é um problema NP-Completo [6], o que levou ao desenvolvimento de uma heurística para o problema de otimização associado. Neste trabalho apresentamos um escalonador de tarefas em grades computacionais baseado no Xavantes [3], um middleware que oferece suporte a execução de tarefas dependentes através de estruturas de controle hierárquicas chamadas controladores. O algoritmo desenvolvido, chamado de Path Clustering Heuristic (PCH), agrupa as tarefas com o objetivo de minimizar a comunicação entre os controladores e as tarefas, diminuindo o tempo de execução total do processo / Abstract: A computational grid is a collaborative heterogeneous, geographically distributed, multiinstitutional and dynamic system, where any computational resource with a network connection, local or remote, is a potential collaborator. In computational grids, problems related to the execution of parallel applications, those which need a lot of computational power, as well as those which fit well in distributed environments, are wide studied nowadays. As the grid resources belong to various different administrative domains with different policies, each resource has the autonomy to participate or leave the grid at any time. These dynamic and heterogeneous characteristics make the application scheduling, the resource management and the fault tolerance relevant issues on these systems. Particularly, the scheduler plays an important role, since it is determinative in the execution time of an application. The task scheduling problem is NP-Complete [6], what led to the development of a heuristic for the associated optimization problem. In this work we present a task scheduler for a computational grid based on Xavantes [3], a middleware that supports dependent task execution through control structures called controllers. The developed algorithm, called Path Clustering Heuristic (PCH), clusterizes tasks aiming to minimize the communication between controllers and tasks, reducing the process execution time / Mestrado / Sistemas de Computação / Mestre em Ciência da Computação

Orientador: Edmundo Roberto Mauro Madeira / Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Computação / Made available in DSpace on 2018-08-09T11:43:09Z (GMT). No. of bitstreams: 1 Senna_CarlosRoberto_M.pdf: 1604896 bytes, checksum: 4d91ce46c46772043ce75490d16c3b98 (MD5) Previous issue date: 2007 / Resumo: No ambiente colaborativo das grades computacionais são poucas as ferramentas para gerência de processos e serviços orientadas ao usuário. Esta dissertação apresenta o Grid Process Orchestration (GPO), uma infraestrutura que faz orquestração de serviços e processos em grades computacionais, permitindo ao usuário criar e gerenciar ?uxos complexos, com tarefas fortemente acopladas, sem suporte adicional. O GPO é baseado na OGSA (Open Grid Services Architecture) e descreve os ?uxos usando o conceito de orquestra¸ao de serviços Web aplicados aos serviços das Grades Computacionais. A dissertação descreve a arquitetura da infraestrutura proposta, detalha seus principais componentes, suas funcionalidades para gerência de ?uxos e alguns aspectos do protótipo implementado. Além disso, propõe uma linguagem compacta para descrever os work?ows. Uma aplicação exemplo é apresentada ilustrando as facilidades da infraestrutura proposta / Abstract: In the collaborative environment of the Computational Grids, there are few tools used for process management and user guide services. This work presents the Grid Process Orchestration (GPO), an infrastructure for service and process orchestration in computational grids, which allows to create and manage complex work?ows composed of strongcoupled jobs with no additional support. The GPO is based on the Open Grid Services Architecture (OGSA) and describes work?ows using Web Services orchestration concepts applied to computational grid services. This work describes the architecture of the proposed infrastructure, detailing its main components, functionalities for ?ow management, and shows an implemented prototype. In addition to the architecture, it proposes a compact language for describing work?ows. An application example is presented to illustrate the facilities of the proposed infrastructure / Mestrado / Redes de Computadores / Mestre em Ciência da Computação

Orientador: Claudia Maria Bauzer Medeiros / Tese (doutorado) - Universidade Estadual de Campinas, Instituto de Computação / Made available in DSpace on 2018-08-15T04:11:30Z (GMT). No. of bitstreams: 1 Macario_CarlaGeovanadoNascimento_D.pdf: 3780981 bytes, checksum: 4b8ad7138779392bff940f1f95ad1f51 (MD5) Previous issue date: 2009 / Resumo: Dados geoespaciais constituem a base para sistemas de decisão utilizados em vários domínios, como planejamento de transito, fornecimento de serviços ou controle de desastres. Entretanto, para serem usados, estes dados precisam ser analisados e interpretados, atividades muitas vezes trabalhosas e geralmente executadas por especialistas. Apesar disso estas interpretacoes nao sao armazenadas e quando o são, geralmente correspondem a alguma informacao textual e em linguagem própria, gravadas em arquivos tecnicos. A ausencia de solucoes eficientes para armazenar estas interpretaçães leva a problemas como retrabalho e dificuldades de compartilhamento de informação. Neste trabalho apresentamos uma soluçao para estes problemas que baseia-se no uso de anotações semânticas, uma abordagem que promove um entendimento comum dos conceitos usados. Para tanto, propomos a adocão de workflows científicos para descricao do processo de anotacão dos dados e tambíem de um esquema de metadados e ontologias bem conhecidas, aplicando a soluçao a problemas em agricultura. As contribuicães da tese envolvem: (i) identificacao de um conjunto de requisitos para busca semantica a dados geoespaciais; (ii) identificacao de características desejóveis para ferramentas de anotacão; (iii) proposta e implementacao parcial de um framework para a anotacão semântica de diferentes tipos de dados geoespaciais; e (iv) identificacao dos desafios envolvidos no uso de workflows para descrever o processo de anotaçcaão. Este framework foi parcialmente validado, com implementação para aplicações em agricultura / Abstract: Geospatial data are a basis for decision making in a wide range of domains, such as traffic planning, consumer services disasters controlling. However, to be used, these kind of data have to be analyzed and interpreted, which constitutes a hard task, prone to errors, and usually performed by experts. Although all of these factors, the interpretations are not stored. When this happens, they correspond to descriptive text, which is stored in technical files. The absence of solutions to efficiently store them leads to problems such as rework and difficulties in information sharing. In this work we present a solution for these problems based on semantic annotations, an approach for a common understanding of concepts being used. We propose the use of scientific workflows to describe the annotation process for each kind of data, and also the adoption of well known metadata schema and ontologies. The contributions of this thesis involves: (i) identification of requirements for semantic search of geospatial data; (ii) identification of desirable features for annotation tools; (iii) proposal, and partial implementation, of a a framework for semantic annotation of different kinds of geospatial data; and (iv) identification of challenges in adopting scientific workflows for describing the annotation process. This framework was partially validated, through an implementation to produce annotations for applications in agriculture / Doutorado / Banco de Dados / Doutora em Ciência da Computação

Submitted by Raul Bezerra (raul.bezerra@hotmail.com) on 2016-03-28T19:03:48Z No. of bitstreams: 1 Dissertacao_RaulBezerra_MEX_2014_28MAR16.pdf: 5114761 bytes, checksum: 4fefb9faa63eb88b89ab980f19a1c993 (MD5) / Approved for entry into archive by ÁUREA CORRÊA DA FONSECA CORRÊA DA FONSECA (aurea.fonseca@fgv.br) on 2016-05-13T14:34:05Z (GMT) No. of bitstreams: 1 Dissertacao_RaulBezerra_MEX_2014_28MAR16.pdf: 5114761 bytes, checksum: 4fefb9faa63eb88b89ab980f19a1c993 (MD5) / Approved for entry into archive by Maria Almeida (maria.socorro@fgv.br) on 2016-05-16T16:39:49Z (GMT) No. of bitstreams: 1 Dissertacao_RaulBezerra_MEX_2014_28MAR16.pdf: 5114761 bytes, checksum: 4fefb9faa63eb88b89ab980f19a1c993 (MD5) / Made available in DSpace on 2016-05-16T16:40:03Z (GMT). No. of bitstreams: 1 Dissertacao_RaulBezerra_MEX_2014_28MAR16.pdf: 5114761 bytes, checksum: 4fefb9faa63eb88b89ab980f19a1c993 (MD5) Previous issue date: 2015-12-01 / Implement a Shared Services Center (SSC) is a practice currently used by both Brazilian companies and in other countries to standardize processes, optimize resources and reduce costs, allowing its operating units are engaged in their activities end, leaving ordinary activities (transactional ) in support of SSC and responsibility. On the other hand, the areas of Environment, Occupational Health and Safety (EHS) have an important role in most companies, given that the management of the health and safety of the company's employees are under their responsibility. The objective of this study is to analyze the feasibility and identify the activities for integrating the results related to EHS in a Shared Services Center (SSC). To meet this goal, we chose to adopt as a research methodology, in addition to literature review, a case study in a multinational company operating in the mining segments, Logistics, Energy, Oil and Gas and Entertainment. The data collected allowed a comparison between the studied literature and the case study. The results showed that the mapping of the processes EHS area was essential to challenge existing processes, generating organizational performance improvement opportunities to identify critical interfaces and, above all, basis for creating SAP implementation. This structured process mapping allowed also reduce costs in product development and services, integration gaps between areas and promote improvement of organizational performance, and is an excellent tool for better understanding of the current processes and elimination or simplification of those in need changes. / Implantar um Centro de serviços Compartilhados (CSC) é uma prática atualmente utilizada tanto por empresas brasileiras quanto em outros países para padronizar processos, otimizar recursos e reduzir custos, permitindo que suas unidades operacionais se dediquem as suas atividades fim, deixando as atividades comuns (transacionais) sob suporte e responsabilidade do CSC. De outro lado, as áreas de Saúde Ocupacional e Meio Ambiente (SSMA) têm importante papel em grande parte das empresas, tendo em vista que a gestão da saúde e segurança dos empregados da empresa está sob sua responsabilidade. O objetivo deste trabalho é analisar a viabilidade e identificar os resultados da inserção de atividades relacionadas à SSMA em um Centro de Serviços Compartilhados (CSC). Para cumprir esse objetivo, optou-se por adotar como metodologia de pesquisa, além do levantamento bibliográfico, um estudo de caso em uma empresa multinacional atuante nos segmentos de Mineração, Logística, Energia, Óleo e Gás e Entretenimento. Os dados coletados permitiram uma comparação entre a bibliografia pesquisada e o estudo de caso realizado. Os resultados mostraram que o mapeamento dos processos da área de SSMA foi essencial para desafiar os processos existentes, gerando oportunidades de melhoria de desempenho organizacional ao identificar interfaces críticas e, sobretudo, criar bases para implantação do SAP. Este mapeamento estruturado de processos permitiu, ainda, reduzir custos no desenvolvimento de produtos e serviços, falhas de integração entre áreas e promover melhoria de desempenho organizacional, além de ser uma excelente ferramenta para o melhor entendimento dos processos atuais e eliminação ou simplificação dos que necessitam de mudanças.

Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / This work presents a method for qualitative and quantitative analysis of WorkFlow nets based on the proof trees of linear logic, and an approach for the verification of workflow specifications in UML through the transformation of UML Activity Diagrams into WorkFlow nets. The qualitative analysis is concerned with the proof of soundness correctness criterion defined for WorkFlow nets. The quantitative analysis is based on the computation of symbolic dates for the planning of resources used to handle each task of the workflow process modeled by a t-Time WorkFlow net. For the verification of the specifications of workflow processes mapped into UML Activity Diagrams are presented formal rules to transform this ones into WorkFlow nets. In this context is proposed the analysis and correction of critical points in UML Activity Diagrams through the analysis of proof trees of linear logic. The advantages of such an approach are diverse. The fact of working with linear logic permits one to prove the correctness criterion soundness in a linear time without considering the construction of the reachability graph, considering the proper structure of the WorkFlow net instead of considering the corresponding automata. Moreover, the computation of symbolic dates for the execution of each task mapped into the t-Time WorkFlow net permits to plan the utilization of the resources involved in the activities of the workflow process, through formulas that can be used for any case handled by the correspondent workflow process, without to examine again the process to recalculate, for each new case, the dates of start and conclusion for the activities involved in the process. Regarding the verification of workflow processes mapped into UML Activity Diagrams, the major advantage of this approach is the transformation of a semi-formal model into a formal model, such that some properties, like soundness, can be formally verified. / Este trabalho apresenta um método para a análise qualitativa e quantitativa de Work- Flow nets baseado nas árvores de prova canônica da lógica linear e uma abordagem para a verificação de especificações de processos de workflow em UML através da transformação de Diagramas de Atividades da UML em WorkFlow nets. A análise qualitativa refere-se à prova do critério de corretude soundness definido para WorkFlow nets. Já a análise quantitativa preocupa-se com o planejamento de recursos para cada atividade de um processo de workflow mapeado em uma t-Time WorkFlow net e baseia-se no cálculo de datas simbólicas para o planejamento de recursos utilizados na realização de cada tarefa do processo de workflow. Para a verificação das especificações de processos de workflow mapeados em Diagramas de Atividades da UML são apresentadas regras formais para transformar estes diagramas em WorkFlow nets. Neste contexto também é proposta a análise e correção de pontos críticos em Diagramas de Atividades da UML através da análise de árvores de prova canônica da lógica linear. As vantagens das abordagens apresentadas neste trabalho são diversas. O fato de trabalhar com lógica linear permite provar o critério de corretude soundness em tempo linear e sem que seja necessária a construção de um grafo das marcações acessíveis, considerando diretamente a própria estrutura da WorkFlow net, ao invés de considerar o seu autômato correspondente. Além disso, o cálculo de datas simbólicas correspondentes à execução de cada tarefa mapeada em uma t-Time WorkFlow net permite planejar a utilização dos recursos envolvidos nas atividades do processo de workflow, através de fórmulas que podem ser utilizadas por qualquer caso tratado pelo processo de workflow correspondente, sem que seja necessário percorrer novamente o processo de workflow inteiro para recalcular, para cada novo caso, datas de início e término das atividades envolvidas no processo. Já no que diz respeito à verificação de processos de workflow mapeados em Diagramas de Atividades da UML, a principal vantagem desta abordagem é a transformação de um modelo semi-formal em um modelo formal, para o qual algumas propriedades, como soundness, podem ser formalmente verificadas. / Mestre em Ciência da Computação

Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / This work formalizes four methods based on Linear Logic for the verification of interorganizational workflow processes modelled by Interorganizational Workflow nets, which are Petri nets that model such processes. The first method is related to the verification of the Soundness criteria for interorganizational workflow processes. The method is based on the construction and analysis of Linear Logic proof trees, which represent the local processes as much as they do the global processes. The second and third methods are related, respectively to Soundness criteria verification, Relaxed Soundness and Weak Soundness for the interorganizational workflow processes. These are obtained through the analysis of reutilized Linear Logic proof trees that have been constructed for the verification of the Soundness criteria. However, the fourth method has the objective of detecting the deadlock free scenarios in interorganizational workflow and is based on the construction and analysis of Linear Logic proof trees, which initially takes into consideration the local processes and communication between such, and thereafter the candidate scenarios. A case study is carried out in the context of a Web services composition check, since there is a close correlation between the modelling of the interorganizational workflow process and a Web services composition. Therefore, the four methods proposed in the interorganizational workflow process context, are applied to a Web services composition. The evaluation of the obtained results shows that the reutilization of Linear Logic proof trees initially constructed for verifying the Soundness criteria, in fact occurs in the context of verifying the Relaxed Soundness andWeak Soundness criteria. In addition, the evaluation shows how the Linear Logic sequents and their proof trees explicitly show the possibilities for existing collaborations in a Web service composition. An evaluation that takes into account the number of constructed linear logic proof trees shows that this number can be significantly reduced in the deadlock-freeness scenarios detection method. An approach for resource planning based on the symbolic date calculation, which considers data extracted from Linear Logic proof trees is presented and validated through simulations performed on the CPN tools simulator. Two approaches for the monitoring of deadlockfreeness scenarios are introduced and show how data obtained from the Linear Logic proof trees can be used to guide the execution of such scenarios. / Este trabalho formaliza quatro métodos baseados na Lógica Linear para verificação de processos de workflow interorganizacionais modelados por WorkFlow nets interorganizacionais, que são redes de Petri que modelam tais processos. O primeiro método está relacionado com a verificação do critério de correção Soundness para processos de workflow interorganizacionais. O método é baseado na construção e análise de árvores de prova da Lógica Linear que representam tanto os processos locais quanto o processo global. O segundo e terceiro métodos estão relacionados, respectivamente, com a verificação dos critérios de correção Relaxed Soundness e Weak Soundness para processos de workflow interorganizacionais, e são obtidos através da análise de árvores de prova da Lógica Linear reutilizadas, construídas para a prova do critério de correção Soundness. Já o quarto método tem por objetivo a detecção dos cenários livres de deadlock em processos de workflow interorganizacionais e é baseado na construção e análise de árvores de prova da Lógica Linear que consideram, inicialmente, os processos locais e as comunicações entre estes e, posteriormente, os cenários candidatos. Um estudo de caso é realizado no contexto da verificação de composições de serviços Web, uma vez que há uma relação estreita entre a modelagem de um processo de workflow interorganizacional e uma composição de serviços Web. Assim, os quatro métodos propostos no contexto dos processos de workflow interorganizacionais são aplicados a uma composição de serviços Web. A avaliação dos resultados mostra que o reuso de árvores de prova da Lógica Linear construídas inicialmente para a prova do critério de correção Soundness de fato ocorre no contexto da verificação dos critérios de correção Relaxed Soundness e Weak Soundness. Além disso, a avaliação mostra como os sequentes da Lógica Linear e suas árvores de prova explicitam as possibilidades de colaboração existentes em uma composição de serviços Web. Uma avaliação que leva em conta o número de árvores de prova da Lógica Linear construídas mostra que este número pode ser significativamente reduzido no método para detecção de cenários livres de deadlock. Uma abordagem para planejamento de recursos, baseada no cálculo de datas simbólicas, que considera dados extraídos de árvores de prova da Lógica Linear, é apresentada e validada através de simulações realizadas no simulador CPN Tools. Duas abordagens para a monitoração dos cenários livres de deadlock são introduzidas e mostram como dados obtidos nas árvores de prova da Lógica Linear podem ser utilizados para guiar a execução de tais cenários. / Doutor em Ciência da Computação

Orientador: Mauricio Ferreira Magalhães / Dissertação (mestrado) - Universidade Estadual de Campinas, Faculdade de Engenharia Eletrica e de Computação / Made available in DSpace on 2018-08-08T01:16:08Z (GMT). No. of bitstreams: 1 Nader_MarcosVaninePortilhode_M.pdf: 1214383 bytes, checksum: 40e83a8be1c7e86e788d810a8799f6b8 (MD5) Previous issue date: 2006 / Resumo: Duas áreas importantes estão em desenvolvimento: Gerência de Processos de Negócios (Business Process Management) e Orquestração de Web Services (Web Services Orchestration). Ambas têm um objetivo que é integrar aplicações ou outros processos que tenham interfaces web services, usando o paradigma de processos de negócios. Uma linguagem que vem sendo difundida para essas aplicações é a BPEL (Business Process Execution Language). Este trabalho apresenta um framework aplicável à análise e verificação de processos de negócios escritos em BPEL através do uso de Pi-Calculus. Pi-Calculus é uma álgebra de processos que possui mecanismos formais para criação e ativação de processos que se comunicam através da troca de mensagens em canais, usando o modelo de rendezvous síncrono. Nesse framework, o processo BPEL é traduzido para um programa Pi-Calculus. Uma Máquina Virtual Pi-Calculus (MVP) recebe o programa Pi-Calculus e produz todas as reações possíveis, ou seja, gera todos os caminhos de execução que o programa pode seguir. A partir desse resultado, efetua-se a verificação de propriedades como: atendimento às especificações de mais alto nível, ordenação de eventos e ocorrência ou não de deadlocks. Em termos práticos, uma ferramenta desse tipo pode ser incorporada aos Sistemas de Gerência de Processos de Negócios (Business Process Management Systems - BPMS) para ampliar a cobertura de testes durante as fases de análise e implementação de um processo dentro do seu ciclo de vida. Nesses tipos de sistemas, a reparação de um erro durante a fase de execução é muito mais custosa que nos sistemas tradicionais / Abstract: Two important areas have been in development lately: Business Process Management and Web Service Orchestration. In both of them, the objective is to integrate applications with web services interface through business process paradigm. A number of languages have been proposed with consensus being formed around BPEL (Business Process Execution Language). This dissertation presents a framework for BPEL processes analysis and verification through Pi-Calculus. Pi-Calculus is a process algebra with formal mechanisms for processes creation and activation; these processes communicate sending and receiving messages through channels using the synchronous rendezvous model. In this framework, the BPEL process is translated to a Pi-Calculus program, A Pi-Calculus Virtual Machine (MVP) receives a Pi-calculus program and executes all possible reactions, that is, it generates all execution paths possible to be taken. With this result, the properties such as high-level specification accomplishment, events ordering and deadlock freedom are verified. In practical terms, a tool of this sort can be part of a Business Process Management System (BPMS) to broaden test coverage during the analysis and implementation phases within a process life cycle. In these kinds of systems, a repairing mistake during the execution phase is more complex than in traditional systems / Mestrado / Engenharia de Computação / Mestre em Engenharia Elétrica