Método de Modelagem e Verificação Formal aplicado a Sistemas de Controle de Tráfego Aéreo
Rafael Leme Costa1; Fabio Seiti Aguchiku1; Douglas D.S. Santana1; Newton Maruyama1
1 Departamento de Engenharia Mecatrônica e Sistemas Mecânicos da Escola Politécnica da USP
Baixar PDF doi:10.20906/CPS/CBA2018-0307
Resumo
O desenvolvimento de sistemas complexos é atualmente um dos problemas mais desafiadores 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 tráfego 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 específico 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 nas lógicas linear temporal (LTL) e computacional de árvore (CTL) para garantir que o sistema satisfaça requisitos dos tipos vivacidade e segurança.
Palavras-chave: CTL; LTL; modelagem; tráfego aéreo; verificação formal