Please use this identifier to cite or link to this item:
https://repositorio.ufu.br/handle/123456789/30801
ORCID: | ![]() |
Document type: | Tese |
Access type: | Acesso Aberto |
Title: | Verificação de requisitos funcionais e não funcionais em Arquiteturas Orientadas a Serviços |
Alternate title (s): | Verification of functional and non-functional requirements in Service Oriented Architectures |
Author: | Oliveira, Kênia Santos de |
First Advisor: | Julia, Stéphane |
First member of the Committee: | Rosa, Pedro Frosi |
Second member of the Committee: | Lopes, Carlos Roberto |
Third member of the Committee: | Silva, José Reinaldo |
Fourth member of the Committee: | Lüders, Ricardo |
Summary: | 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. |
Keywords: | 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 |
Area (s) of CNPq: | CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO |
Subject: | Arquitetura orientada a serviços (Computador) Fluxo de trabalho Petri, Redes de |
Language: | por |
Country: | Brasil |
Publisher: | Universidade Federal de Uberlândia |
Program: | Programa de Pós-graduação em Ciência da Computação |
Quote: | 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. |
Document identifier: | http://doi.org/10.14393/ufu.te.2020.786 |
URI: | https://repositorio.ufu.br/handle/123456789/30801 |
Date of defense: | 3-Dec-2020 |
Appears in Collections: | TESE - Ciência da Computação |
Files in This Item:
File | Description | Size | Format | |
---|---|---|---|---|
VerificacaoRequisitosFuncionais.pdf | Tese | 21.28 MB | Adobe PDF | ![]() View/Open |
This item is licensed under a Creative Commons License