A representação e execução de processos de negócio têm gerado importantes desafios na área de Ciência da Computação. Um desses desafios é a escolha do melhor arcabouço formal para a especificação dos controles de fluxo padrões. Algumas linguagens defendem o uso de redes de Petri ou álgebras de processos como base formal. O uso de redes de Petri para especificar workflows clássicos é uma abordagem bastante conhecida. Entretanto, pesquisas recentes vêm difundindo o uso de novas extensões da álgebra de processos como uma alternativa para a especificação formal de workflows. A principal contribuição deste trabalho é a definição da Navigation Plan Definition Language (NPDL). A NPDL foi implementada como uma extensão da linguagem SQL. Ela é uma alternativa para a representação de workflows que utiliza a álgebra de processos como arcabouço formal. A NPDL promove uma separação explícita entre o ambiente de especificação e o ambiente de execução de um workflow. Esta separação propicia o reaproveitamento de passos de negócio e o uso das propriedades da álgebra de processos não só na modelagem, mas também no controle da execução dos processos. Após a especificação de um workflow por meio da NPDL, a execução dos passos que o definem é controlada pela ferramenta NavigationPlanTool. Essa ferramenta é a segunda contribuição deste trabalho de pesquisa. / The representation and execution of business processes have generated some important challenges in Computer Science. An important related concern is the choosing of the best formal foundation to represent control-flow patterns. Some of the workflow languages advocate the Petri nets or process algebra as formal foundation. The use of Petri nets is a famous approach to support classic workflows. On the other hand some researches are introducing modern process algebra extensions as an alternative formal foundation for representing workflows. The first contribution of this research is the definition of the Navigation Plan Definition Language (NPDL). NPDL was implemented as an extension of SQL language. It is an alternative to represent business processes using process algebra as formal foundation. NPDL provides the explicit separation between specification and execution workflow environment. This separation allows reusing of business steps and usage of process algebra properties in the process modeling and execution controlling tasks. After the definition of a workflow using NPDL, the business steps execution is carried out and controlled by a tool called NavigationPlanTool. This tool is the second contribution of this research.

Recentemente, várias abordagens estão sendo propostas na área de modelagem de processos de negócio. Dentre elas estão as linguagens BPEL e NPDL. BPEL é uma linguagem de representação e execução de processos de negócio que se mostrou bastante expressiva e uma forte candidata a padrão de mercado. NPDL é uma linguagem de definição de processos de negócio baseada em uma extensão de álgebra de processos chamada ACP. NPDL possui uma ferramenta capaz de interpretar e controlar a execução de processos de negócio chamada de NavigationPlanTool. A tradução de processos BPEL para expressões NPDL tem como objetivo fornecer aos processos descritos em BPEL um ambiente de controle e execução baseado em um formalismo algébrico. Entretanto, isso não é uma tarefa fácil. A presença de conceitos em BPEL que não são mapeáveis para NPDL faz com que grande parte da expressividade de BPEL se perca na tradução. Essa perda se dá pela limitação da própria ACP, na qual NPDL se baseia. Para sanar essa dificuldade, surgiu a idéia de estender ou trocar a base algébrica da NPDL. Substituindo a ACP por outro arcabouço algébrico ou incorporando idéias de outras álgebras, seria possível tornar a NPDL mais próxima de BPEL, facilitando, assim, o trabalho de mapeamento. Dentre os arcabouços formais disponíveis, LOTOS tem se mostrado uma interessante alternativa à ACP como base para a NPDL. Para comprovar os benefícios da utilização de conceitos de LOTOS na NPDL ou, até mesmo, de uma troca da base algébrica da NPDL de ACP para LOTOS, este trabalho faz um estudo comparativo entre esses dois formalismos algébricos, buscando encontrar a álgebra com maior expressividade e que represente melhor os conceitos presentes em BPEL. Para essa comparação, serão utilizados os principais conceitos existentes na linguagem BPEL, bem como os Padrões de Controle de Fluxo de Workflow. Não pertence ao escopo deste trabalho a implementação da NPDL usando LOTOS como base formal. / Recently, several approaches are being proposed in the business process modeling area. Among them are BPEL and NPDL languages. BPEL is a business process representation and execution language that has showed itself to be very expressive and a strong candidate to market reference. NPDL is a business process definition language based on a process algebra extension called ACP. NPDL has a tool called NavigationPlanTool that is able to interpret and control the business processes execution. The translation from BPEL processes to NPDL expressions aims to provide to BPEL processes a control and execution environment based on an algebraic foundation. However, this is not an easy task. Due to the translation, the presence of BPEL concepts that can´t be mapped to NPDL results in a heavy BPEL expressiveness loss. This loss occurs by the limitation of ACP, in which NPDL is based on. To solve this problem, the idea of extending or replacing the NPDL algebraic base has appeared. Replacing ACP with other algebraic framework or incorporating ideas from other algebras, could make NPDL closer to BPEL, turning the mapping work easier. Among the formal frameworks available, LOTOS has showed itself an interesting alternative to ACP as an NPDL basis. To prove the benefits of using LOTOS concepts in NPDL, or even exchanging the NPDL algebraic base from ACP to LOTOS, this work presents a comparative study between these two algebraic foundations, trying to find the most expressive algebra and the one that best represents the BPEL concepts. For this comparison, the BPEL main concepts and the Workflow Control-Flow Patterns will be used. The NPDL implementation using LOTOS as formal foundation is out of the scope of this work.

