Formal Verification and Validation of Aircraft Departure Process in Air Traffic Control System Using VDM++

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.