Projeto EMBRAER

Projeto EMBRAER

Aeronaves remotamente pilotadas têm se tornado mais importantes a cada dia. O projeto destes sistemas, contudo, é muito complexo e sujeito a erros. O desenvolvimento de um sistema para aeronaves remotamente pilotadas tem um custo elevado devido ao potencial grande número de erros e da dificuldade em encontrar-los e corrigi-los. Métodos tradicionais de análise e validação incluem testes e simulações, mas a cobertura de falhas destes métodos é muito baixa, porque o número de comportamento possível em um sistema aumenta exponencialmente enquanto um seu tamanho aumenta linearmente. Uma alternativa a estes métodos de validação tradicionais são métodos formais, que têm como característica explorar exaustivamente todas as possíveis execuções de um sistema avaliado.Desta forma, os resultados obtidos são garantidos, ao contrário de testes e simulações, que exploram somente uma parcela dos padrões possíveis. Algoritmos e estruturas de dados eficientes garantem que as ferramentas modernas podem ser capazes de analisar os sistemas de complexidade industrial. Este projeto tem como objetivo desenvolver uma metodologia baseada na aplicação de métodos formais para projetar e analisar sistemas de aeronaves remotamente pilotadas. Uma fase inicial a partir da modelagem de um sistema já existente, que será posteriormente refinado e acrescido de funcionalidades para gerar um sistema mais realista e adequado para aplicações reais da Embraer.Além disso, será desenvolvido no projeto uma ferramenta de tradução automática de descrições de sistemas aeronáuticos em Simulink para ferramentas de verificação formal, que permitir a automatização deste tipo de análise no futuro. Esperamos ao fim do projeto propor um sistema de aeronaves remotamente pilotadas que está correto por construção, e desenvolver ferramentas e metodologias que facilitam a aplicação destes métodos em outros tipos de sistemas aeronáuticos. A certificação de propriedades formais dar-se-á mediante a aplicação de duas técnicas bem conforme: a verificação de modelos, e a interpretação abstrata de programas.