Exportar este item: EndNote BibTex

Use este identificador para citar ou linkar para este item: https://tede.ufam.edu.br/handle/tede/6368
Tipo do documento: Dissertação
Título: Formal verification applied to attitude control software of unmanned aerial vehicles
Autor: Chaves, Lennon Corrêa 
Primeiro orientador: Cordeiro, Lucas Carvalho
Primeiro coorientador: Lima Filho, Eddie Batista de
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.
Abstract: During the last decades, model checking techniques have been applied to improve overall system reliability, in unmanned aerial vehicle (UAV) approaches. Nonetheless, there is little effort focused on applying those methods to the control-system domain, especially when it comes to the investigation of low-level implementation errors, which are related to digital controllers and hardware compatibility. The present study addresses the mentioned problems and proposes the application of a bounded model checking tool, named as Digital System Verifier (DSVerifier), to the verification of digital-system implementation issues, in order to investigate problems that emerge in digital controllers designed for UAV attitude systems. A verification methodology to search for implementation errors related to finite word-length effects ( e.g., arithmetic overflows and limit cycles), in UAV attitude controllers, is presented, along with its evaluation, which aims to ensure correct-by-design systems. Experimental results show that failures in UAV attitude control software used in aerial surveillance, which are hardly found by simulation and testing tools, can be easily identified by DSVerifier.
Palavras-chave: Veículos Aéreos não tripulados
Verificação simbólica de modelos
Controladores de ponto-fixo
Sistemas Embarcados
Área(s) do CNPq: ENGENHARIAS: ENGENHARIA ELÉTRICA
Idioma: eng
País: Brasil
Instituição: Universidade Federal do Amazonas
Sigla da instituição: UFAM
Departamento: Faculdade de Tecnologia
Programa: Programa de Pós-graduação em Engenharia Elétrica
Citação: CHAVES, Lennon Corrêa. Formal verification applied to attitude control software of unmanned aerial vehicles. 2018. 95 f. Dissertação (Mestrado em Engenharia Elétrica) - Universidade Federal do Amazonas, Manaus, 2018.
Tipo de acesso: Acesso Aberto
Endereço da licença: http://creativecommons.org/licenses/by-nc-nd/4.0/
URI: https://tede.ufam.edu.br/handle/tede/6368
Data de defesa: 2-Fev-2018
Aparece nas coleções:Mestrado em Engenharia Elétrica

Arquivos associados a este item:
Arquivo Descrição TamanhoFormato 
Dissertação_Lennon Chaves.pdf2,75 MBAdobe PDFThumbnail

Baixar/Abrir Pré-Visualizar


Este item está licenciada sob uma Licença Creative Commons Creative Commons