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