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.

Developing safety critical systems is one of the most challenging problems in Engineering nowadays. There is usually a pressure to reduce the total time of the development, what makes it difficult to deliver systems with an acceptable low level of defects. In the recent years, there has been an increase in air trffic, what demands a modernization in the current air traffic systems, which are very dependent on the human controller. Air traffic systems are considered safety critical and real time systems. The objective of the present work is to establish a modeling and formal verification method for critical systems, applicable to the air traffic domain. By adopting modeling and formal verification techniques, it is expected to ensure the systems' correctness compared with the initially specified requirements and the error detection in the initial phases of the project. Guidelines are provided for applying the method by means of a case study, based in three modules of and ATC system in a low abstraction level, for the validation of the operation of software modules. For the formal verification, it is used the NuSMV tool and the properties to be checked are described in the computational tree logic (CTL) to ensure that the system satisfies requirements of liveness and safety types.