[TESE DE DOUTORADO] Verificação de Requisitos Funcionais e não Funcionais em Arquiteturas Orientadas a Serviços

Local: 
Por videoconferência
Data de Defesa: 
03/12/2020 - 14:00
Banca examinadora: 
Prof. Dr. Stéphane Julia - FACOM/UFU (Orientador)
Prof. Dr. Pedro Frosi Rosa - FACOM/UFU
Prof. Dr. Carlos Roberto Lopes - FACOM/UFU
Prof. Dr. José Reinaldo Silva - USP
Prof. Dr. Ricardo Luders - UTFPR

Este trabalho de pesquisa apresenta formalmente dois métodos para a verificação de cenários de requisitos funcionais e não funcionais em modelos de Arquiteturas Orientadas a Serviços (SOA), os quais representam processos de negócio e são representados por WorkFlow nets interorganizacionais que não são necessariamente livres de deadlock (bloqueios mortais). O propósito destes métodos é mostrar que, no contexto de SOA, todos os cenários presentes em um modelo de requisitos também estão presentes no modelo de arquitetura correspondente em termos de comportamento e desempenho. Este trabalho de pesquisa também apresenta métodos para a detecção e remoção de requisitos negativos do tipo deadlock em SOA. Na abordagem apresentada neste trabalho, um modelo de requisitos corresponde a um modelo público que somente especifica as ações que são de interesse de todas as partes envolvidas nos processos. Um modelo de arquitetura é considerado como um conjunto de processos privados que interagem através de mecanismos de comunicação assíncrona a fim de produzir os serviços especificados no modelo de requisitos correspondente. Os serviços podem ser vistos como cenários de uma WorkFlow net. O primeiro método proposto está relacionado com a verificação de cenários dos requisitos de serviços (comportamentais) em SOA. A verificação é baseada na construção das árvores de prova da Lógica Linear e dos grafos de precedência derivados a partir das árvores de prova corretamente finalizadas. Os grafos de precedência dos modelos de requisitos e de arquitetura são comparados por meio de um tipo de bissimulação definida neste trabalho a fim de verificar se todos os cenários que existem no modelo de requisitos também existem no modelo de arquitetura. O segundo método está relacionado com a verificação do desempenho dos requisitos de serviços em SOA. As árvores de prova da Lógica Linear construídas para o primeiro método são reutilizadas com o acréscimo de datas simbólicas associadas a cada átomo das árvores geradas. No final da execução de cada cenário, intervalos de datas simbólicas são gerados para comparar se os cenários que são equivalentes em termos de comportamento também são equivalentes em termos de desempenho. O terceiro método está relacionado com a detecção de requisitos negativos do tipo deadlock em SOA. Como uma exploração sistemática gera modelos muito grandes, neste trabalho, as situações de deadlock são consideradas somente quando, de fato, elas ocorrem. Portanto, a partir de uma marcação indesejada, que representa um estado parcial do modelo, serão identificadas todas as sequências de ações, ou seja, todos os cenários que podem tornar um requisito de serviço em um requisito negativo do tipo deadlock. Para a identificação destas sequências de ações, será utilizado um raciocínio inverso no modelo de arquitetura aplicando a mesma ideia utilizada no método para verificação de requisitos funcionais. O quarto método está relacionado com o controle do deadlock. Após o diagnóstico do deadlock, é importante fornecer meios de recuperação do requisito de serviço que levou a tal situação e também de correção do modelo de arquitetura para impedir ocorrências futuras de tal comportamento. Para prevenir as situações de deadlock que são causadas pela troca de mensagens em um workflow interorganizacional, será utilizada a sincronização dos processos locais. A sincronização força os processos de workflow locais executarem simultaneamente certas atividades, removendo, desse modo, a situação de deadlock do modelo. Os métodos são validados através de um estudo de caso que também é simulado no simulador CPN Tools. A validação e a análise de complexidade realizada, mostram que os métodos podem ser efetivos para identificar se um sistema baseado em SOA satisfaz o comportamento e o desempenho das necessidades de negócio especificadas por um modelo de requisitos público e também para identificar e corrigir requisitos negativos do tipo deadlock.