Pantheon Repositorio Institucional
Recopila, preserva y difundi la producción académica digital en todas las áreas del conocimiento.
Comprende los activos del repositorio, además de tesis y disertaciones en la UFRJ, artículos científicos, libros electrónicos, capítulos de libros y trabajos presentados en eventos para los profesores, investigadores, personal administrativo y estudiantes de maestría y doctorado.
Por favor, use este identificador para citar o enlazar este ítem:
http://hdl.handle.net/11422/23625| Especie: | Trabalho de conclusão de graduação |
| Título : | Relato de experiência em modelagem e verificação de algoritmos concorrentes com TLA+ |
| Autor(es)/Inventor(es): | Cruz, Jones Martins Vieira da |
| Tutor: | Moreira, Anamaria Martins |
| Tutor : | Rossetto, Silvana |
| Resumen: | Sistemas concorrentes corretos são difíceis de se implementar. Abordagens em nível de programação, desde linguagens de programação modernas a ferramentas sofisticadas de testes, são incapazes de verificar propriedades importantes de sistemas concorrentes. Analisamos métodos formais como abordagem complementar para verificar tais propriedades, e, principalmente, para projetar sistemas concorrentes corretos. Métodos formais aqui são representados pela linguagem de especificação TLA+ e o verificador de modelos TLC. Estudamos TLA+ e sua lógica subjacente (TLA), desenvolvemos dois exemplos de modelagem e especificação em TLA+ – uma lock e um contador compartilhado– e, finalmente, discutimos os aprendizados e dificuldades dessa experiência. Concluímos que TLA+ nos dá uma base sólida sobre a qual futuras implementações de sistemas concorrentes podem ser construídas, principalmente porque a linguagem e seu ecossistema nos permitem definir e verificar propriedades relevantes impossíveis de se verificar com testes e simulações de programas. |
| Materia: | Computação concorrente Métodos formais Verificação de modelos TLA+ Concurrent systems Formal methods Formal methods |
| Materia CNPq: | CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO |
| Unidade de producción: | Instituto de Computação |
| Editor: | Universidade Federal do Rio de Janeiro |
| Fecha de publicación: | 26-jun-2024 |
| País de edición : | Brasil |
| Idioma de publicación: | por |
| Tipo de acceso : | Acesso Aberto |
| Aparece en las colecciones: | Ciência da Computação |
Ficheros en este ítem:
| Fichero | Descripción | Tamaño | Formato | |
|---|---|---|---|---|
| JMVCruz.pdf | 565.18 kB | Adobe PDF | Visualizar/Abrir |
Los ítems de DSpace están protegidos por copyright, con todos los derechos reservados, a menos que se indique lo contrario.