Melhorando a segurança de programas numéricos

Abstract

Este trabalho discute como a precisão dos erros de arredondamento envolvidos em implementações reais do sistema de gerenciamento da NASA para veículos não tripulados DAIDALUS afetam a segurança geral do sistema. A biblioteca DAIDALUS fornece definições formais para os conceitos de Detecção e Evasão em aviônica demonstrados mecanicamente no assistente de provas PVS. No entanto, tais verificações são apenas certificados do bom comportamento da especificação do ponto de vista lógico, o que não garante a precisão dos algoritmos implementados sob restrições aritméticas de ponto flutuante. Nossa análise assume o padrão IEEE 754 de ponto flutuante, implementados em diversas linguagens de programação, e a técnica de verificação se baseia na geração de uma especificação de primeira ordem dos cálculos numéricos. Uma característica proeminente da abordagem é dividir a especificação em fatias definidas de acordo com os diferentes ramos de computação. O fatiamento é crucial para simplificar a análise formal das computações com aritmética de ponto flutuante.