Please use this identifier to cite or link to this item: http://riu.ufam.edu.br/handle/prefix/3103
Full metadata record
DC FieldValueLanguage
dc.contributor.advisor1Lucas Carvalho Cordeiro-
dc.creatorFelipe Rodrigues Monteiro Sousa-
dc.date.accessioned2016-09-23T15:25:22Z-
dc.date.available2016-09-23T15:25:22Z-
dc.date.issued2013-07-31-
dc.identifier.urihttp://riu.ufam.edu.br/handle/prefix/3103-
dc.description.resumoNossa dependência no funcionamento correto de sistemas embarcados está aumentando rapidamente. A grande difusão de dispositivos móveis e da evolução dos softwares e hardwares que os compõe é um bom exemplo da importância desses sistemas. Os mesmos estão se tornando cada vez mais complexos e requerem processadores multi-core com memória compartilhada escalável para atender a crescente demanda do poder computacional. Desta maneira, a confiabilidade dos sistemas (distribuídos) embarcados é um assunto chave no processo de desenvolvimento de tais sistemas. As empresas cada vez mais procuram formas mais rápidas e baratas para verificar a confiabilidade dos seus sistemas, evitando assim grandes prejuízos. Uma das formas mais eficazes e de mais baixo custo é a verificação formal de software. Apesar da eficácia desse método de verificação, existem muitos sistemas que não podem ser verificados de forma automática pelo fato de não existir disponível no mercado um verificador que englobe determinadas linguagens ou frameworks. Um bom exemplo disso, são as aplicações que utilizam o framework multi-plataforma QT. Neste projeto de pesquisa, nós investigaremos, a partir de análise de aplicações reais, quais são as funcionalidades mais utilizadas do framework QT no mercado, definindo assim uma estrutura de como será feita a verificação de programas C++ que utilizam desse framework. Os algoritmos desenvolvidos neste projeto de pesquisa serão integrados no nosso verificador de código ESBMC (Efficient SMT-based Context-Bounded Model Checker) reconhecido internacionalmente pelo sua robustez e eficácia na verificação de programas ANSI-C, ganhando destaque ao conseguir medalha de ouro nas categorias SystemC e Concurrency na Primeira Competição Internacional em Verificação de Software (SVCOMP'12), além de ganhar medalha de bronze no ranking geral. É importante salientar que o acadêmico irá ter contato com o estado da arte da sub-área de Verificação Formal de Software, além disso, o acadêmico será capaz de implementar algoritmos de média complexidade, analisar aplicações reais, e desenvolver habilidades de desenvolvimento com a linguagem C++ e o framework Qt.pt_BR
dc.description.sponsorshipCNPQpt_BR
dc.formatPDF-
dc.languagept_BRpt_BR
dc.publisherUniversidade Federal do Amazonaspt_BR
dc.publisher.countryBrasilpt_BR
dc.publisher.departmentFaculdade de Tecnologiapt_BR
dc.publisher.departmentFaculdade de Tecnologiapt_BR
dc.publisher.programPROGRAMA PIBIC 2012pt_BR
dc.publisher.initialsUFAMpt_BR
dc.rightsAcesso Abertopt_BR
dc.subjectMétodos Formais-
dc.subjectVerificação de Software-
dc.subjectFramework QT-
dc.subject.cnpqCIÊNCIAS EXATAS E DA TERRA: ENGENHARIA DE SOFTWAREpt_BR
dc.titleVerificação Formal de Programas C++ que Usam o Framework Multi-Plataforma QTpt_BR
dc.typeRelatório de Pesquisapt_BR
dc.pibic.cursoEngenharia da Computaçãopt_BR
dc.pibic.nrprojetoPIB-E/0015/2012-
dc.pibic.projetoVerificação Formal de Programas C++ que Usam o Framework Multi-Plataforma QT-
dc.pibic.dtinicio2012-08-01-
dc.pibic.dtfim2013-07-31-
Appears in Collections:Relatórios finais de Iniciação Científica - Ciências Exatas e da Terra

Files in This Item:
File Description SizeFormat 
Felipe Rodrigues Monteiro Sousa.pdf927,14 kBAdobe PDFView/Open
Show simple item record Recommend this item


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.