Use este identificador para citar ou linkar para este item: https://repositorio.ufu.br/handle/123456789/30801
ORCID:  http://orcid.org/0000-0002-4011-9247
Tipo do documento: Tese
Tipo de acesso: Acesso Aberto
Título: Verificação de requisitos funcionais e não funcionais em Arquiteturas Orientadas a Serviços
Título(s) alternativo(s): Verification of functional and non-functional requirements in Service Oriented Architectures
Autor(es): Oliveira, Kênia Santos de
Primeiro orientador: Julia, Stéphane
Primeiro membro da banca: Rosa, Pedro Frosi
Segundo membro da banca: Lopes, Carlos Roberto
Terceiro membro da banca: Silva, José Reinaldo
Quarto membro da banca: Lüders, Ricardo
Resumo: Este trabalho de pesquisa apresenta formalmente dois métodos para a verificação de cenários de requisitos funcionais e não funcionais em Arquiteturas Orientadas a Serviços (SOA) e também dois métodos para a detecção e remoção de requisitos negativos do tipo deadlock em SOA. A SOA representa processos de negócio e é modelada por uma WorkFlow net interorganizacional que não é necessariamente livre de deadlock (bloqueios). 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 na arquitetura correspondente. 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. A partir de uma marcação indesejada, que representa um estado parcial do modelo, sã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, é utilizado um raciocínio inverso na 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. Para prevenir as situações de deadlock, que são causadas pela troca de mensagens em um workflow interorganizacional, é 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.
Abstract: This research work formally presents two methods for scenarios verification of functional and non-functional requirements in Service-Oriented Architecture (SOA) models and also two methods for detecting and removing negative requirements of deadlock type in SOA. SOA represents business processes and it is modeled by a Interorganizational WorkFlow net that is not necessarily deadlock-free. The first method is related to the verification of scenarios of service requirements (behavior) in SOA. The verification is based on the construction of Linear Logic proof trees and precedence graphs derived from proof trees correctly finalized. The precedence graphs of the requirement and architectural models are compared using a type of bisimulation defined in this work in order to verify if all existing scenarios of the requirement model also exist in the corresponding architecture. The second method is related to the verification of performance of service requirements in SOA. The Linear Logic proof trees constructed for the first method are reused with the addition of symbolic dates associated with each atom of the produced trees. At the end of the execution of each scenario, symbolic date intervals are generated to compare if the scenarios that are equivalents in terms of behavior are also equivalents in terms of performance. The third method is related to the detection of negative requirements of deadlock type in SOA. Starting from a feared marking, which represents a partial state of the model, all sequences of actions will be identified, that is, all scenarios that can turn a service requirement into a negative requirement of deadlock type. To identify these sequences of actions, an inverse reasoning will be used in the architecture model, applying the same idea used in the method to verify functional requirements. The fourth method is related to deadlock control. To prevent deadlock situations that are caused by the exchange of messages in an interorganizational workflow, the synchronization of local processes will be used. Synchronization forces local workflow processes to perform certain activities simultaneously; thereby, removing the deadlock situation from the model. The methods are validated through a case study that is also simulated in the CPN Tools simulator. The validation and the complexity analysis performed, show that the methods can be effective to identify whether an SOA-based system satisfies the behavior and performance of the business needs specified by a public requirements model and also to identify and correct negative requirements of deadlock type.
Palavras-chave: WorkFlow net Interorganizacional
t-Time WorkFlow net
Redes de Petri
Lógica Linear
Arquitetura Orientada a Serviços
Verificação de Requisitos
Bissimulação
Interorganizational WorkFlow net
t-Time WorkFlow net
Petri net
Linear Logic
Service Oriented Architecture
Requirements Verification
Bisimulation
Área(s) do CNPq: CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO
Assunto: Arquitetura orientada a serviços (Computador)
Fluxo de trabalho
Petri, Redes de
Idioma: por
País: Brasil
Editora: Universidade Federal de Uberlândia
Programa: Programa de Pós-graduação em Ciência da Computação
Referência: OLIVEIRA, Kênia Santos de. Verificação de requisitos funcionais e não funcionais em Arquiteturas Orientadas a Serviços. 2020. 204 f. Tese (Doutorado em Ciência da Computação) - Universidade Federal de Uberlândia, Uberlândia, 2020. DOI http://doi.org/10.14393/ufu.te.2020.786.
Identificador do documento: http://doi.org/10.14393/ufu.te.2020.786
URI: https://repositorio.ufu.br/handle/123456789/30801
Data de defesa: 3-Dez-2020
Aparece nas coleções:TESE - Ciência da Computação

Arquivos associados a este item:
Arquivo Descrição TamanhoFormato 
VerificacaoRequisitosFuncionais.pdfTese21.28 MBAdobe PDFThumbnail
Visualizar/Abrir


Este item está licenciada sob uma Licença Creative Commons Creative Commons