Dissertação

Formal verification applied to attitude control software of unmanned aerial vehicles

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

ver descrição completa

Autor principal: Chaves, Lennon Corrêa
Outros Autores: http://lattes.cnpq.br/9580905200186919
Grau: Dissertação
Idioma: eng
Publicado em: Universidade Federal do Amazonas 2018
Assuntos:
Veículos Aéreos não tripulados
Verificação simbólica de modelos
Controladores de ponto-fixo
Sistemas Embarcados
ENGENHARIAS: ENGENHARIA ELÉTRICA
Acesso em linha: https://tede.ufam.edu.br/handle/tede/6368
id oai:https:--tede.ufam.edu.br-handle-:tede-6368
recordtype dspace
spelling oai:https:--tede.ufam.edu.br-handle-:tede-63682018-05-11T05:04:17Z Formal verification applied to attitude control software of unmanned aerial vehicles Chaves, Lennon Corrêa Cordeiro, Lucas Carvalho http://lattes.cnpq.br/9580905200186919 http://lattes.cnpq.br/5005832876603012 Veículos Aéreos não tripulados Verificação simbólica de modelos Controladores de ponto-fixo Sistemas Embarcados ENGENHARIAS: ENGENHARIA ELÉTRICA 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. 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. 2018-05-10T17:56:14Z 2018-02-02 Dissertaçã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. https://tede.ufam.edu.br/handle/tede/6368 eng Acesso Aberto http://creativecommons.org/licenses/by-nc-nd/4.0/ application/pdf Universidade Federal do Amazonas Faculdade de Tecnologia Brasil UFAM Programa de Pós-graduação em Engenharia Elétrica
institution TEDE - Universidade Federal do Amazonas
collection TEDE-UFAM
language eng
topic Veículos Aéreos não tripulados
Verificação simbólica de modelos
Controladores de ponto-fixo
Sistemas Embarcados
ENGENHARIAS: ENGENHARIA ELÉTRICA
spellingShingle Veículos Aéreos não tripulados
Verificação simbólica de modelos
Controladores de ponto-fixo
Sistemas Embarcados
ENGENHARIAS: ENGENHARIA ELÉTRICA
Chaves, Lennon Corrêa
Formal verification applied to attitude control software of unmanned aerial vehicles
topic_facet Veículos Aéreos não tripulados
Verificação simbólica de modelos
Controladores de ponto-fixo
Sistemas Embarcados
ENGENHARIAS: ENGENHARIA ELÉTRICA
description 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.
author_additional Cordeiro, Lucas Carvalho
author_additionalStr Cordeiro, Lucas Carvalho
format Dissertação
author Chaves, Lennon Corrêa
author2 http://lattes.cnpq.br/9580905200186919
author2Str http://lattes.cnpq.br/9580905200186919
title Formal verification applied to attitude control software of unmanned aerial vehicles
title_short Formal verification applied to attitude control software of unmanned aerial vehicles
title_full Formal verification applied to attitude control software of unmanned aerial vehicles
title_fullStr Formal verification applied to attitude control software of unmanned aerial vehicles
title_full_unstemmed Formal verification applied to attitude control software of unmanned aerial vehicles
title_sort formal verification applied to attitude control software of unmanned aerial vehicles
publisher Universidade Federal do Amazonas
publishDate 2018
url https://tede.ufam.edu.br/handle/tede/6368
_version_ 1831969619033718784
score 11.753735

Registros relacionados