Abstract—The safety critical systems are those whose failure may cause the loss of human life, serious injuries and financial disasters. The air traffic control system (ATC) is a safety critical system and rise in the air traffic volume make it more critical and complex which caused for the unwanted delay in the aircraft departure process. To ensure its safety it requires advance methodologies for its designing process. The VDM++ is an emerging technique based on mathematical notation having object oriented features and used to specify and verify the software system. This technique is used to formalize the departure process of ATC system. The departure process is controlled by the air traffic controllers. The air traffic controllers control the aircraft traffic. This departure process is made possible with the help of the ground and local controller. Initially, the aircraft is under the control of ground controller. Further the control is transfer to the local controller. These both controllers communicate to aircraft and also to each other for safe and secure movement of aircraft and finally the aircraft depart from the airport.
Index Terms—VDM, VDM++, ATC, formal method.
Shahid Yousaf is with Department of Computer Science & IT, The
University of Lahore, Pakistan (e-mail: firstname.lastname@example.org).
Nazir Ahmad Zafar is with the Department of Computer Science, College of CS & IT, King Faisal University, Al Hassa, Saudi Arabia (e-mail: email@example.com ).
Sher Afzal khan is with the Department of Computer Science, Abdul Wali Khan University, Mardan, Pakistan (e-mail: firstname.lastname@example.org).
Cite: Shahid Yousaf, Nazir Ahmad Zafar, and Sher Afzal Khan, "Formal Verification and Validation of Aircraft Departure Process in Air Traffic Control System Using VDM++," International Journal of Engineering and Technology vol. 4, no. 6, pp. 755-759, 2012.