Relato de experiência em modelagem e verificação de algoritmos concorrentes com TLA+
| dc.contributor.advisor | Moreira, Anamaria Martins | |
| dc.contributor.advisorCo1 | Rossetto, Silvana | |
| dc.contributor.referee1 | Menasché, Daniel Sadoc | |
| dc.contributor.referee2 | Paixão, João Antônio Récio da | |
| dc.creator | Cruz, Jones Martins Vieira da | |
| dc.date.accessioned | 2024-09-06T15:50:15Z | |
| dc.date.available | 2026-05-16T03:08:44Z | |
| dc.date.issued | 2024-06-26 | |
| dc.description.resumo | 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. | pt_BR |
| dc.embargo.terms | aberto | pt_BR |
| dc.identifier.uri | http://hdl.handle.net/11422/23625 | |
| dc.language | por | pt_BR |
| dc.publisher | Universidade Federal do Rio de Janeiro | pt_BR |
| dc.publisher.country | Brasil | pt_BR |
| dc.publisher.department | Instituto de Computação | pt_BR |
| dc.publisher.initials | UFRJ | pt_BR |
| dc.rights | Acesso Aberto | pt_BR |
| dc.subject | Computação concorrente | pt_BR |
| dc.subject | Métodos formais | pt_BR |
| dc.subject | Verificação de modelos | pt_BR |
| dc.subject | TLA+ | pt_BR |
| dc.subject | Concurrent systems | pt_BR |
| dc.subject | Formal methods | pt_BR |
| dc.subject | Formal methods | pt_BR |
| dc.subject.cnpq | CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO | pt_BR |
| dc.title | Relato de experiência em modelagem e verificação de algoritmos concorrentes com TLA+ | pt_BR |
| dc.type | Trabalho de conclusão de graduação | pt_BR |