Lima, Lucas Albertins deAraújo, Daniel José Freire de2020-01-292020-01-292019ARAÚJO, Daniel José Freire de. Verificação de refinamento em diagramas de sequência com estruturas de controle. 2019. 69 f. Trabalho de Conclusão de Curso (Bacharelado em Ciência da Computação) - Departamento de Computação, Universidade Federal Rural de Pernambuco, Recife, 2019.https://repository.ufrpe.br/handle/123456789/1858A linguagem UML oferece diversos tipos de diagramas para modelagem de sistemas,entre os principais diagramas comportamentais está o diagrama de sequência. O diagrama de sequência pode ser utilizado para modelar casos de uso de sistemas deforma simples e visual. Contudo, a linguagem UML como um todo apresenta modelos informais que possuem verificações baseadas em experiência humana. Este trabalho é a continuação de um linha de pesquisa que tem o objetivo de formalizar diagramas de sequência UML e realizar verificações de refinamento entre diagramas. Aqui é proposta a versão inicial de uma ferramenta capaz de traduzir diagramas de sequência UML para uma especificação formal CSP e realizar a verificação de refinamentos através do verificador FDR4. O ponto diferencial deste trabalho é o processo de formalização de fragmentos combinados que representam estruturas de controle no contexto de diagramas de sequência, aqui serão abordados os fragmentos option, alternative, parallel e loop.69 f.porhttps://creativecommons.org/licenses/by-nc-sa/4.0/deed.pt_BRLinguagem de programação (Computadores)Software - DesenvolvimentobachelorThesisAtribuição-NãoComercial-CompartilhaIgual 4.0 Internacional (CC BY-NC-SA 4.0)https://n2t.net/ark:/57462/001300000ff4v