Relato de experiência em modelagem e verificação de algoritmos concorrentes com TLA+

Cruz, Jones Martins Vieira da

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

Registro completo de metadados

Campo DC	Valor	Idioma
dc.contributor.advisor	Moreira, Anamaria Martins	-
dc.contributor.author	Cruz, Jones Martins Vieira da	-
dc.date.accessioned	2024-09-06T15:50:15Z	-
dc.date.available	2024-09-08T03:00:17Z	-
dc.date.issued	2024-06-26	-
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.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.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
dc.contributor.advisorCo1	Rossetto, Silvana	-
dc.contributor.referee1	Menasché, Daniel Sadoc	-
dc.contributor.referee2	Paixão, João Antônio Récio da	-
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.publisher.country	Brasil	pt_BR
dc.publisher.department	Instituto de Computação	pt_BR
dc.publisher.initials	UFRJ	pt_BR
dc.subject.cnpq	CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO	pt_BR
dc.embargo.terms	aberto	pt_BR
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

Mostrar registro simples do item Recomendar este item Visualizar estatísticas