Verificação de refinamento em diagramas de sequência com estruturas de controle
| dc.contributor.advisor | Lima, Lucas Albertins de | |
| dc.contributor.advisorLattes | http://lattes.cnpq.br/0465071050875729 | |
| dc.contributor.author | Araújo, Daniel José Freire de | |
| dc.contributor.authorLattes | http://lattes.cnpq.br/5219541109924367 | |
| dc.date.accessioned | 2020-01-29T13:26:23Z | |
| dc.date.available | 2020-01-29T13:26:23Z | |
| dc.date.issued | 2019 | |
| dc.degree.departament | Computação | |
| dc.degree.graduation | Bacharelado em Ciência da Computação | |
| dc.degree.grantor | Universidade Federal Rural de Pernambuco | |
| dc.degree.level | Graduacao | |
| dc.degree.local | Recife | |
| dc.description.abstract | 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. | |
| dc.description.abstractx | The UML language offers several types of diagrams for system modeling, among themain behavioral diagrams is the sequence diagram. The sequence diagram can beused to model system use cases simply and visually. However, the UML language asa whole presents informal models that can only be verified by human experience. Thispaper refers to the continuation of a research line that aims to formalize UML sequence diagrams and perform refinement checks between diagrams.Here we propose aninitial version of a tool capable of translating UML sequence diagrams into CSP and perform-ing a refinement check using the FDR4 verifier. The differential point of this work isthe process of formalization of combined fragments that represent control structures insequence diagrams, here we will cover fragments such asoption,alternative, paralleland loop. | |
| dc.format.extent | 69 f. | |
| dc.identifier.citation | ARAÚ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. | |
| dc.identifier.darkflstrmv | https://n2t.net/ark:/57462/001300000ff4v | |
| dc.identifier.uri | https://repository.ufrpe.br/handle/123456789/1858 | |
| dc.language.iso | por | |
| dc.publisher.country | Brasil | |
| dc.relation.uri | openAccess | pt_BR |
| dc.rights.license | Atribuição-NãoComercial-CompartilhaIgual 4.0 Internacional (CC BY-NC-SA 4.0) | |
| dc.rights.uri | https://creativecommons.org/licenses/by-nc-sa/4.0/deed.pt_BR | |
| dc.subject | Linguagem de programação (Computadores) | |
| dc.subject | Software - Desenvolvimento | |
| dc.title | Verificação de refinamento em diagramas de sequência com estruturas de controle | |
| dc.type | bachelorThesis |