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

Cruz, Jones Martins Vieira da

Please use this identifier to cite or link to this item: http://hdl.handle.net/11422/23625

Full metadata record

DC Field	Value	Language
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
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

Show simple item record Recommend this item View Statistics

Pantheon Institutional repository