Modeling and Parameters Synthesis for an Air TrafficManagement System

  • Adilson Luiz Bonifácio
  • Arnaldo Vieira Moura
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1954)


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), which uses 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 synthesizedusing parametric analysis.All results were obtained on a 350MHz desktop PC, with 320MB of main memory.


Parameter Synthesis Vertical Separation Hybrid Automaton Nondeterministic Choice Horizontal Separation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Rajeev Alur, Thomas A. Henzinger, and Pei-Hsin Ho. Automatic symbolic verification of embedded systems. In Proceedings of the 14th Annual IEEE Real-Time Systems Symposium, pages 2–11. IEEE Computer Society Press, 1993.Google Scholar
  2. 2.
    Johan Bengtsson, Kim G. Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi. UPPAAL a tool suite for automatic verification of real–time systems. Technical Report RS-96-58, BRICS, Aalborg University, DENMARK and Department of Computer Systems, Uppsala University, Sweden, December 1996.Google Scholar
  3. 3.
    Adilson Luiz Bonifácio, Arnaldo Vieira Moura, João Batista Camargo Jr., and Jorge Rady Almeida Junior. Análise e Verificação de Segmentos de Via de uma Malha Metroviária. In Proceedings of the II Workshop on Formal Methods, pages 13–22, Florianópolis, Brazil, October 1999. (In Portuguese).Google Scholar
  4. 4.
    Adilson Luiz Bonifácio, Arnaldo Vieira Moura, João Batista Camargo Jr., and Jorge Rady Almeida Junior. Formal Parameters Synthesis for Track Segments of the Subway Mesh. In 7th Annual IEEE International Conference and Workshop on the Engineering of Computer Based Systems, pages 263–272, Edinburgh, Scotland, 3–7, April 2000. IEEE Computer Society Press.Google Scholar
  5. 5. Adilson Luiz Bonifácio, Arnaldo Vieira Moura, João Batista Camargo Jr., and Jorge Rady Almeida Junior. Formal Verification and Synthesis for an Air Traffic Management System. Technical Report 05, Computing Institute, University of Campinas, Campinas, Brazil, February 2000.Google Scholar
  6. 6.
    E. W. Dijkstra. Guarded commands, nondeterminacy and formal derivation of programs. CACM, 18(8):453–457, August 1975.zbMATHMathSciNetGoogle Scholar
  7. 7.
    Kathryn T. Heimerman. Air traffic control modeling. As appears in the book entitled Frontiers of Engineering 1997, National Academy Press, 1998.Google Scholar
  8. 8.
    Thomas A. Henzinger and Pei-Hsin Ho. HyTech: The cornell hybrid technology tool. Workshop on Hybrid Systems and Autonomous Control, October 1994.Google Scholar
  9. 9.
    Thomas A. Henzinger, Pei-Hsin Ho, and Howard Wong-Toi. A user guide to HyTech. In E. Brinksma, W. R. Cleaveland, K. G. Larsen, T. Margaria, and B. Steffen, editors, TACAS 95: Proceedings of the FirstWorkshop on Tools and Algorithms for the Construction and Analysis of Systems, volume 1019 of Lecture Notes in Computer Science, pages 41–71. Springer-Verlag, 1995.Google Scholar
  10. 10.
    Thomas A. Henzinger, Pei-Hsin Ho, and Howard Wong-Toi. HYTECH: A model checker for hybrid systems. In O. Grumberg, editor, CAV’97: Proceedings of the Ninth International Conference on Computer-Aided Verification, volume 1254 of Lecture Notes in Computer Science, pages 460–463. Springer-Verlag, 1997.Google Scholar
  11. 11.
    Thomas A. Henzinger, Benjamin Horowitz, Rupak Majumdar, and Howard Wong-Toi. Beyond HyTech: Hybrid systems analysis using interval numerical methods. In Nancy Lynch and Bruce H. Krogh, editors, Hybrid Systems: Computation and Control, Third International Workshop, volume 1790 of Lecture Notes in Computer Science, pages 130–144, Pittsburgh, April 2000. Springer-Verlag.Google Scholar
  12. 12.
    Pei-Hsin Ho. Automatic Analysis of Hybrid Systems. PhD thesis, Cornell University, August 1995.Google Scholar
  13. 13.
    John Law. Acas ii programme. ACAS Programme Manager, January 1999.Google Scholar
  14. 14.
    John Lygeros and Nancy Lynch. On the formal verification of the tcas conflict resolution algorithms. Technical report, Laboratory of Computer Science, Massachusetts Institute of Technology, 545 Technology Square, Cambridge, MA 02139, 1995.Google Scholar
  15. 15.
    Phil Scott. Technology and business: Self-control in the skies. Scientific American, pages 24–55, January 2000.Google Scholar
  16. 16.
    Claire Tomlin, George J. Pappas, and Shankar Satry. Conflict resolution for air traffic management: a study in multi-agent hybrid systems. In IEEE Conference on Decision and Control, Department of Electrical Engineering and Computer Sciences,University of California at Berkeley, Berkeley, CA 94720, 1997.Google Scholar
  17. 17.
    Lee F. Winder and James K. Kuchar. Evaluation of vertical collision avoidance maneuvers for parallel approach. In AIAA Guidance, Naviation, and Control Conference, Department of Aeronautics and Astronautics, Massachusetts Institute of Technology, Crambridge, MA 02139, August 1998. Boston, MA.Google Scholar

Copyright information

© Springer-VerlagBerlin Heidelberg 2000

Authors and Affiliations

  • Adilson Luiz Bonifácio
    • 1
  • Arnaldo Vieira Moura
    • 1
  1. 1.Computing InstituteUniversity of CampinasCampinasBrazil

Personalised recommendations