@techreport{TR-IC-00-05,
  number = {IC-00-05},
  author = {Adilson Luiz Bonifácio and Arnaldo Vieira Moura and João Batista de {Camargo Jr.} and Jorge Rady de {Almeida Jr.}},
  title = {Formal Verification and Synthesis for an Air Traffic Management System},
  month = {February},
  year = {2000}, 
  institution = {Institute of Computing, University of Campinas},
  note = {In English, 37 pages.
    \par\selectlanguage{brazil}\textbf{Resumo}
      O objetivo deste trabalho é aplicar técnicas de
      especificação formal para modelar sistemas
      distribuídos de tempo real provenientes de
      aplicações realistas. O sistemas alvo é um Sistema
      de Gerenciamento de Tráfego Aéreo (Air Traffic
      Management System - ATM), usando o protocolo do Sistema de
      alerta de Tráfego e Prevenção de Colisão
      (Traffic alert and Collision Avoidance System - TCAS). Os
      modelos formais desenvolvidos aqui são baseados na abordagem
      de autômatos híbridos. Ferramentas (semi)
      automáticas são usadas na verificação dos
      modelos, e alguns parâmetros importantes do sistema são
      sintetizados usando uma análise paramétrica. Todos os
      resultados foram obtidos sobre um PC de 350MHz típico, com
      320MB de memória.
    
    \par\selectlanguage{english}\textbf{Abstract}
      The aim of this work is to apply formal specification techniques
      to model real-time distributed systems arising from real-world
      applications. The target system is an Air Traffic Management
      System (ATM), using the Traffic alert and Collision Avoidance
      System (TCAS) protocol. The formal models developed here are
      based on the notion of hybrid automata. Semi-automatic tools are
      used in the verification of the models, and some important
      system parameters are synthesized using a parametric analysis.
      All results were obtained on a 350MHz desktop PC, with 320MB of
      main memory.
  }
}