Verificação de programas multi-tarefas baseado no framework multiplataforma QT
Ano de defesa: | 2019 |
---|---|
Autor(a) principal: | |
Outros Autores: | |
Orientador(a): | |
Banca de defesa: | |
Tipo de documento: | Dissertação |
Tipo de acesso: | Acesso aberto |
Idioma: | por |
Instituição de defesa: |
Universidade Federal do Amazonas
Faculdade de Tecnologia Brasil UFAM Programa de Pós-graduação em Engenharia Elétrica |
Programa de Pós-Graduação: |
Não Informado pela instituição
|
Departamento: |
Não Informado pela instituição
|
País: |
Não Informado pela instituição
|
Palavras-chave em Português: | |
Link de acesso: | https://tede.ufam.edu.br/handle/tede/7541 |
Resumo: | 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. |