Método de modelagem e verificação formal aplicado a sistemas de tráfego aéreo.

• Ano de defesa: 2018
• Autor(a) principal: Costa, Rafael Leme
• Tipo de documento: Dissertação
• Tipo de acesso: Acesso aberto
• Idioma: por
• Instituição de defesa: Biblioteca Digitais de Teses e Dissertações da USP
• Palavras-chave em Português: Air traffic; CTL; Formal verification; Model checking; Safety-critical systems; Tráfego aéreo (Sistemas; Modelagem); Verificação e validação de software
• Link de acesso: http://www.teses.usp.br/teses/disponiveis/3/3152/tde-05112018-091509/

O desenvolvimento de sistemas críticos é atualmente um dos problemas mais desafiadores enfrentados pela Engenharia. Há frequentemente uma pressão para se reduzir o tempo total de desenvolvimento, o que dificulta a entrega de sistemas com um mínimo aceitável de defeitos. 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 é estabelecer um método de modelagem e verificação formal para sistemas críticos, com aplicação no domínio de tráfego aéreo. Com a adoção de técnicas de modelagem e verificação formal, pretende-se garantir a corretude dos sistemas frente aos requisitos inicialmente especificados e a detecção de erros em fases mais iniciais do projeto, o que resultaria em menores custos envolvidos na sua correção. São fornecidas diretivas para a aplicação do método através de um estudo de caso, baseado em três módulos de um sistema ATC em baixo nível de abstração, para a validação do funcionamento de módulos de software. Para verificação formal, é utilizada a ferramenta NuSMV e as propriedades a serem verificadas são descritas na lógica computacional de árvore (CTL) para garantir que o sistema satisfaça requisitos dos tipos vivacidade e segurança.