PROCESS algebras are a family of techniques used in formal specification and analysis of computer systems, specially when independent processes that perform and synchronize in parallel are concerned. The so-called concurrent systems. Circus is a process algebra that aggregates the expressiveness power for concurrent behaviors from CSP, along with the predicative data modelling aspects of Z. Recent publications have established a formal exhaustive symbolic testing theory for specifications modelled in Circus. Aiming to improve the feasibility of applying such tests in practical scenarios, it is convenient to look for criteria that reduces the number of test cases which, by the exhaustive nature of the approach, is often infinite. In the light of this, the work we present proposes the application of mutation testing techniques in Circus specifications, targeting the coverage of faults seeded by well-known mutation operators, along with operators designed with the particularities of the language in mind. Some contributions were produced in the pursuit of these goals, such as establishing a formal theory for mutation testing in Circus specifications and the implementation of a symbolic traces generator for the language. / ÁLGEBRAS de processos são uma família de técnicas de especificação e análise formal utilizadas em sistemas computacionais, especialmente em contextos de processos independentes, que atuam paralelamente e efetuam comunicação entre si. São os chamados sistemas concorrentes. Circus é uma álgebra de processos que agrega a capacidade de expressão de comportamentos concorrentes do CSP com a modelagem predicativa de dados da notação Z. Trabalhos recentes vêm estabelecer uma teoria para o teste simbólico exaustivo baseado em especificações modeladas em Circus. Com o objetivo de viabilizar a aplicação prática desses testes, é conveniente estudar critérios que reduzam o conjunto de casos de teste que, pela sua natureza exaustiva, torna-se frequentemente infinito. Neste sentido, o presente trabalho propõe a aplicação de técnicas de teste de mutação à partir de especificações Circus, visando a cobertura de falhas inseridas por meio de operadores de mutação já conhecidos, juntamente com operadores propostos especificamente para a linguagem. Algumas contribuições foram produzidas na busca destes objetivos, como o estabelecimento de uma teoria formal para a aplicação de teste de mutação em especificações Circus e a implementação de um gerador de rastros simbólicos para a mesma linguagem.

