(2019) Araújo, Daniel José Freire de; Lima, Lucas Albertins de; http://lattes.cnpq.br/0465071050875729; http://lattes.cnpq.br/5219541109924367
A 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.
