Please use this identifier to cite or link to this item: https://repository.ufrpe.br/handle/123456789/4508
Title: Verificação de modelos comportamentais UML como um serviço habilitando a aplicação de métodos formais ocultos
Authors: Cavalcanti, Paulo Henrique Nascimento
metadata.dc.contributor.authorLattes: http://lattes.cnpq.br/7089611179473920
metadata.dc.contributor.advisor: Lima, Lucas Albertins de
metadata.dc.contributor.advisorLattes: http://lattes.cnpq.br/0465071050875729
Keywords: UML (Computação);Diagrama de atividade
Issue Date: 4-Oct-2022
Citation: CAVALCANTI, Paulo Henrique Nascimento. Verificação de modelos comportamentais UML como um serviço habilitando a aplicação de métodos formais ocultos. 2022. 50 f. Trabalho de Conclusão de Curso (Bacharelado em Ciência da Computação) – Departamento de Computação, Universidade Federal Rural de Pernambuco, Recife, 2022.
Abstract: As systems become more complex, more effort is required to perform validations on them. In addition to complexity, the cost of corrections also increases as projects progress, making error detection at the earliest stages essential. Within Model-Based Systems Engineering, model verification is one of the possible approaches to solving the problem. However, performing such verification often involves the use of formal methods. These methods are complex and not all system designers are knowledgeable in them. Another important point is that, given the increasing need to support large loads, it is common to use concurrency in systems. This concurrent nature of systems brings with it the possibility of including problems such as deadlock and non-determinism, usually not verified by current tools, which often also require licenses for their use and offer little possibilities of integration with other tools and environments. In this sense, our work uses the framework built in previous initiatives to expand the possibility of checking models through free and open source microservices. Although other works have already performed the verification of properties in UML models, most of them depend on the installation of tools and allow little or no integration with other systems. Therefore, our main contribution is the construction of a microservices-based architecture to provide services for checking classic properties (deadlock and non-determinism) for a subset of behavioral UML models, more precisely activity diagrams and state machines.
Description: Conforme os sistemas vão ficando mais complexos, mais esforço tem sido necessário para realizar validações sobre eles. Além da complexidade, o custo de correções também aumenta conforme os projetos avançam de fase, tornando essencial a detecção de erros nos estágios mais iniciais. Dentro da Model-Based Systems Engineering, a verificação de modelos é uma das possíveis abordagens para a solução do problema. Contudo, realizar tal verificação envolve muitas vezes a utilização de métodos formais. Estes métodos são complexos e nem todos os projetistas de sistemas têm conhecimento deles. Um outro ponto importante é que, dada a necessidade cada vez maior de suportar grandes cargas, é comum a utilização de concorrência nos sistemas. Essa natureza concorrente dos sistemas atuais traz consigo a possibilidade da inclusão de problemas como deadlock e não-determinismo, normalmente não verificados pelas ferramentas atuais, que muitas vezes também exigem licenças para sua utilização e oferecem poucas possibilidades de integração com outras ferramentas ou ambientes. Neste sentido, nosso trabalho utiliza-se do arcabouço construído em trabalhos anteriores parwa expandir a possibilidade da checagem de modelos através de microsserviços, gratuitos e de código aberto. Apesar de outros trabalhos já realizarem a verificação de propriedades em modelos UML, em sua maioria, eles dependem da instalação de ferramentas e permitem pouca ou nenhuma integração com outros sistemas. Sendo assim, nossa principal contribuição é a construção de uma arquitetura baseada em microsserviços para disponibilizar serviços de verificação de propriedades clássicas (deadlock e não-determinismo) para um subconjunto de modelos UML comportamentais, mais precisamente diagramas de atividade e de máquinas de estado.
URI: https://repository.ufrpe.br/handle/123456789/4508
Appears in Collections:TCC - Bacharelado em Ciência da Computação (Sede)

Files in This Item:
File Description SizeFormat 
tcc_paulohenriquenascimentocavalcanti.pdf1,05 MBAdobe PDFView/Open


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.