A representação e execução de processos de negócio têm gerado importantes desafios na área de Ciência da Computação. Um desses desafios é a escolha do melhor arcabouço formal para a especificação dos controles de fluxo padrões. Algumas linguagens defendem o uso de redes de Petri ou álgebras de processos como base formal. O uso de redes de Petri para especificar workflows clássicos é uma abordagem bastante conhecida. Entretanto, pesquisas recentes vêm difundindo o uso de novas extensões da álgebra de processos como uma alternativa para a especificação formal de workflows. A principal contribuição deste trabalho é a definição da Navigation Plan Definition Language (NPDL). A NPDL foi implementada como uma extensão da linguagem SQL. Ela é uma alternativa para a representação de workflows que utiliza a álgebra de processos como arcabouço formal. A NPDL promove uma separação explícita entre o ambiente de especificação e o ambiente de execução de um workflow. Esta separação propicia o reaproveitamento de passos de negócio e o uso das propriedades da álgebra de processos não só na modelagem, mas também no controle da execução dos processos. Após a especificação de um workflow por meio da NPDL, a execução dos passos que o definem é controlada pela ferramenta NavigationPlanTool. Essa ferramenta é a segunda contribuição deste trabalho de pesquisa. / The representation and execution of business processes have generated some important challenges in Computer Science. An important related concern is the choosing of the best formal foundation to represent control-flow patterns. Some of the workflow languages advocate the Petri nets or process algebra as formal foundation. The use of Petri nets is a famous approach to support classic workflows. On the other hand some researches are introducing modern process algebra extensions as an alternative formal foundation for representing workflows. The first contribution of this research is the definition of the Navigation Plan Definition Language (NPDL). NPDL was implemented as an extension of SQL language. It is an alternative to represent business processes using process algebra as formal foundation. NPDL provides the explicit separation between specification and execution workflow environment. This separation allows reusing of business steps and usage of process algebra properties in the process modeling and execution controlling tasks. After the definition of a workflow using NPDL, the business steps execution is carried out and controlled by a tool called NavigationPlanTool. This tool is the second contribution of this research.

Recentemente, várias abordagens estão sendo propostas na área de modelagem de processos de negócio. Dentre elas estão as linguagens BPEL e NPDL. BPEL é uma linguagem de representação e execução de processos de negócio que se mostrou bastante expressiva e uma forte candidata a padrão de mercado. NPDL é uma linguagem de definição de processos de negócio baseada em uma extensão de álgebra de processos chamada ACP. NPDL possui uma ferramenta capaz de interpretar e controlar a execução de processos de negócio chamada de NavigationPlanTool. A tradução de processos BPEL para expressões NPDL tem como objetivo fornecer aos processos descritos em BPEL um ambiente de controle e execução baseado em um formalismo algébrico. Entretanto, isso não é uma tarefa fácil. A presença de conceitos em BPEL que não são mapeáveis para NPDL faz com que grande parte da expressividade de BPEL se perca na tradução. Essa perda se dá pela limitação da própria ACP, na qual NPDL se baseia. Para sanar essa dificuldade, surgiu a idéia de estender ou trocar a base algébrica da NPDL. Substituindo a ACP por outro arcabouço algébrico ou incorporando idéias de outras álgebras, seria possível tornar a NPDL mais próxima de BPEL, facilitando, assim, o trabalho de mapeamento. Dentre os arcabouços formais disponíveis, LOTOS tem se mostrado uma interessante alternativa à ACP como base para a NPDL. Para comprovar os benefícios da utilização de conceitos de LOTOS na NPDL ou, até mesmo, de uma troca da base algébrica da NPDL de ACP para LOTOS, este trabalho faz um estudo comparativo entre esses dois formalismos algébricos, buscando encontrar a álgebra com maior expressividade e que represente melhor os conceitos presentes em BPEL. Para essa comparação, serão utilizados os principais conceitos existentes na linguagem BPEL, bem como os Padrões de Controle de Fluxo de Workflow. Não pertence ao escopo deste trabalho a implementação da NPDL usando LOTOS como base formal. / Recently, several approaches are being proposed in the business process modeling area. Among them are BPEL and NPDL languages. BPEL is a business process representation and execution language that has showed itself to be very expressive and a strong candidate to market reference. NPDL is a business process definition language based on a process algebra extension called ACP. NPDL has a tool called NavigationPlanTool that is able to interpret and control the business processes execution. The translation from BPEL processes to NPDL expressions aims to provide to BPEL processes a control and execution environment based on an algebraic foundation. However, this is not an easy task. Due to the translation, the presence of BPEL concepts that can´t be mapped to NPDL results in a heavy BPEL expressiveness loss. This loss occurs by the limitation of ACP, in which NPDL is based on. To solve this problem, the idea of extending or replacing the NPDL algebraic base has appeared. Replacing ACP with other algebraic framework or incorporating ideas from other algebras, could make NPDL closer to BPEL, turning the mapping work easier. Among the formal frameworks available, LOTOS has showed itself an interesting alternative to ACP as an NPDL basis. To prove the benefits of using LOTOS concepts in NPDL, or even exchanging the NPDL algebraic base from ACP to LOTOS, this work presents a comparative study between these two algebraic foundations, trying to find the most expressive algebra and the one that best represents the BPEL concepts. For this comparison, the BPEL main concepts and the Workflow Control-Flow Patterns will be used. The NPDL implementation using LOTOS as formal foundation is out of the scope of this work.

