???item.export.label??? ???item.export.type.endnote??? ???item.export.type.bibtex???

Please use this identifier to cite or link to this item: https://tede.ufam.edu.br/handle/tede/5492
???metadata.dc.type???: Dissertação
Title: Verificação de programas C++ baseados no framework crossplataforma Qt
???metadata.dc.creator???: Garcia, Mário Angel Praia 
???metadata.dc.contributor.advisor1???: Cordeiro, Lucas Carvalho
First advisor-co: Silva Júnior, Waldir Sabino da
???metadata.dc.contributor.referee1???: Barreto, Raimundo da Silva
???metadata.dc.contributor.referee2???: Conte, Tayana Uchôa
???metadata.dc.description.resumo???: O desenvolvimento de software para sistemas embarcados tem crescido rapidamente, o que na maioria das vezes acarreta em um aumento da complexidade associada a esse tipo de projeto. Como consequência, as empresas de eletrônica de consumo costumam investir recursos em mecanismos de verificação rápida e automática, com o intuito de desenvolver sistemas robustos e assim reduzir as taxas de recall de produtos. Além disso, a redução no tempo de desenvolvimento e na robustez dos sistemas desenvolvidos podem ser alcançados através de frameworks multi-plataformas, tais como Qt, que oferece um conjunto de bibliotecas (gráficas) confiáveis para vários dispositivos embarcados. Desta forma, este trabalho propõe uma versão simplificada do framework Qt que integrado a um verificador baseado nas teorias do módulo da satisfatibilidade, denominado Efficient SMT-Based Bounded Model Checker (ESBMC++), verifica aplicações reais que ultilizam o Qt, apresentando uma taxa de sucesso de 89%, para os benchmarks desenvolvidos. Com a versão simplificada do framework Qt proposto, também foi feita uma avaliação ultilizando outros verificadores que se encontram no estado da arte para verificação de programas em C++ e uma avalição a cerca de seu nível de conformidade. Dessa maneira, a metodologia proposta se afirma como a primeira a verificar formalmente aplicações baseadas no framework Qt, além de possuir um potencial para desenvolver novas frentes para a verificação de código portátil.
Abstract: The software development for embedded systems is getting faster and faster, which generally incurs an increase in the associated complexity. As a consequence, consumer electronics companies usually invest a lot of resources in fast and automatic verification mechanisms, in order to create robust systems and reduce product recall rates. In addition, further development-time reduction and system robustness can be achieved through cross-platform frameworks, such as Qt, which favor the reliable port of software stacks to different devices. Based on that, the present work proposes a simplified version of the Qt framework, which is integrated into a checker based on satisfiability modulo theories (SMT), name as the efficient SMT-based bounded model checker (ESBMC++), for verifying actual Qt-based applications, and presents a success rate of 89%, for the developed benchmark suite. We also evaluate our simplified version of the Qt framework using other state-of-the-art verifiers for C++ programs and an evaluation about their level of compliance. It is worth mentioning that the proposed methodology is the first one to formally verify Qt-based applications, which has the potential to devise new directions for software verification of portable code.
Keywords: Framework Qt
Bounded Model Checking
Satisfiability Modulo Theories (SMT)
???metadata.dc.subject.cnpq???: ENGENHARIAS: ENGENHARIA ELÉTRICA
Language: por
???metadata.dc.publisher.country???: Brasil
Publisher: Universidade Federal do Amazonas
???metadata.dc.publisher.initials???: UFAM
???metadata.dc.publisher.department???: Faculdade de Tecnologia
???metadata.dc.publisher.program???: Programa de Pós-graduação em Engenharia Elétrica
Citation: GARCIA, Mário Angel Praia. Verificação de programas C++ baseados no framework crossplataforma Qt. 2016. 68 f. Dissertação (Mestrado em Engenharia Elétrica) - Universidade Federal do Amazonas, Manaus, 2016.
???metadata.dc.rights???: Acesso Aberto
???metadata.dc.rights.uri???: http://creativecommons.org/licenses/by-nc-nd/4.0/
URI: http://tede.ufam.edu.br/handle/tede/5492
Issue Date: 13-Sep-2016
Appears in Collections:Mestrado em Engenharia Elétrica

Files in This Item:
File Description SizeFormat 
Dissertação - Mário A. P. Garcia.pdf1.74 MBAdobe PDFThumbnail

Download/Open Preview


This item is licensed under a Creative Commons License Creative Commons