Formal verification applied to attitude control software of unmanned aerial vehicles

Detalhes bibliográficos
Ano de defesa: 2018
Autor(a) principal: Chaves, Lennon Corrêa
Outros Autores: http://lattes.cnpq.br/9580905200186919
Orientador(a): Não Informado pela instituição
Banca de defesa: Não Informado pela instituição
Tipo de documento: Dissertação
Tipo de acesso: Acesso aberto
Idioma: eng
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:
Veículos Aéreos não tripulados
Verificação simbólica de modelos
Controladores de ponto-fixo
Sistemas Embarcados
ENGENHARIAS: ENGENHARIA ELÉTRICA
Link de acesso: https://tede.ufam.edu.br/handle/tede/6368
Resumo: Durante as últimas décadas, técnicas de verificação de modelos tem sido utilizadas para melhorar a confiabilidade de sistemas, no que diz respeito a veículos aéreos não-tripulados (VANTs). Contudo, existem poucos esforços focados em aplicar esses métodos ao controle de sistemas, especialmente os relativos à investigação de erros de implementação de baixo nível, os quais estão relacionados a controladores digitais e compatibilidade de hardware. O presente trabalho aborda os problemas mencionados e propõe a aplicação de uma ferramenta de verificação limitada de modelos, conhecida como Digital System Verifier (DSVerifier) ou Verificador de Sistemas Digitais, à verificação de implementação de sistemas digiais, com o objetivo de investigar problemas em controladores digitais projetados para sistemas de atitude em VANTs. Apresenta-se uma metodologia de verificação para procurar por erros de implementação relacionados a efeitos de tamanho de palavra finita (i.e, estouros aritméticos e ciclos-limites), em controladores de atitude de VANTs, juntamente com sua avaliação, o que visa garantir a corretude desses sistemas. Resultados experimentais mostram que falhas encontradas em software de controle de atitude de VANTs usados em vigilância aérea, as quais são dificilmente encontradas pro simulação e ferramentas de teste, podem ser facilmente identificadas pelo DSVerifier.

Registros relacionados