MÉTODO DE MODELAGEM E VERIFICAÇÃO FORMAL APLICADO A SISTEMAS DE CONTROLE DE TRAFEGO AÉREO

Abstract

1. O desenvolvimento de sistemas complexos  é atualmente um dos problemas mais desatadores enfrentados pela Engenharia. Nos últimos anos, houve um aumento no tráfego aéreo, o que demanda uma modernização dos sistemas de tráfego aéreo atuais, muito dependentes na figura do controlador. Sistemas de trafego aéreo são sistemas considerados críticos em segurança e de tempo real. O objetivo do presente trabalho é a aplicação de um método de modelagem e verificação formal para o domínio especo de sistemas de tráfego aéreo. Com a adoção de técnicas de modelagem e verificação formal, pretende-se garantir eficiência no projeto e no desenvolvimento desses sistemas, além da sua corretude. Descreve-se um estudo de caso de três módulos reais do sistema de tráfego aéreo, em operação atualmente nos centros de controle brasileiros. Para verificação formal, é utilizada a ferramenta NuSMV e as propriedades a serem verificadas são descritas no lógico linear temporal (LTL) e computacional de árvore (CTL) para garantir que o sistema satisfaça requisitos dos tipos vivacidade e segurança.