Devido à grande diversidade de microrganismos desconhecidos no meio ambiente, 99% deles não podem ser cultivados nos meios de cultura tradicionais dos laboratórios. Para isso, projetos metagenômicos são propostos para estudar comunidades microbianas presentes no meio ambiente, a partir de técnicas moleculares, em especial o seqüenciamento. Dessa forma, para os próximos anos é esperado um acúmulo de seqüências produzidas por esses projetos. As seqüências produzidas pelos projetos genomas e metagenomas apresentam vários desafios para o tratamento, armazenamento e análise, como exemplo: a busca de clones contendo genes de interesse. Este trabalho apresenta uma abordagem algébrica que define e gerencia de forma dinâmica as regras para a seleção de clones em bibliotecas genômicas e metagenômicas, que se baseiam em álgebra de processos. Além disso, uma interface web foi desenvolvida para permitir que os pesquisadores criem e executem facilmente suas próprias regras de seleção de clones em bancos de dados de seqüências genômicas e metagenômicas. Este software foi testado em bibliotecas genômicas e metagenômicas e foi capaz de selecionar clones contendo genes de interesse. / Due to the wide diversity of unknown organisms in the environment, 99% of them cannot be grown in traditional culture medium in laboratories. Therefore, metagenomics projects are proposed to study microbial communities present in the environment, from molecular techniques, especially the sequencing. Thereby, for the coming years it is expected an accumulation of sequences produced by these projects. Thus, the sequences produced by genomics and metagenomics projects present several challenges for the treatment, storing and analysis such as: the search for clones containing genes of interest. This work presents an algebraic approach that defines it dynamically and manages the rules of the selection of clones in genomic and metagenomic libraries, which are based on process algebra. Furthermore, a web interface was developed to allow researchers to easily create and execute their own rules to select clones in genomic and metagenomic sequence database. This software was tested in genomics and metagenomics libraries and it was able to select clones containing genes of interest.

CCS (Communicating and Concurrent Systems) is the process algebra to specify and verify concurrent and communicating systems. This work proposes a transformation guide of the CCS equations into to the UML-RT (Unified Modeling Language for Real-Time) model and a transformation guide of the UML-RT model into a set of CCS equations. The UML-RT model is a software design language, which supports code generation and the construction of executable systems. The UML-RT is an UML extension, and it does not have a formal semantics; therefore it is not possible to verify UMLRT models. The transformation guide of UML-RT models into CCS equations allows verifying the models. We argue that the transformation of CCS models into UML-RT models allows an alternative way of correctly building systems. This work details the transformation guides from CCS equations to UML-RT models and from UML-RT models to CSS equations and it discusses the limitations and benefits.

