@MASTERSTHESIS{ 2019:1905879555,
 	title = {Verifica??o de programas multi-tarefas baseado no framework multiplataforma QT},
 	year = {2019},
 	url = "https://tede.ufam.edu.br/handle/tede/7541",
 	abstract = "Com o avan?o da tecnologia, progressos t?m acontecido no que diz respeito ao desenvolvimento de hardware e software. O resultado de tais avan?os ? decorrente da evolu??o das aplica??es que, atualmente, requerem mais capacidade de processamento e armazenamento de dados. A partir desta realidade, a ind?stria investe fortemente em processos de verifica??o r?pidos e autom?ticos. Com o intuito de obter a diminui??o das taxas de erros presentes nos sistemas produzidos, durante o processo de desenvolvimento ? de fundamental import?ncia utilizar t?cnicas adequadas para a implementa??o do paralelismo e da sincroniza??o dos dados,
 para que possa ser extra?do o desempenho m?ximo do sistema produzido. Tendo em vista que o tempo do processo de desenvolvimento est? cada vez menor e a robustez dos sistemas tende a aumentar exponencialmente com o tempo, muitos frameworks t?m sido utilizados no processo de desenvolvimento das empresas de sistemas embarcados, com o intuito de acelerar os processos de desenvolvimento. Um frameworkque tem se destacando ? o de desenvolvimento multi-plataforma chamado Qt, que conta com um amplo conjunto de bibliotecas de f?cil implementa??o, manuten??o e multi-plataforma, para sistemas multi-tarefas. Sendo assim, o presente trabalho prop?e um conjunto de bibliotecas simplificadas chamadas de Modelo Operacional Simplificado Multi-Tarefas Qt, similares ? biblioteca padr?o para a cria??o e manipula??o de threads dentro do framework Qt. Estas bibliotecas foram integradas inicialmente ao verificador de software Efficient SMT-Based Bounded Model Checking (ESBMC) de forma que, atrav?s do modelo operacional proposto, o verificador ESBMC possa realizar a verifica??o de aplica??es que utilizam o framework Qt para implementar programas concorrentes. A inclus?o do modelo operacional nos processos de verifica??o do ESBMC mostrou-se uma excelente abordagem para a verifica??o de programas multi-tarefas Qt, tendo uma taxa de verifica??es bem sucedidas de 90%. O modelo operacional proposto mostrou sua versatilidade ao ser inclu?do nos processos de verifica??es de outros dois verificadores de modelos chamados DIVINE e LLBMC. O verificador de modelos DIVINE obteve uma taxa de verifica??es bem sucedidas de 87%, j? o verificador
 de modelos LLBMC obteve uma taxa de 85%. Com isso, podemos validar a viabilidade da abordagem que propomos para verificar programas multi-tarefas Qt. Por fim, a metodologia que propomos encontra-se em estado da arte, sendo a primeira a viabilizar a verifica??o de estruturas multi-tarefas Qt, podendo ser expandido, para outras estruturas que ainda n?o foram cobertas.",
 	publisher = {Universidade Federal do Amazonas},
 	scholl = {Programa de P?s-gradua??o em Engenharia El?trica},
 	note = {Faculdade de Tecnologia}
}