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-02 / 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. / 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.
| Identifer | oai:union.ndltd.org:IBICT/oai:http://localhost:tede/6368 |
| Date | 02 February 2018 |
| Creators | Chaves, Lennon Corrêa, 92-99155-6510 |
| Contributors | ppgee@ufam.edu.br, Cordeiro, Lucas Carvalho, Lima Filho, Eddie Batista de |
| Publisher | Universidade Federal do Amazonas, Programa de Pós-graduação em Engenharia Elétrica, UFAM, Brasil, Faculdade de Tecnologia |
| Source Sets | IBICT Brazilian ETDs |
| Language | English |
| Detected Language | Portuguese |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis |
| Format | application/pdf |
| Source | reponame:Biblioteca Digital de Teses e Dissertações da UFAM, instname:Universidade Federal do Amazonas, instacron:UFAM |
| Rights | http://creativecommons.org/licenses/by-nc-nd/4.0/, info:eu-repo/semantics/openAccess |
| Relation | -5930111888266832212, 500 |
Page generated in 0.0027 seconds