Pantheon Institutional repository
Collect, preserve and disseminate digital academic production in all areas of knowledge.
Comprise the assets of the repository, in addition to theses and dissertations at UFRJ, scientific articles, electronic books, book chapters and papers presented at events for teachers, researchers, administrative staff and students of master's and doctoral degrees.
Please use this identifier to cite or link to this item:
http://hdl.handle.net/11422/23625| Type: | Trabalho de conclusão de graduação |
| Title: | Relato de experiência em modelagem e verificação de algoritmos concorrentes com TLA+ |
| Author(s)/Inventor(s): | Cruz, Jones Martins Vieira da |
| Advisor: | Moreira, Anamaria Martins |
| Co-advisor: | Rossetto, Silvana |
| Abstract: | 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. |
| Keywords: | Computação concorrente Métodos formais Verificação de modelos TLA+ Concurrent systems Formal methods Formal methods |
| Subject CNPq: | CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO |
| Production unit: | Instituto de Computação |
| Publisher: | Universidade Federal do Rio de Janeiro |
| Issue Date: | 26-Jun-2024 |
| Publisher country: | Brasil |
| Language: | por |
| Right access: | Acesso Aberto |
| Appears in Collections: | Ciência da Computação |
Files in This Item:
| File | Description | Size | Format | |
|---|---|---|---|---|
| JMVCruz.pdf | 565.18 kB | Adobe PDF | View/Open |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.