Pantheon Repositório Institucional da UFRJ
Coleta, preserva e divulga a produção acadêmica digital em todas as áreas do conhecimento.
São os ativos do repositório, além de teses e dissertações da UFRJ, artigos científicos, livros eletrônicos, capítulos de livros e trabalhos apresentados em eventos por professores, pesquisadores, funcionários administrativos e alunos de mestrado e doutorado.
Use este identificador para citar ou linkar para este item:
http://hdl.handle.net/11422/23625| Tipo: | 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 |
| Orientador: | Moreira, Anamaria Martins |
| Coorientador: | Rossetto, Silvana |
| 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. |
| Palavras-chave: | Computação concorrente Métodos formais Verificação de modelos TLA+ Concurrent systems Formal methods Formal methods |
| Assunto CNPq: | CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO |
| Unidade produtora: | Instituto de Computação |
| Editora: | Universidade Federal do Rio de Janeiro |
| Data de publicação: | 26-Jun-2024 |
| País de publicação: | Brasil |
| Idioma da publicação: | por |
| Tipo de acesso: | Acesso Aberto |
| Aparece nas coleções: | Ciência da Computação |
Arquivos associados a este item:
| Arquivo | Descrição | Tamanho | Formato | |
|---|---|---|---|---|
| JMVCruz.pdf | 565.18 kB | Adobe PDF | Visualizar/Abrir |
Os itens no repositório estão protegidos por copyright, com todos os direitos reservados, salvo quando é indicado o contrário.