Formal verification applied to attitude control software of unmanned aerial vehicles

Submitted by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2018-05-10T17:55:53Z No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) dissertacao_lennon_chaves.pdf: 2813829 bytes, checksum: 48c3fbefe451491c81bbf9ddb680a318 (MD5)Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2018-05-10T17:56:13Z (GMT) No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) dissertacao_lennon_chaves.pdf: 2813829 bytes, checksum: 48c3fbefe451491c81bbf9ddb680a318 (MD5)Made available in DSpace on 2018-05-10T17:56:14Z (GMT). No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) dissertacao_lennon_chaves.pdf: 2813829 bytes, checksum: 48c3fbefe451491c81bbf9ddb680a318 (MD5) Previous issue date: 2018-02-0292-99155-6510During 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.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