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