Submitted by Fabio Sobreira Campos da Costa (fabio.sobreira@ufpe.br) on 2016-08-08T12:10:14Z No. of bitstreams: 2 license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) v_final_assinaturas_branco.pdf: 10378086 bytes, checksum: 35e52eff52531ee36b6a5af5b2a20645 (MD5) / Made available in DSpace on 2016-08-08T12:10:14Z (GMT). No. of bitstreams: 2 license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) v_final_assinaturas_branco.pdf: 10378086 bytes, checksum: 35e52eff52531ee36b6a5af5b2a20645 (MD5) Previous issue date: 2016-03-03 / The increasing complexity of systems has led to increasing difficulty in design. Thestandard approach to development, based on trial and error, with testing used at later stages toidentify errors, is costly and leads to unpredictable delivery times. In addition, for critical systems,for which safety is a major concern, early verification and validation (V&V) is recognised asa valuable approach to promote dependability. In this context, we identify three important anddesirable features of a V&V technique: (i) a graphical modelling language; (ii) formal andrigorous reasoning, and (iii) automated support for modelling and reasoning. We address these points with a refinement technique for SysML supported by tools. SysML is a UML-based language for systems design; it has itself become a de facto standard in the area. There is wide availability of tool support from vendors like IBM, Atego, and Sparx Systems. Our work is distinctive in two ways: a semantics for refinement and for a representative collection of elements from the UML4SysML profile (blocks, state machines, activities, and interactions) used in combination. We provide a means to analyse design models specified using SysML. This facilitates the discovery of problems earlier in the system development lifecycle, reducing time and costs of production. In this work we describe our semantics, which is defined using a state-rich process algebra called CML and implemented in a tool for automatic generation of formal models. We also show how the semantics can be used for refinement-based analysis and development. Our case studies are a leadership-election protocol, a critical component of an industrial application, and a dwarf signal, a device used to control rail traffic. Our contributions are: a set of guidelines that provide meaning to the different modelling elements of SysML used during the design of systems; the individual formal semantics for SysML activities, blocks and interactions; an integrated semantics that combines these semantics with another defined for state machines; and a framework for reasoning using refinement about systems specified by collections of SysML diagrams. / O aumento da complexidade dos sistemas tem levado a um aumento na dificuldade da atividade de projeto. A abordagem padrão para desenvolvimento, baseada em tentativa e erro, com testes usados em estágios avançados para identificar erros, é custosa e leva a prazos de entrega imprevisíveis. Além disto, para sistemas críticos, para os quais segurança é um conceito chave, Verificação e Validação (V&V) com antecedência é reconhecida como uma abordagem valiosa para promover confiança. Neste contexto, nós identificamos três características importantes e desejáveis de uma técnica de V&V: (i) uma linguagem de modelagem gráfica; (ii) raciocínio formal e rigoroso, e (iii) suporte automático para modelagem e raciocínio. Nós tratamos estes pontos com uma técnica de refinamento para SysML apoiada por ferramentas. SysML é uma linguagem baseada na UML para o projeto de sistemas. Ela tem se tornado um padrão de facto na área. Há uma grande disponibilidade de ferramentas de fornecedores como IBM, Atego, e Sparx Systems. Nosso trabalho se destaca de duas maneiras: ao fornecer uma semântica para refinamento e considerar uma coleção representativa de elementos do perfil UML4SysML (blocos, máquina de estados, atividades, e interações) usados de forma combinada. Nós fornecemos uma estratégia para analisar modelos de projeto especificados em SysML. Isto facilita a descoberta de problemas mais cedo durante o ciclo de vida de desenvolvimento de sistemas, reduzindo tempo e custos de produção. Neste trabalho nós descrevemos nossa semântica a qual é definida usando uma álgebra de processo rica em estado chamada CML e implementada em uma ferramenta para geração automática de modelos formais. Nós também mostramos como esta semântica pode ser usada para análise baseada em refinamento. Nossos estudos de caso são um protocolo de eleição de líder, o qual é um componente crítico de uma aplicação industrial, e um sinal anão, o qual é um dispositivo para controlar tráfego em linhas férreas. Nossas contribuições são: um conjunto de orientações que fornecem significado para os diferentes elementos de modelagem de SysML usados durante o projeto de sistemas; as semânticas formais individuais para atividades, blocos e interações de SysML; uma semântica integrada que combina estas semânticas com outra definida para máquina de estados; e um arcabouço que usa refinamento para raciocínio de sistemas especificados por coleções de diagramas SysML.

