Verificação automática de programas utilizando Lógica Dinâmica com aplicações a smart contracts

Registro completo de metadados
MetadadosDescriçãoIdioma
Autor(es): dc.contributorLopes, Bruno-
Autor(es): dc.contributorSantos, Jefferson de Barros-
Autor(es): dc.contributorCoelho, Igor Machado-
Autor(es): dc.creatorSantana, Allan Patrick de Freitas-
Data de aceite: dc.date.accessioned2024-07-11T18:03:50Z-
Data de disponibilização: dc.date.available2024-07-11T18:03:50Z-
Data de envio: dc.date.issued2021-07-16-
Data de envio: dc.date.issued2021-07-16-
Data de envio: dc.date.issued2019-
Fonte completa do material: dc.identifierhttps://app.uff.br/riuff/handle/1/22647-
Fonte: dc.identifier.urihttp://educapes.capes.gov.br/handle/capes/762795-
Descrição: dc.descriptionEm sistemas críticos falhas ou erros podem causar catástrofes, como mortes ou grandes perdas de dinheiro. A verificação de modelos provê uma forma automatizada para provar a corretude dos requisitos de um programa. E uma técnica conveniente para ser ´ utilizada em sistemas que necessitam de confiabilidade. Lógica Dinâmica Proposicional (PDL) é um sistema formal feito para se raciocinar sobre programas. Ela possui um modelo de Kripke simples e bom desempenho de verificação. Este trabalho apresenta uma implementação de compilação de programas em um subconjunto da linguagem C e tamb´em para Json sobre o modelo Smacco, ambos para a linguagem de PDL e desta para a linguagem de um verificador de modelos. Esta implementação está acoplada a um sistema de geração de modelos de Blockchain para modelar e verificar smart contracts-
Descrição: dc.descriptionIn critical systems, failures or errors can cause catastrophes, such as deaths or considerably losses of money. Model checking provides an automated way to prove the correctness of programs’ requirements. It is a convenient technique to be used in systems that need reliability. Propositional Dynamic Logic (PDL) is a formal system designed to reason about programs. It has a simple Kripke model and good verification performance. This work presents a compiler implementation from a subset of the C language and also for Json on the Smacco model, both to the PDL language, and after that to the language of a model checker. This implementation is coupled with a Blockchain model generation system to model and reason about smart contracts-
Formato: dc.formatapplication/pdf-
Idioma: dc.languagept_BR-
Direitos: dc.rightsAttribution-NonCommercial-NoDerivs 3.0 Brazil-
Direitos: dc.rightsOpen Access-
Direitos: dc.rightshttp://creativecommons.org/licenses/by-nc-nd/3.0/br/-
Direitos: dc.rightsCC-BY-SA-
Palavras-chave: dc.subjectVerificação de modelos-
Palavras-chave: dc.subjectPDL-
Palavras-chave: dc.subjectBlockchain-
Palavras-chave: dc.subjectCiência da computação-
Palavras-chave: dc.subjectModel checking-
Palavras-chave: dc.subjectPDL-
Palavras-chave: dc.subjectBlockchain-
Título: dc.titleVerificação automática de programas utilizando Lógica Dinâmica com aplicações a smart contracts-
Tipo de arquivo: dc.typeTrabalho de conclusão de curso-
Aparece nas coleções:Repositório Institucional da Universidade Federal Fluminense - RiUFF

Não existem arquivos associados a este item.