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