Dissertação

Verificação de programas C++ baseados no framework crossplataforma Qt

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ápi...

ver descrição completa

Autor principal: Garcia, Mário Angel Praia
Outros Autores: http://lattes.cnpq.br/4530652865344771
Grau: Dissertação
Idioma: por
Publicado em: Universidade Federal do Amazonas 2017
Assuntos:
Framework Qt
Bounded Model Checking
Satisfiability Modulo Theories (SMT)
ENGENHARIAS: ENGENHARIA ELÉTRICA
Acesso em linha: http://tede.ufam.edu.br/handle/tede/5492
id oai:https:--tede.ufam.edu.br-handle-:tede-5492
recordtype dspace
spelling oai:https:--tede.ufam.edu.br-handle-:tede-54922017-02-08T05:03:57Z Verificação de programas C++ baseados no framework crossplataforma Qt Garcia, Mário Angel Praia Cordeiro, Lucas Carvalho http://lattes.cnpq.br/4530652865344771 http://lattes.cnpq.br/5005832876603012 Barreto, Raimundo da Silva Conte, Tayana Uchôa Framework Qt Bounded Model Checking Satisfiability Modulo Theories (SMT) ENGENHARIAS: ENGENHARIA ELÉTRICA 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. 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. CAPES - Coordenação de Aperfeiçoamento de Pessoal de Nível Superior 2017-02-07T17:48:08Z 2016-09-13 Dissertação 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. http://tede.ufam.edu.br/handle/tede/5492 por Acesso Aberto http://creativecommons.org/licenses/by-nc-nd/4.0/ application/pdf Universidade Federal do Amazonas Faculdade de Tecnologia Brasil UFAM Programa de Pós-graduação em Engenharia Elétrica
institution TEDE - Universidade Federal do Amazonas
collection TEDE-UFAM
language por
topic Framework Qt
Bounded Model Checking
Satisfiability Modulo Theories (SMT)
ENGENHARIAS: ENGENHARIA ELÉTRICA
spellingShingle Framework Qt
Bounded Model Checking
Satisfiability Modulo Theories (SMT)
ENGENHARIAS: ENGENHARIA ELÉTRICA
Garcia, Mário Angel Praia
Verificação de programas C++ baseados no framework crossplataforma Qt
topic_facet Framework Qt
Bounded Model Checking
Satisfiability Modulo Theories (SMT)
ENGENHARIAS: ENGENHARIA ELÉTRICA
description 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.
author_additional Cordeiro, Lucas Carvalho
author_additionalStr Cordeiro, Lucas Carvalho
format Dissertação
author Garcia, Mário Angel Praia
author2 http://lattes.cnpq.br/4530652865344771
author2Str http://lattes.cnpq.br/4530652865344771
title Verificação de programas C++ baseados no framework crossplataforma Qt
title_short Verificação de programas C++ baseados no framework crossplataforma Qt
title_full Verificação de programas C++ baseados no framework crossplataforma Qt
title_fullStr Verificação de programas C++ baseados no framework crossplataforma Qt
title_full_unstemmed Verificação de programas C++ baseados no framework crossplataforma Qt
title_sort verificação de programas c++ baseados no framework crossplataforma qt
publisher Universidade Federal do Amazonas
publishDate 2017
url http://tede.ufam.edu.br/handle/tede/5492
_version_ 1831969469221568512
score 11.755432

Registros relacionados