Abstract
The air traffic control (ATC) is safety, monetary and environmental critical system. Its failure may cause the loss of human life, severe injuries, loss of money and environmental issues. The complexity of such systems requires formal modeling and step by step design processes. In this paper we investigate the use of formal method VDM++ to specify and verify the arrival procedure of aircrafts. The control along arrival procedure changes from the ramp to the gate controller to make possible the safe arrival. For the specification the bottom up approach is used to model the system. Initially, aircraft, ramp and gate controller are specified, then all are combine for their synchronize approach. The specification and syntactical verification are performed by VDM++ which is an object oriented model based formal approach. [Yousaf S, Khan SA, Zafar NA and Farooq A and Khan MA. Formal Analysis of Arrival Procedure of Air Traffic Control System. Life Sci J 2012;9(4):3094-3098] (ISSN:1097-8135). http://www.lifesciencesite.com. 454