Submitted by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2017-02-07T17:47:31Z
No. of bitstreams: 2
license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5)
Dissertação - Mário A. P. Garcia.pdf: 1777955 bytes, checksum: bbc5f97c856505f518492e5c8ec65c28 (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2017-02-07T17:47:47Z (GMT) No. of bitstreams: 2
license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5)
Dissertação - Mário A. P. Garcia.pdf: 1777955 bytes, checksum: bbc5f97c856505f518492e5c8ec65c28 (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2017-02-07T17:48:08Z (GMT) No. of bitstreams: 2
license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5)
Dissertação - Mário A. P. Garcia.pdf: 1777955 bytes, checksum: bbc5f97c856505f518492e5c8ec65c28 (MD5) / Made available in DSpace on 2017-02-07T17:48:08Z (GMT). No. of bitstreams: 2
license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5)
Dissertação - Mário A. P. Garcia.pdf: 1777955 bytes, checksum: bbc5f97c856505f518492e5c8ec65c28 (MD5)
Previous issue date: 2016-09-13 / CAPES - Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / 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. / 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.
| Identifer | oai:union.ndltd.org:IBICT/oai:http://localhost:tede/5492 |
| Date | 13 September 2016 |
| Creators | Garcia, Mário Angel Praia |
| Contributors | Cordeiro, Lucas Carvalho, Silva Júnior, Waldir Sabino da, Barreto, Raimundo da Silva, Conte, Tayana Uchôa |
| Publisher | Universidade Federal do Amazonas, Programa de Pós-graduação em Engenharia Elétrica, UFAM, Brasil, Faculdade de Tecnologia |
| Source Sets | IBICT Brazilian ETDs |
| Language | Portuguese |
| Detected Language | Portuguese |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis |
| Format | application/pdf |
| Source | reponame:Biblioteca Digital de Teses e Dissertações da UFAM, instname:Universidade Federal do Amazonas, instacron:UFAM |
| Rights | http://creativecommons.org/licenses/by-nc-nd/4.0/, info:eu-repo/semantics/openAccess |
| Relation | -161377036298529205, 600, 500, -5930111888266832212 |
Page generated in 0.0018 seconds