Métodos Formais Algébricos para Geração de Invariantes
Resumo
É bem sabido que a eficácia de métodos de verificação formal de sistemas embarcados, ou sistemas híbridos, depende da geração automática e eficiente de invariantes precisas. Nesta tese propusemos , primordialmente, a redução de problemas de geração de invariantes para problemas algébricos lineares. Logrando esta contribução, conseguimos ultrapassar as deficiências dos mais modernos métodos de geração de invariante hoje conhecidos, permitindo, assim, a geração eficiente de invariantes para software, programs complexos, sistemas híbridos e embarcados não lineares. Os algoritmos algébricos que propusemos apresentam complexidades significativamente inferiores aqueles que suportam as demais abordagens usadas hoje. Conseguimos fundamentar técnicas inéditas e eficientes que venham a formar o núcleo de novos algoritmos para a automação de processos dedutivos, e de novos algoritmos para verificação de modelos complexos que vão além dos limites alcançados hoje por outros métodos. Em particular, desenvolvemos métodos pioneiros que automaticamente gerem bases de invariantes expressas por séries de potências multi-variáveis e por funções transcendentais. Finalmente, estendemos o domínio de aplicações, acessíveis através de métodos de geração de invariantes, para a área de segurança fornecendo uma plataforma extensível baseada em invariantes pré-computadas para análise e deteção dos ataques de intrusões mais virulentos.