Devido à grande diversidade de microrganismos desconhecidos no meio ambiente, 99% deles não podem ser cultivados nos meios de cultura tradicionais dos laboratórios. Para isso, projetos metagenômicos são propostos para estudar comunidades microbianas presentes no meio ambiente, a partir de técnicas moleculares, em especial o seqüenciamento. Dessa forma, para os próximos anos é esperado um acúmulo de seqüências produzidas por esses projetos. As seqüências produzidas pelos projetos genomas e metagenomas apresentam vários desafios para o tratamento, armazenamento e análise, como exemplo: a busca de clones contendo genes de interesse. Este trabalho apresenta uma abordagem algébrica que define e gerencia de forma dinâmica as regras para a seleção de clones em bibliotecas genômicas e metagenômicas, que se baseiam em álgebra de processos. Além disso, uma interface web foi desenvolvida para permitir que os pesquisadores criem e executem facilmente suas próprias regras de seleção de clones em bancos de dados de seqüências genômicas e metagenômicas. Este software foi testado em bibliotecas genômicas e metagenômicas e foi capaz de selecionar clones contendo genes de interesse. / Due to the wide diversity of unknown organisms in the environment, 99% of them cannot be grown in traditional culture medium in laboratories. Therefore, metagenomics projects are proposed to study microbial communities present in the environment, from molecular techniques, especially the sequencing. Thereby, for the coming years it is expected an accumulation of sequences produced by these projects. Thus, the sequences produced by genomics and metagenomics projects present several challenges for the treatment, storing and analysis such as: the search for clones containing genes of interest. This work presents an algebraic approach that defines it dynamically and manages the rules of the selection of clones in genomic and metagenomic libraries, which are based on process algebra. Furthermore, a web interface was developed to allow researchers to easily create and execute their own rules to select clones in genomic and metagenomic sequence database. This software was tested in genomics and metagenomics libraries and it was able to select clones containing genes of interest.

Modelagem e controle de execução são duas abordagens do gerenciamento de processos de negócio que, embora complementares, têm se desenvolvido independentemente. Por um lado, a modelagem é normalmente conduzida por especialistas de negócio e explora aspectos semânticos do processo. Por outro lado, o controle de execução estuda mecanismos consistentes e eficientes de implementação. Este trabalho apresenta um método algorítmico que relaciona modelagem e controle de execução, por meio da geração de expressões algébricas a partir de digrafos acíclicos. Por hipótese, assumimos que modelos de processos de negócio são formados por estruturas baseadas em grafos, e mecanismos de controle de execução são baseados na interpretação de expressões de álgebra de processos. Para a geração de expressões algébricas, esta tese apresenta as propriedades topológicas de digrafos série-paralelo e define um sistema de transformação baseado em redução de digrafos. Além disso, um algoritmo de identificação de digrafos série-paralelo e geração de expressões algébricas é apresentado. O texto também discute o tratamento de digrafos que não são série-paralelo e apresenta, para alguns desses casos, soluções baseadas em mudanças topológicas. Finalmente, o algoritmo é ilustrado com o estudo de caso de uma aplicação real. / Modeling and execution control are complementary approaches of business process management that have been developed independently. On one hand, modeling is usually performed by business specialists and explores semantical aspects of the business process. On other hand, execution control studies consistent and efficient mechanisms for implementation. This work presents an algorithmic method which joins modeling and execution control through algebraic expression generation from acyclic digraphs. By hypothesis, we assume that business process models are defined by graph structures, and execution control mechanisms are based on interpretation of process algebra expressions. For algebraic expression generation, this thesis presents the topological properties of series-parallel digraphs and defines a transformation system based on digraph reduction. Therefore, we present an algorithm for identification of series-parallel digraphs and generation of algebraic expressions. This work also discusses the treatment of non-series-parallel digraphs and presents solutions based on topological changing for some cases. Finally, the algorithm is illustrated with a case study based on a real system.